The bear eats the mouse. The bear eats the squirrel. The bear visits the rabbit. The bear visits the squirrel. The mouse is blue. The mouse is green. The mouse is rough. The mouse needs the bear. The mouse needs the rabbit. The mouse visits the squirrel. The rabbit eats the bear. The rabbit eats the mouse. The rabbit is blue. The rabbit needs the squirrel. The rabbit visits the bear. The squirrel eats the mouse. If something needs the rabbit then the rabbit eats the bear. If the mouse eats the squirrel then the mouse is blue.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
If something needs the rabbit then the rabbit eats the bear.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "eats" "bear" "+"))
If the mouse eats the squirrel then the mouse is blue.
((("mouse" "eats" "squirrel" "+")) -> ("mouse" "is" "blue" "+"))
The bear eats the mouse.
True
1
proof
[(triple1)]
("bear" "eats" "mouse" "+")
triple1
The rabbit is not blue.
False
1
inv-proof
[(triple13)]
("rabbit" "is" "blue" "-")
triple13
The bear does not need the mouse.
Unknown
inv-random
[@0: The bear needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "mouse" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The bear eats the mouse.[(triple1)] The bear eats the squirrel.[(triple2)] The bear visits the rabbit.[(triple3)] The bear visits the squirrel.[(triple4)] The mouse is blue.[(triple5)] The mouse is green.[(triple6)] The mouse is rough.[(triple7)] The mouse needs the bear.[(triple8)] The mouse needs the rabbit.[(triple9)] The mouse visits the squirrel.[(triple10)] The rabbit eats the bear.[(triple11 OR ((triple9) -> rule1))] The rabbit eats the mouse.[(triple12)] The rabbit is blue.[(triple13)] The rabbit needs the squirrel.[(triple14)] The rabbit visits the bear.[(triple15)] The squirrel eats the mouse.[(triple16)]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple2
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple3
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple8
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple9
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple10
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple11
((triple9) -> (rule1 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple12
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple13
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple14
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple15
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple16