The bear sees the squirrel. The cat likes the bear. The mouse is rough. The squirrel sees the bear. If someone is nice and they like the squirrel then they see the cat. If someone is red and they see the cat then the cat sees the squirrel. All kind people are young.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone is nice and they like the squirrel then they see the cat.
((("someone" "is" "nice" "+") ("someone" "likes" "squirrel" "+")) -> ("someone" "sees" "cat" "+"))
If someone is red and they see the cat then the cat sees the squirrel.
((("someone" "is" "red" "+") ("someone" "sees" "cat" "+")) -> ("cat" "sees" "squirrel" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
The bear sees the squirrel.
True
1
proof
[(triple1)]
("bear" "sees" "squirrel" "+")
triple1
The cat does not like the bear.
False
1
inv-proof
[(triple2)]
("cat" "likes" "bear" "-")
triple2
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "young" "-")
The cat sees the mouse.
Unknown
random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "+")
@0: The bear sees the squirrel.[(triple1)] The cat likes the bear.[(triple2)] The mouse is rough.[(triple3)] The squirrel sees the bear.[(triple4)]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The cat likes the bear.
("cat" "likes" "bear" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple4