The rabbit is cold. The rabbit is kind. The rabbit is red. The rabbit is rough. The rabbit likes the squirrel. The rabbit needs the squirrel. The rabbit sees the squirrel. The squirrel is kind. The squirrel is rough. The squirrel likes the rabbit. The squirrel needs the rabbit. The squirrel sees the rabbit. If someone is red then they need the rabbit.
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone is red then they need the rabbit.
((("someone" "is" "red" "+")) -> ("someone" "needs" "rabbit" "+"))
The squirrel is kind.
True
1
proof
[(triple8)]
("squirrel" "is" "kind" "+")
triple8
The squirrel does not like the rabbit.
False
1
inv-proof
[(triple10)]
("squirrel" "likes" "rabbit" "-")
triple10
The rabbit needs the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "needs" "rabbit" "+")
((triple3) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "needs" "rabbit" "-")
((triple3) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
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 is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The rabbit is cold.[(triple1)] The rabbit is kind.[(triple2)] The rabbit is red.[(triple3)] The rabbit is rough.[(triple4)] The rabbit likes the squirrel.[(triple5)] The rabbit needs the squirrel.[(triple6)] The rabbit sees the squirrel.[(triple7)] The squirrel is kind.[(triple8)] The squirrel is rough.[(triple9)] The squirrel likes the rabbit.[(triple10)] The squirrel needs the rabbit.[(triple11)] The squirrel sees the rabbit.[(triple12)] @1: The rabbit needs the rabbit.[(((triple3) -> rule1))]
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple2
The rabbit is red.
("rabbit" "is" "red" "+")
triple3
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple4
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple5
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple6
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple7
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple8
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple9
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple10
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple11
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple12
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple3) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1