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