The bear is rough. The mouse likes the bear. The squirrel likes the mouse. If someone eats the bear then the bear is red. If someone likes the bear then they are blue. If someone is cold and red then they like the squirrel.
The bear is rough.
("bear" "is" "rough" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If someone eats the bear then the bear is red.
((("someone" "eats" "bear" "+")) -> ("bear" "is" "red" "+"))
If someone likes the bear then they are blue.
((("someone" "likes" "bear" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold and red then they like the squirrel.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "likes" "squirrel" "+"))
The bear is rough.
True
1
proof
[(triple1)]
("bear" "is" "rough" "+")
triple1
The squirrel does not like the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "likes" "mouse" "-")
triple3
The mouse does not like the squirrel.
Unknown
inv-rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "squirrel" "-")
The bear eats the squirrel.
Unknown
random
[@0: The bear eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "squirrel" "+")
@0: The bear is rough.[(triple1)] The mouse likes the bear.[(triple2)] The squirrel likes the mouse.[(triple3)] @1: The mouse is blue.[(((triple2) -> rule2))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
((triple2) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1