The rabbit is blue. The rabbit is not nice. The rabbit is not red. The rabbit is round. The rabbit is young. The rabbit likes the squirrel. The rabbit needs the squirrel. The rabbit visits the squirrel. The squirrel is blue. The squirrel is nice. The squirrel is red. The squirrel is round. The squirrel is young. The squirrel likes the rabbit. The squirrel needs the rabbit. The squirrel visits the rabbit. If something is blue and it needs the squirrel then it is round. If something likes the rabbit and it is blue then it needs the rabbit. If something likes the squirrel and the squirrel visits the rabbit then the rabbit likes the squirrel. If the rabbit is young and the rabbit does not need the squirrel then the squirrel visits the rabbit. If something visits the rabbit then it is blue. If something needs the squirrel then it likes the rabbit. If the squirrel is not blue then the squirrel is red. If the squirrel does not visit the rabbit then the rabbit visits the squirrel.
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit is not red.
("rabbit" "is" "red" "-")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If something is blue and it needs the squirrel then it is round.
((("something" "is" "blue" "+") ("something" "needs" "squirrel" "+")) -> ("something" "is" "round" "+"))
If something likes the rabbit and it is blue then it needs the rabbit.
((("something" "likes" "rabbit" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "rabbit" "+"))
If something likes the squirrel and the squirrel visits the rabbit then the rabbit likes the squirrel.
((("something" "likes" "squirrel" "+") ("squirrel" "visits" "rabbit" "+")) -> ("rabbit" "likes" "squirrel" "+"))
If the rabbit is young and the rabbit does not need the squirrel then the squirrel visits the rabbit.
((("rabbit" "is" "young" "+") ("rabbit" "needs" "squirrel" "~")) -> ("squirrel" "visits" "rabbit" "+"))
If something visits the rabbit then it is blue.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "blue" "+"))
If something needs the squirrel then it likes the rabbit.
((("something" "needs" "squirrel" "+")) -> ("something" "likes" "rabbit" "+"))
If the squirrel is not blue then the squirrel is red.
((("squirrel" "is" "blue" "~")) -> ("squirrel" "is" "red" "+"))
If the squirrel does not visit the rabbit then the rabbit visits the squirrel.
((("squirrel" "visits" "rabbit" "~")) -> ("rabbit" "visits" "squirrel" "+"))
The rabbit is not nice.
True
1
proof
[(triple2)]
("rabbit" "is" "nice" "-")
triple2
The squirrel is not round.
False
1
inv-proof
[(triple12)]
("squirrel" "is" "round" "-")
triple12
The rabbit likes the rabbit.
True
2
proof
[(((triple7) -> rule6))]
("rabbit" "likes" "rabbit" "+")
((triple7) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple7) -> rule6))]
("rabbit" "likes" "rabbit" "-")
((triple7) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit needs the rabbit.
True
4
proof
[(((((triple7) -> rule6) triple1) -> rule2))]
("rabbit" "needs" "rabbit" "+")
((((triple7) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit does not need the rabbit.
False
4
inv-proof
[(((((triple7) -> rule6) triple1) -> rule2))]
("rabbit" "needs" "rabbit" "-")
((((triple7) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
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 visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The rabbit is blue.[(triple1)] The rabbit is not nice.[(triple2)] The rabbit is not red.[(triple3)] The rabbit is round.[(triple4 OR ((triple1 triple7) -> rule1))] The rabbit is young.[(triple5)] The rabbit likes the squirrel.[(triple6)] The rabbit needs the squirrel.[(triple7)] The rabbit visits the squirrel.[(triple8)] The squirrel is blue.[(triple9 OR ((triple16) -> rule5))] The squirrel is nice.[(triple10)] The squirrel is red.[(triple11)] The squirrel is round.[(triple12)] The squirrel is young.[(triple13)] The squirrel likes the rabbit.[(triple14)] The squirrel needs the rabbit.[(triple15 OR ((triple14 triple9) -> rule2) OR ((triple14 ((triple16) -> rule5)) -> rule2))] The squirrel visits the rabbit.[(triple16)] @1: The rabbit likes the rabbit.[(((triple7) -> rule6))] @2: The rabbit needs the rabbit.[(((((triple7) -> rule6) triple1) -> rule2))]
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple1
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple2
The rabbit is not red.
("rabbit" "is" "red" "-")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
((triple1 triple7) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
triple5
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple6
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple7
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple8
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple9
((triple16) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple10
The squirrel is red.
("squirrel" "is" "red" "+")
triple11
The squirrel is round.
("squirrel" "is" "round" "+")
triple12
The squirrel is young.
("squirrel" "is" "young" "+")
triple13
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple14
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple15
((triple14 triple9) -> (rule2 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
((triple14 ((triple16) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple16
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple7) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple7) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2