The bear eats the cow. The bear is kind. The bear likes the cat. The cat eats the squirrel. The cat is kind. The cat likes the cow. The cow is kind. The cow likes the cat. The squirrel eats the cat. The squirrel is young. If something likes the bear and the bear is big then the bear visits the squirrel. If something likes the cow then it likes the squirrel.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If something likes the bear and the bear is big then the bear visits the squirrel.
((("something" "likes" "bear" "+") ("bear" "is" "big" "+")) -> ("bear" "visits" "squirrel" "+"))
If something likes the cow then it likes the squirrel.
((("something" "likes" "cow" "+")) -> ("something" "likes" "squirrel" "+"))
The squirrel eats the cat.
True
1
proof
[(triple9)]
("squirrel" "eats" "cat" "+")
triple9
The bear does not like the cat.
False
1
inv-proof
[(triple3)]
("bear" "likes" "cat" "-")
triple3
The cat likes the squirrel.
True
2
proof
[(((triple6) -> rule2))]
("cat" "likes" "squirrel" "+")
((triple6) -> (rule2 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat does not like the squirrel.
False
2
inv-proof
[(((triple6) -> rule2))]
("cat" "likes" "squirrel" "-")
((triple6) -> (rule2 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The bear does not like the squirrel.
Unknown
inv-rconc
[@1: The bear likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "squirrel" "-")
The cow likes the squirrel.
Unknown
rconc
[@1: The cow likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "squirrel" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear eats the cow.[(triple1)] The bear is kind.[(triple2)] The bear likes the cat.[(triple3)] The cat eats the squirrel.[(triple4)] The cat is kind.[(triple5)] The cat likes the cow.[(triple6)] The cow is kind.[(triple7)] The cow likes the cat.[(triple8)] The squirrel eats the cat.[(triple9)] The squirrel is young.[(triple10)] @1: The cat likes the squirrel.[(((triple6) -> rule2))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear likes the cat.
("bear" "likes" "cat" "+")
triple3
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple4
The cat is kind.
("cat" "is" "kind" "+")
triple5
The cat likes the cow.
("cat" "likes" "cow" "+")
triple6
The cow is kind.
("cow" "is" "kind" "+")
triple7
The cow likes the cat.
("cow" "likes" "cat" "+")
triple8
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple9
The squirrel is young.
("squirrel" "is" "young" "+")
triple10
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((triple6) -> (rule2 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1