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