The bear visits the dog. The dog likes the bear. The squirrel is blue. The squirrel is cold. The squirrel is green. The squirrel is kind. The squirrel visits the dog. If something is blue then it sees the dog. If something visits the bear and it does not like the bear then the bear is not cold. If something sees the dog then it is young.
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If something is blue then it sees the dog.
((("something" "is" "blue" "+")) -> ("something" "sees" "dog" "+"))
If something visits the bear and it does not like the bear then the bear is not cold.
((("something" "visits" "bear" "+") ("something" "likes" "bear" "~")) -> ("bear" "is" "cold" "-"))
If something sees the dog then it is young.
((("something" "sees" "dog" "+")) -> ("something" "is" "young" "+"))
The squirrel is blue.
True
1
proof
[(triple3)]
("squirrel" "is" "blue" "+")
triple3
The dog does not like the bear.
False
1
inv-proof
[(triple2)]
("dog" "likes" "bear" "-")
triple2
The squirrel sees the dog.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "sees" "dog" "+")
((triple3) -> (rule1 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The squirrel does not see the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "sees" "dog" "-")
((triple3) -> (rule1 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The squirrel is young.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("squirrel" "is" "young" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The squirrel is not young.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("squirrel" "is" "young" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The bear does not see the dog.
Unknown
inv-rconc
[@1: The bear sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "dog" "-")
The dog is young.
Unknown
rconc
[@2: The dog is young.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("dog" "is" "young" "+")
The bear is not young.
Unknown
inv-rconc
[@2: The bear is young.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("bear" "is" "young" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The dog does not visit the squirrel.
Unknown
inv-random
[@0: The dog visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "squirrel" "-")
The squirrel visits the bear.
Unknown
random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "+")
@0: The bear visits the dog.[(triple1)] The dog likes the bear.[(triple2)] The squirrel is blue.[(triple3)] The squirrel is cold.[(triple4)] The squirrel is green.[(triple5)] The squirrel is kind.[(triple6)] The squirrel visits the dog.[(triple7)] @1: The squirrel sees the dog.[(((triple3) -> rule1))] @2: The squirrel is young.[(((((triple3) -> rule1)) -> rule3))]
The bear visits the dog.
("bear" "visits" "dog" "+")
triple1
The dog likes the bear.
("dog" "likes" "bear" "+")
triple2
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple4
The squirrel is green.
("squirrel" "is" "green" "+")
triple5
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple6
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple7
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
((triple3) -> (rule1 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2