The bear eats the squirrel. The bear is cold. The bear is green. The bear likes the squirrel. The bear needs the squirrel. The squirrel eats the bear. The squirrel is blue. The squirrel is cold. The squirrel is green. The squirrel is kind. The squirrel likes the bear. The squirrel needs the bear. If something likes the squirrel and it needs the squirrel then the squirrel likes the bear. If something likes the squirrel and it likes the bear then the squirrel is kind. If something needs the squirrel and it needs the bear then it is kind. If the bear needs the squirrel and the bear likes the squirrel then the bear is green. If something likes the bear and the bear needs the squirrel then it eats the bear. If something likes the bear then the bear eats the squirrel. If something is blue then it needs the bear. If something eats the bear and the bear is cold then the bear is blue.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The squirrel eats the bear.
("squirrel" "eats" "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 likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If something likes the squirrel and it needs the squirrel then the squirrel likes the bear.
((("something" "likes" "squirrel" "+") ("something" "needs" "squirrel" "+")) -> ("squirrel" "likes" "bear" "+"))
If something likes the squirrel and it likes the bear then the squirrel is kind.
((("something" "likes" "squirrel" "+") ("something" "likes" "bear" "+")) -> ("squirrel" "is" "kind" "+"))
If something needs the squirrel and it needs the bear then it is kind.
((("something" "needs" "squirrel" "+") ("something" "needs" "bear" "+")) -> ("something" "is" "kind" "+"))
If the bear needs the squirrel and the bear likes the squirrel then the bear is green.
((("bear" "needs" "squirrel" "+") ("bear" "likes" "squirrel" "+")) -> ("bear" "is" "green" "+"))
If something likes the bear and the bear needs the squirrel then it eats the bear.
((("something" "likes" "bear" "+") ("bear" "needs" "squirrel" "+")) -> ("something" "eats" "bear" "+"))
If something likes the bear then the bear eats the squirrel.
((("something" "likes" "bear" "+")) -> ("bear" "eats" "squirrel" "+"))
If something is blue then it needs the bear.
((("something" "is" "blue" "+")) -> ("something" "needs" "bear" "+"))
If something eats the bear and the bear is cold then the bear is blue.
((("something" "eats" "bear" "+") ("bear" "is" "cold" "+")) -> ("bear" "is" "blue" "+"))
The squirrel is green.
True
1
proof
[(triple9)]
("squirrel" "is" "green" "+")
triple9
The squirrel is not kind.
False
1
inv-proof
[(triple10)]
("squirrel" "is" "kind" "-")
triple10
The bear is blue.
True
3
proof
[(((triple6 triple2) -> rule8) OR ((((triple11 triple5) -> rule5) triple2) -> rule8) OR ((((((triple4 triple5) -> rule1) triple5) -> rule5) triple2) -> rule8))]
("bear" "is" "blue" "+")
((triple6 triple2) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((((triple11 triple5) -> (rule5 % int2)) triple2) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
((((((triple4 triple5) -> (rule1 % int3)) triple5) -> (rule5 % int2)) triple2) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The bear is not blue.
False
3
inv-proof
[(((triple6 triple2) -> rule8) OR ((((triple11 triple5) -> rule5) triple2) -> rule8) OR ((((((triple4 triple5) -> rule1) triple5) -> rule5) triple2) -> rule8))]
("bear" "is" "blue" "-")
((triple6 triple2) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((((triple11 triple5) -> (rule5 % int2)) triple2) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
((((((triple4 triple5) -> (rule1 % int3)) triple5) -> (rule5 % int2)) triple2) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The bear needs the bear.
True
4
proof
[(((((triple6 triple2) -> rule8)) -> rule7) OR ((((((triple11 triple5) -> rule5) triple2) -> rule8)) -> rule7) OR ((((((((triple4 triple5) -> rule1) triple5) -> rule5) triple2) -> rule8)) -> rule7))]
("bear" "needs" "bear" "+")
((((triple6 triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((((triple11 triple5) -> (rule5 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int3
((((((((triple4 triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int4
The bear does not need the bear.
False
4
inv-proof
[(((((triple6 triple2) -> rule8)) -> rule7) OR ((((((triple11 triple5) -> rule5) triple2) -> rule8)) -> rule7) OR ((((((((triple4 triple5) -> rule1) triple5) -> rule5) triple2) -> rule8)) -> rule7))]
("bear" "needs" "bear" "-")
((((triple6 triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((((triple11 triple5) -> (rule5 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int3
((((((((triple4 triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int4
The bear is kind.
True
6
proof
[(((triple5 ((((triple6 triple2) -> rule8)) -> rule7)) -> rule3) OR ((triple5 ((((((triple11 triple5) -> rule5) triple2) -> rule8)) -> rule7)) -> rule3) OR ((triple5 ((((((((triple4 triple5) -> rule1) triple5) -> rule5) triple2) -> rule8)) -> rule7)) -> rule3))]
("bear" "is" "kind" "+")
((triple5 ((((triple6 triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((triple5 ((((((triple11 triple5) -> (rule5 % int4)) triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int4
((triple5 ((((((((triple4 triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4)) triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int4
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int5
The bear is not kind.
False
6
inv-proof
[(((triple5 ((((triple6 triple2) -> rule8)) -> rule7)) -> rule3) OR ((triple5 ((((((triple11 triple5) -> rule5) triple2) -> rule8)) -> rule7)) -> rule3) OR ((triple5 ((((((((triple4 triple5) -> rule1) triple5) -> rule5) triple2) -> rule8)) -> rule7)) -> rule3))]
("bear" "is" "kind" "-")
((triple5 ((((triple6 triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((triple5 ((((((triple11 triple5) -> (rule5 % int4)) triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int4
((triple5 ((((((((triple4 triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4)) triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int4
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int5
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "bear" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bear eats the squirrel.[(triple1 OR ((triple11) -> rule6) OR ((((triple4 triple5) -> rule1)) -> rule6))] The bear is cold.[(triple2)] The bear is green.[(triple3 OR ((triple5 triple4) -> rule4))] The bear likes the squirrel.[(triple4)] The bear needs the squirrel.[(triple5)] The squirrel eats the bear.[(triple6 OR ((triple11 triple5) -> rule5) OR ((((triple4 triple5) -> rule1) triple5) -> rule5))] The squirrel is blue.[(triple7)] The squirrel is cold.[(triple8)] The squirrel is green.[(triple9)] The squirrel is kind.[(triple10)] The squirrel likes the bear.[(triple11 OR ((triple4 triple5) -> rule1))] The squirrel needs the bear.[(triple12 OR ((triple7) -> rule7))] @1: The bear is blue.[(((triple6 triple2) -> rule8) OR ((((triple11 triple5) -> rule5) triple2) -> rule8) OR ((((((triple4 triple5) -> rule1) triple5) -> rule5) triple2) -> rule8))] @2: The bear needs the bear.[(((((triple6 triple2) -> rule8)) -> rule7) OR ((((((triple11 triple5) -> rule5) triple2) -> rule8)) -> rule7) OR ((((((((triple4 triple5) -> rule1) triple5) -> rule5) triple2) -> rule8)) -> rule7))] @3: The bear is kind.[(((triple5 ((((triple6 triple2) -> rule8)) -> rule7)) -> rule3) OR ((triple5 ((((((triple11 triple5) -> rule5) triple2) -> rule8)) -> rule7)) -> rule3) OR ((triple5 ((((((((triple4 triple5) -> rule1) triple5) -> rule5) triple2) -> rule8)) -> rule7)) -> rule3))]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
((triple11) -> (rule6 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
((((triple4 triple5) -> (rule1 % int2))) -> (rule6 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
((triple5 triple4) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple4
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple5
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple6
((triple11 triple5) -> (rule5 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
((((triple4 triple5) -> (rule1 % int2)) triple5) -> (rule5 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel is green.
("squirrel" "is" "green" "+")
triple9
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple11
((triple4 triple5) -> (rule1 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple12
((triple7) -> (rule7 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
((triple6 triple2) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((((triple11 triple5) -> (rule5 % int2)) triple2) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
((((((triple4 triple5) -> (rule1 % int3)) triple5) -> (rule5 % int2)) triple2) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
((((triple6 triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((((triple11 triple5) -> (rule5 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int3
((((((((triple4 triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int4
The bear is kind.
("bear" "is" "kind" "+")
((triple5 ((((triple6 triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((triple5 ((((((triple11 triple5) -> (rule5 % int4)) triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int4
((triple5 ((((((((triple4 triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4)) triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int4
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int5