The bear is red. The lion chases the squirrel. The mouse chases the squirrel. The squirrel sees the bear. If someone sees the mouse then they are kind. If someone likes the squirrel and they chase the squirrel then they are round. If someone likes the mouse and the mouse likes the lion then the mouse chases the lion.
The bear is red.
("bear" "is" "red" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone sees the mouse then they are kind.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "kind" "+"))
If someone likes the squirrel and they chase the squirrel then they are round.
((("someone" "likes" "squirrel" "+") ("someone" "chases" "squirrel" "+")) -> ("someone" "is" "round" "+"))
If someone likes the mouse and the mouse likes the lion then the mouse chases the lion.
((("someone" "likes" "mouse" "+") ("mouse" "likes" "lion" "+")) -> ("mouse" "chases" "lion" "+"))
The squirrel sees the bear.
True
1
proof
[(triple4)]
("squirrel" "sees" "bear" "+")
triple4
The mouse does not chase the squirrel.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "squirrel" "-")
triple3
The lion is not round.
Unknown
inv-rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "round" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The bear is red.[(triple1)] The lion chases the squirrel.[(triple2)] The mouse chases the squirrel.[(triple3)] The squirrel sees the bear.[(triple4)]
The bear is red.
("bear" "is" "red" "+")
triple1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple2
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple3
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple4