The rabbit eats the squirrel. The rabbit is green. The rabbit is kind. The rabbit is red. The rabbit is rough. The rabbit is young. The rabbit needs the squirrel. The rabbit sees the squirrel. The squirrel eats the rabbit. The squirrel is green. The squirrel is kind. The squirrel is red. The squirrel is rough. The squirrel is young. The squirrel needs the rabbit. The squirrel sees the rabbit. If someone needs the rabbit then the rabbit eats the squirrel. If someone sees the squirrel and the squirrel is red then they need the rabbit. If someone eats the squirrel then the squirrel sees the rabbit. If someone needs the rabbit then the rabbit is young. If someone sees the rabbit then the rabbit sees the squirrel. If someone needs the rabbit and they are green then they eat the rabbit.
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone needs the rabbit then the rabbit eats the squirrel.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "eats" "squirrel" "+"))
If someone sees the squirrel and the squirrel is red then they need the rabbit.
((("someone" "sees" "squirrel" "+") ("squirrel" "is" "red" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone eats the squirrel then the squirrel sees the rabbit.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "sees" "rabbit" "+"))
If someone needs the rabbit then the rabbit is young.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If someone sees the rabbit then the rabbit sees the squirrel.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If someone needs the rabbit and they are green then they eat the rabbit.
((("someone" "needs" "rabbit" "+") ("someone" "is" "green" "+")) -> ("someone" "eats" "rabbit" "+"))
The squirrel is rough.
True
1
proof
[(triple13)]
("squirrel" "is" "rough" "+")
triple13
The rabbit is not rough.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "rough" "-")
triple5
The rabbit needs the rabbit.
True
3
proof
[(((triple8 triple12) -> rule2) OR ((((triple16) -> rule5) triple12) -> rule2) OR ((((((triple1) -> rule3)) -> rule5) triple12) -> rule2) OR ((((((((triple15) -> rule1)) -> rule3)) -> rule5) triple12) -> rule2))]
("rabbit" "needs" "rabbit" "+")
((triple8 triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((((triple16) -> (rule5 % int2)) triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
((((((((triple15) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int4
The rabbit does not need the rabbit.
False
3
inv-proof
[(((triple8 triple12) -> rule2) OR ((((triple16) -> rule5) triple12) -> rule2) OR ((((((triple1) -> rule3)) -> rule5) triple12) -> rule2) OR ((((((((triple15) -> rule1)) -> rule3)) -> rule5) triple12) -> rule2))]
("rabbit" "needs" "rabbit" "-")
((triple8 triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((((triple16) -> (rule5 % int2)) triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
((((((((triple15) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int4
The rabbit eats the rabbit.
True
5
proof
[(((((triple8 triple12) -> rule2) triple2) -> rule6) OR ((((((triple16) -> rule5) triple12) -> rule2) triple2) -> rule6) OR ((((((((triple1) -> rule3)) -> rule5) triple12) -> rule2) triple2) -> rule6) OR ((((((((((triple15) -> rule1)) -> rule3)) -> rule5) triple12) -> rule2) triple2) -> rule6))]
("rabbit" "eats" "rabbit" "+")
((((triple8 triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
((((((triple16) -> (rule5 % int3)) triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
((((((((triple1) -> (rule3 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int4
((((((((((triple15) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int4
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int5
The rabbit does not eat the rabbit.
False
5
inv-proof
[(((((triple8 triple12) -> rule2) triple2) -> rule6) OR ((((((triple16) -> rule5) triple12) -> rule2) triple2) -> rule6) OR ((((((((triple1) -> rule3)) -> rule5) triple12) -> rule2) triple2) -> rule6) OR ((((((((((triple15) -> rule1)) -> rule3)) -> rule5) triple12) -> rule2) triple2) -> rule6))]
("rabbit" "eats" "rabbit" "-")
((((triple8 triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
((((((triple16) -> (rule5 % int3)) triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
((((((((triple1) -> (rule3 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int4
((((((((((triple15) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int4
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int5
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 squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The rabbit eats the squirrel.[(triple1 OR ((triple15) -> rule1) OR ((((triple8 triple12) -> rule2)) -> rule1) OR ((((((triple16) -> rule5) triple12) -> rule2)) -> rule1))] The rabbit is green.[(triple2)] The rabbit is kind.[(triple3)] The rabbit is red.[(triple4)] The rabbit is rough.[(triple5)] The rabbit is young.[(triple6 OR ((triple15) -> rule4) OR ((((triple8 triple12) -> rule2)) -> rule4) OR ((((((triple16) -> rule5) triple12) -> rule2)) -> rule4) OR ((((((((triple1) -> rule3)) -> rule5) triple12) -> rule2)) -> rule4) OR ((((((((((triple15) -> rule1)) -> rule3)) -> rule5) triple12) -> rule2)) -> rule4))] The rabbit needs the squirrel.[(triple7)] The rabbit sees the squirrel.[(triple8 OR ((triple16) -> rule5) OR ((((triple1) -> rule3)) -> rule5) OR ((((((triple15) -> rule1)) -> rule3)) -> rule5))] The squirrel eats the rabbit.[(triple9 OR ((triple15 triple10) -> rule6))] The squirrel is green.[(triple10)] The squirrel is kind.[(triple11)] The squirrel is red.[(triple12)] The squirrel is rough.[(triple13)] The squirrel is young.[(triple14)] The squirrel needs the rabbit.[(triple15)] The squirrel sees the rabbit.[(triple16 OR ((triple1) -> rule3) OR ((((triple15) -> rule1)) -> rule3) OR ((((((triple8 triple12) -> rule2)) -> rule1)) -> rule3))] @1: The rabbit needs the rabbit.[(((triple8 triple12) -> rule2) OR ((((triple16) -> rule5) triple12) -> rule2) OR ((((((triple1) -> rule3)) -> rule5) triple12) -> rule2) OR ((((((((triple15) -> rule1)) -> rule3)) -> rule5) triple12) -> rule2))] @2: The rabbit eats the rabbit.[(((((triple8 triple12) -> rule2) triple2) -> rule6) OR ((((((triple16) -> rule5) triple12) -> rule2) triple2) -> rule6) OR ((((((((triple1) -> rule3)) -> rule5) triple12) -> rule2) triple2) -> rule6) OR ((((((((((triple15) -> rule1)) -> rule3)) -> rule5) triple12) -> rule2) triple2) -> rule6))]
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple1
((triple15) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
((((triple8 triple12) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
((((((triple16) -> (rule5 % int3)) triple12) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit is red.
("rabbit" "is" "red" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
((triple15) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
((((triple8 triple12) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
((((((triple16) -> (rule5 % int3)) triple12) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
((((((((triple1) -> (rule3 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int4
((((((((((triple15) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int4
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int5
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple7
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple8
((triple16) -> (rule5 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
((((((triple15) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple9
((triple15 triple10) -> (rule6 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
triple10
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple11
The squirrel is red.
("squirrel" "is" "red" "+")
triple12
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple13
The squirrel is young.
("squirrel" "is" "young" "+")
triple14
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple15
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple16
((triple1) -> (rule3 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
((((((triple8 triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple8 triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((((triple16) -> (rule5 % int2)) triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
((((((((triple15) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int4
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple8 triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
((((((triple16) -> (rule5 % int3)) triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
((((((((triple1) -> (rule3 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int4
((((((((((triple15) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2)) triple2) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int4
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int5