The bear needs the mouse. The mouse sees the bear. The rabbit needs the bear. The squirrel likes the bear. If something sees the squirrel then it sees the bear.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
If something sees the squirrel then it sees the bear.
((("something" "sees" "squirrel" "+")) -> ("something" "sees" "bear" "+"))
The bear needs the mouse.
True
1
proof
[(triple1)]
("bear" "needs" "mouse" "+")
triple1
The squirrel does not like the bear.
False
1
inv-proof
[(triple4)]
("squirrel" "likes" "bear" "-")
triple4
The squirrel does not see the bear.
Unknown
inv-rconc
[@1: The squirrel sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "bear" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The bear needs the mouse.[(triple1)] The mouse sees the bear.[(triple2)] The rabbit needs the bear.[(triple3)] The squirrel likes the bear.[(triple4)]
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple3
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple4