The bear eats the cat. The bear is kind. The bear is red. The bear likes the cat. The cat is round. The cat sees the bear. The lion is big. The lion likes the cat. The squirrel eats the cat. The squirrel is red. The squirrel likes the bear. The squirrel does not like the cat. If someone likes the cat and they like the squirrel then the cat sees the squirrel. If the bear likes the squirrel then the bear is blue. If someone sees the cat and the cat eats the bear then the cat is red. If the lion sees the cat and the lion is not big then the lion is blue. If someone eats the cat then they do not eat the lion. If someone is round and not red then they do not like the bear. If someone is round then they like the bear. If someone likes the bear then they eat the squirrel.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat is round.
("cat" "is" "round" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The lion is big.
("lion" "is" "big" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel does not like the cat.
("squirrel" "likes" "cat" "-")
If someone likes the cat and they like the squirrel then the cat sees the squirrel.
((("someone" "likes" "cat" "+") ("someone" "likes" "squirrel" "+")) -> ("cat" "sees" "squirrel" "+"))
If the bear likes the squirrel then the bear is blue.
((("bear" "likes" "squirrel" "+")) -> ("bear" "is" "blue" "+"))
If someone sees the cat and the cat eats the bear then the cat is red.
((("someone" "sees" "cat" "+") ("cat" "eats" "bear" "+")) -> ("cat" "is" "red" "+"))
If the lion sees the cat and the lion is not big then the lion is blue.
((("lion" "sees" "cat" "+") ("lion" "is" "big" "~")) -> ("lion" "is" "blue" "+"))
If someone eats the cat then they do not eat the lion.
((("someone" "eats" "cat" "+")) -> ("someone" "eats" "lion" "-"))
If someone is round and not red then they do not like the bear.
((("someone" "is" "round" "+") ("someone" "is" "red" "~")) -> ("someone" "likes" "bear" "-"))
If someone is round then they like the bear.
((("someone" "is" "round" "+")) -> ("someone" "likes" "bear" "+"))
If someone likes the bear then they eat the squirrel.
((("someone" "likes" "bear" "+")) -> ("someone" "eats" "squirrel" "+"))
The bear is red.
True
1
proof
[(triple3)]
("bear" "is" "red" "+")
triple3
The cat is not round.
False
1
inv-proof
[(triple5)]
("cat" "is" "round" "-")
triple5
The squirrel does not eat the lion.
True
2
proof
[(((triple9) -> rule5))]
("squirrel" "eats" "lion" "-")
((triple9) -> (rule5 % int1))
The squirrel does not eat the lion.
("squirrel" "eats" "lion" "-")
int1
The bear eats the lion.
False
2
inv-proof
[(((triple1) -> rule5))]
("bear" "eats" "lion" "+")
((triple1) -> (rule5 % int1))
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int1
The cat eats the squirrel.
True
3
proof
[(((((triple5) -> rule7)) -> rule8))]
("cat" "eats" "squirrel" "+")
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat does not eat the squirrel.
False
3
inv-proof
[(((((triple5) -> rule7)) -> rule8))]
("cat" "eats" "squirrel" "-")
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The cat does not see the squirrel.
Unknown
inv-rconc
[@1: The cat sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "squirrel" "-")
The bear likes the bear.
Unknown
rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "likes" "bear" "+")
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "blue" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
@0: The bear eats the cat.[(triple1)] The bear is kind.[(triple2)] The bear is red.[(triple3)] The bear likes the cat.[(triple4)] The cat is round.[(triple5)] The cat sees the bear.[(triple6)] The lion is big.[(triple7)] The lion likes the cat.[(triple8)] The squirrel does not like the cat.[(triple12)] The squirrel eats the cat.[(triple9)] The squirrel is red.[(triple10)] The squirrel likes the bear.[(triple11)] @1: The bear does not eat the lion.[(((triple1) -> rule5))] The cat likes the bear.[(((triple5) -> rule7))] The squirrel does not eat the lion.[(((triple9) -> rule5))] The squirrel eats the squirrel.[(((triple11) -> rule8))] @2: The cat eats the squirrel.[(((((triple5) -> rule7)) -> rule8))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear likes the cat.
("bear" "likes" "cat" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat sees the bear.
("cat" "sees" "bear" "+")
triple6
The lion is big.
("lion" "is" "big" "+")
triple7
The lion likes the cat.
("lion" "likes" "cat" "+")
triple8
The squirrel does not like the cat.
("squirrel" "likes" "cat" "-")
triple12
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple9
The squirrel is red.
("squirrel" "is" "red" "+")
triple10
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple11
The bear does not eat the lion.
("bear" "eats" "lion" "-")
((triple1) -> (rule5 % int1))
The bear does not eat the lion.
("bear" "eats" "lion" "-")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
((triple5) -> (rule7 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The squirrel does not eat the lion.
("squirrel" "eats" "lion" "-")
((triple9) -> (rule5 % int1))
The squirrel does not eat the lion.
("squirrel" "eats" "lion" "-")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple11) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2