The bear eats the cat. The bear eats the squirrel. The bear needs the squirrel. The bear sees the cat. The cat eats the bear. The cat eats the squirrel. The cat is blue. The cat is cold. The cat needs the squirrel. The cat sees the squirrel. The squirrel eats the bear. The squirrel is big. The squirrel is cold. The squirrel needs the cat. The squirrel sees the cat. If someone eats the cat then they see the squirrel. If someone is round then they see the cat. If someone sees the bear and they are young then they eat the bear. If someone is young then they see the cat. If someone needs the bear then they eat the cat. If someone needs the squirrel and they eat the squirrel then the squirrel needs the bear.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If someone eats the cat then they see the squirrel.
((("someone" "eats" "cat" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is round then they see the cat.
((("someone" "is" "round" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the bear and they are young then they eat the bear.
((("someone" "sees" "bear" "+") ("someone" "is" "young" "+")) -> ("someone" "eats" "bear" "+"))
If someone is young then they see the cat.
((("someone" "is" "young" "+")) -> ("someone" "sees" "cat" "+"))
If someone needs the bear then they eat the cat.
((("someone" "needs" "bear" "+")) -> ("someone" "eats" "cat" "+"))
If someone needs the squirrel and they eat the squirrel then the squirrel needs the bear.
((("someone" "needs" "squirrel" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "needs" "bear" "+"))
The cat needs the squirrel.
True
1
proof
[(triple9)]
("cat" "needs" "squirrel" "+")
triple9
The bear does not need the squirrel.
False
1
inv-proof
[(triple3)]
("bear" "needs" "squirrel" "-")
triple3
The squirrel needs the bear.
True
3
proof
[(((triple3 triple2) -> rule6) OR ((triple9 triple6) -> rule6))]
("squirrel" "needs" "bear" "+")
((triple3 triple2) -> (rule6 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
((triple9 triple6) -> (rule6 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel does not need the bear.
False
3
inv-proof
[(((triple3 triple2) -> rule6) OR ((triple9 triple6) -> rule6))]
("squirrel" "needs" "bear" "-")
((triple3 triple2) -> (rule6 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
((triple9 triple6) -> (rule6 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel eats the cat.
True
4
proof
[(((((triple3 triple2) -> rule6)) -> rule5) OR ((((triple9 triple6) -> rule6)) -> rule5))]
("squirrel" "eats" "cat" "+")
((((triple3 triple2) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
((((triple9 triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel does not eat the cat.
False
4
inv-proof
[(((((triple3 triple2) -> rule6)) -> rule5) OR ((((triple9 triple6) -> rule6)) -> rule5))]
("squirrel" "eats" "cat" "-")
((((triple3 triple2) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
((((triple9 triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel sees the squirrel.
True
5
proof
[(((((((triple3 triple2) -> rule6)) -> rule5)) -> rule1) OR ((((((triple9 triple6) -> rule6)) -> rule5)) -> rule1))]
("squirrel" "sees" "squirrel" "+")
((((((triple3 triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
((((((triple9 triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
The squirrel does not see the squirrel.
False
5
inv-proof
[(((((((triple3 triple2) -> rule6)) -> rule5)) -> rule1) OR ((((((triple9 triple6) -> rule6)) -> rule5)) -> rule1))]
("squirrel" "sees" "squirrel" "-")
((((((triple3 triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
((((((triple9 triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "eats" "bear" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "cat" "+")
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "cat" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The bear eats the cat.[(triple1)] The bear eats the squirrel.[(triple2)] The bear needs the squirrel.[(triple3)] The bear sees the cat.[(triple4)] The cat eats the bear.[(triple5)] The cat eats the squirrel.[(triple6)] The cat is blue.[(triple7)] The cat is cold.[(triple8)] The cat needs the squirrel.[(triple9)] The cat sees the squirrel.[(triple10)] The squirrel eats the bear.[(triple11)] The squirrel is big.[(triple12)] The squirrel is cold.[(triple13)] The squirrel needs the cat.[(triple14)] The squirrel sees the cat.[(triple15)] @1: The bear sees the squirrel.[(((triple1) -> rule1))] The squirrel needs the bear.[(((triple3 triple2) -> rule6) OR ((triple9 triple6) -> rule6))] @2: The squirrel eats the cat.[(((((triple3 triple2) -> rule6)) -> rule5) OR ((((triple9 triple6) -> rule6)) -> rule5))] @3: The squirrel sees the squirrel.[(((((((triple3 triple2) -> rule6)) -> rule5)) -> rule1) OR ((((((triple9 triple6) -> rule6)) -> rule5)) -> rule1))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple3
The bear sees the cat.
("bear" "sees" "cat" "+")
triple4
The cat eats the bear.
("cat" "eats" "bear" "+")
triple5
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple6
The cat is blue.
("cat" "is" "blue" "+")
triple7
The cat is cold.
("cat" "is" "cold" "+")
triple8
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple9
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple10
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple11
The squirrel is big.
("squirrel" "is" "big" "+")
triple12
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple13
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple14
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple15
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((triple1) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
((triple3 triple2) -> (rule6 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
((triple9 triple6) -> (rule6 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((((triple3 triple2) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
((((triple9 triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((((triple3 triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
((((((triple9 triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3