The bear eats the squirrel. The bear likes the lion. The bear needs the mouse. The lion does not eat the bear. The lion eats the squirrel. The lion is nice. The lion is not red. The lion does not like the mouse. The lion likes the squirrel. The lion needs the bear. The lion needs the mouse. The mouse is young. The mouse does not like the bear. The mouse likes the lion. The mouse needs the bear. The squirrel eats the bear. If the bear is young and the bear does not eat the mouse then the mouse needs the bear. If someone is young then they do not need the squirrel. If someone is young and they do not need the squirrel then the squirrel is not red.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The lion does not eat the bear.
("lion" "eats" "bear" "-")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is not red.
("lion" "is" "red" "-")
The lion does not like the mouse.
("lion" "likes" "mouse" "-")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
If the bear is young and the bear does not eat the mouse then the mouse needs the bear.
((("bear" "is" "young" "+") ("bear" "eats" "mouse" "~")) -> ("mouse" "needs" "bear" "+"))
If someone is young then they do not need the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "needs" "squirrel" "-"))
If someone is young and they do not need the squirrel then the squirrel is not red.
((("someone" "is" "young" "+") ("someone" "needs" "squirrel" "~")) -> ("squirrel" "is" "red" "-"))
The squirrel eats the bear.
True
1
proof
[(triple16)]
("squirrel" "eats" "bear" "+")
triple16
The lion eats the bear.
False
1
inv-proof
[(triple4)]
("lion" "eats" "bear" "+")
triple4
The mouse does not need the squirrel.
True
2
proof
[(((triple12) -> rule2))]
("mouse" "needs" "squirrel" "-")
((triple12) -> (rule2 % int1))
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
int1
The mouse needs the squirrel.
False
2
inv-proof
[(((triple12) -> rule2))]
("mouse" "needs" "squirrel" "+")
((triple12) -> (rule2 % int1))
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
int1
The squirrel is not red.
True
4
proof
[(((triple12 ((triple12) -> rule2)) -> rule3))]
("squirrel" "is" "red" "-")
((triple12 ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
int2
The squirrel is red.
False
4
inv-proof
[(((triple12 ((triple12) -> rule2)) -> rule3))]
("squirrel" "is" "red" "+")
((triple12 ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
int2
The mouse does not eat the squirrel.
Unknown
inv-random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "-")
The bear likes the squirrel.
Unknown
random
[@0: The bear likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "squirrel" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The squirrel likes the mouse.
Unknown
random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The squirrel likes the bear.
Unknown
random
[@0: The squirrel likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "bear" "+")
@0: The bear eats the squirrel.[(triple1)] The bear likes the lion.[(triple2)] The bear needs the mouse.[(triple3)] The lion does not eat the bear.[(triple4)] The lion does not like the mouse.[(triple8)] The lion eats the squirrel.[(triple5)] The lion is nice.[(triple6)] The lion is not red.[(triple7)] The lion likes the squirrel.[(triple9)] The lion needs the bear.[(triple10)] The lion needs the mouse.[(triple11)] The mouse does not like the bear.[(triple13)] The mouse is young.[(triple12)] The mouse likes the lion.[(triple14)] The mouse needs the bear.[(triple15)] The squirrel eats the bear.[(triple16)] @1: The mouse does not need the squirrel.[(((triple12) -> rule2))] @2: The squirrel is not red.[(((triple12 ((triple12) -> rule2)) -> rule3))]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The bear likes the lion.
("bear" "likes" "lion" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The lion does not eat the bear.
("lion" "eats" "bear" "-")
triple4
The lion does not like the mouse.
("lion" "likes" "mouse" "-")
triple8
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple5
The lion is nice.
("lion" "is" "nice" "+")
triple6
The lion is not red.
("lion" "is" "red" "-")
triple7
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple9
The lion needs the bear.
("lion" "needs" "bear" "+")
triple10
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple11
The mouse does not like the bear.
("mouse" "likes" "bear" "-")
triple13
The mouse is young.
("mouse" "is" "young" "+")
triple12
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple14
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple15
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple16
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
((triple12) -> (rule2 % int1))
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
int1
The squirrel is not red.
("squirrel" "is" "red" "-")
((triple12 ((triple12) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
int2