The bear is red. The bear likes the rabbit. The bear needs the squirrel. The bear does not visit the squirrel. The rabbit is kind. The rabbit does not like the squirrel. The rabbit visits the bear. The squirrel is big. The squirrel is red. The squirrel likes the rabbit. The squirrel needs the rabbit. The squirrel visits the rabbit. If something is big and it does not need the rabbit then it does not need the bear. If something needs the bear and it is not nice then the bear needs the squirrel. If the squirrel is not big then the squirrel does not like the bear. If the squirrel visits the bear and the bear is not kind then the squirrel likes the rabbit. If something is kind and it visits the bear then it is not blue. All nice, big things are not red.
The bear is red.
("bear" "is" "red" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit does not like the squirrel.
("rabbit" "likes" "squirrel" "-")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
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 big and it does not need the rabbit then it does not need the bear.
((("something" "is" "big" "+") ("something" "needs" "rabbit" "~")) -> ("something" "needs" "bear" "-"))
If something needs the bear and it is not nice then the bear needs the squirrel.
((("something" "needs" "bear" "+") ("something" "is" "nice" "~")) -> ("bear" "needs" "squirrel" "+"))
If the squirrel is not big then the squirrel does not like the bear.
((("squirrel" "is" "big" "~")) -> ("squirrel" "likes" "bear" "-"))
If the squirrel visits the bear and the bear is not kind then the squirrel likes the rabbit.
((("squirrel" "visits" "bear" "+") ("bear" "is" "kind" "~")) -> ("squirrel" "likes" "rabbit" "+"))
If something is kind and it visits the bear then it is not blue.
((("something" "is" "kind" "+") ("something" "visits" "bear" "+")) -> ("something" "is" "blue" "-"))
All nice, big things are not red.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "-"))
The squirrel is red.
True
1
proof
[(triple9)]
("squirrel" "is" "red" "+")
triple9
The squirrel does not need the rabbit.
False
1
inv-proof
[(triple11)]
("squirrel" "needs" "rabbit" "-")
triple11
The rabbit is not blue.
True
3
proof
[(((triple5 triple7) -> rule5))]
("rabbit" "is" "blue" "-")
((triple5 triple7) -> (rule5 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1
The rabbit is blue.
False
3
inv-proof
[(((triple5 triple7) -> rule5))]
("rabbit" "is" "blue" "+")
((triple5 triple7) -> (rule5 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The rabbit does not like the bear.
Unknown
inv-random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear does not visit the squirrel.[(triple4)] The bear is red.[(triple1)] The bear likes the rabbit.[(triple2)] The bear needs the squirrel.[(triple3)] The rabbit does not like the squirrel.[(triple6)] The rabbit is kind.[(triple5)] The rabbit visits the bear.[(triple7)] The squirrel is big.[(triple8)] The squirrel is red.[(triple9)] The squirrel likes the rabbit.[(triple10)] The squirrel needs the rabbit.[(triple11)] The squirrel visits the rabbit.[(triple12)] @1: The rabbit is not blue.[(((triple5 triple7) -> rule5))]
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
triple4
The bear is red.
("bear" "is" "red" "+")
triple1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple3
The rabbit does not like the squirrel.
("rabbit" "likes" "squirrel" "-")
triple6
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple10
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple11
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple12
The rabbit is not blue.
("rabbit" "is" "blue" "-")
((triple5 triple7) -> (rule5 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1