The bear is green. The bear is kind. The bear is rough. The bear needs the mouse. The lion chases the mouse. The lion chases the squirrel. The lion needs the mouse. The mouse chases the squirrel. The squirrel chases the bear. The squirrel chases the mouse. If someone eats the bear then the bear is green. If the bear is kind then the bear needs the squirrel. If someone chases the mouse and the mouse chases the squirrel then they are blue.
The bear is green.
("bear" "is" "green" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
If someone eats the bear then the bear is green.
((("someone" "eats" "bear" "+")) -> ("bear" "is" "green" "+"))
If the bear is kind then the bear needs the squirrel.
((("bear" "is" "kind" "+")) -> ("bear" "needs" "squirrel" "+"))
If someone chases the mouse and the mouse chases the squirrel then they are blue.
((("someone" "chases" "mouse" "+") ("mouse" "chases" "squirrel" "+")) -> ("someone" "is" "blue" "+"))
The lion chases the mouse.
True
1
proof
[(triple5)]
("lion" "chases" "mouse" "+")
triple5
The bear is not kind.
False
1
inv-proof
[(triple2)]
("bear" "is" "kind" "-")
triple2
The bear needs the squirrel.
True
2
proof
[(((triple2) -> rule2))]
("bear" "needs" "squirrel" "+")
((triple2) -> (rule2 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The squirrel is not blue.
False
3
inv-proof
[(((triple10 triple8) -> rule3))]
("squirrel" "is" "blue" "-")
((triple10 triple8) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "blue" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "blue" "+")
The bear does not chase the mouse.
Unknown
inv-random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "-")
The mouse chases the bear.
Unknown
random
[@0: The mouse chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bear" "+")
@0: The bear is green.[(triple1)] The bear is kind.[(triple2)] The bear is rough.[(triple3)] The bear needs the mouse.[(triple4)] The lion chases the mouse.[(triple5)] The lion chases the squirrel.[(triple6)] The lion needs the mouse.[(triple7)] The mouse chases the squirrel.[(triple8)] The squirrel chases the bear.[(triple9)] The squirrel chases the mouse.[(triple10)] @1: The bear needs the squirrel.[(((triple2) -> rule2))] The lion is blue.[(((triple5 triple8) -> rule3))] The squirrel is blue.[(((triple10 triple8) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple4
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple5
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple7
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple8
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple9
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple10
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple2) -> (rule2 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((triple5 triple8) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple10 triple8) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1