The bear is round. The mouse likes the bear. The squirrel is rough. If something chases the squirrel and the squirrel likes the bear then it eats the squirrel. If something eats the squirrel then it is round.
The bear is round.
("bear" "is" "round" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If something chases the squirrel and the squirrel likes the bear then it eats the squirrel.
((("something" "chases" "squirrel" "+") ("squirrel" "likes" "bear" "+")) -> ("something" "eats" "squirrel" "+"))
If something eats the squirrel then it is round.
((("something" "eats" "squirrel" "+")) -> ("something" "is" "round" "+"))
The mouse likes the bear.
True
1
proof
[(triple2)]
("mouse" "likes" "bear" "+")
triple2
The mouse does not like the bear.
False
1
inv-proof
[(triple2)]
("mouse" "likes" "bear" "-")
triple2
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The bear is round.[(triple1)] The mouse likes the bear.[(triple2)] The squirrel is rough.[(triple3)]
The bear is round.
("bear" "is" "round" "+")
triple1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3