The bear is red. The bear needs the mouse. The bear needs the squirrel. The cat visits the bear. The mouse likes the bear. The mouse likes the cat. The squirrel is nice. The squirrel is red. The squirrel likes the mouse. The squirrel needs the mouse. If the bear likes the mouse and the bear visits the mouse then the bear visits the squirrel. All round things are nice. If the cat is round then the cat likes the bear. If something needs the cat then the cat is kind. If something is red then it needs the squirrel. Round things are nice.
The bear is red.
("bear" "is" "red" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If the bear likes the mouse and the bear visits the mouse then the bear visits the squirrel.
((("bear" "likes" "mouse" "+") ("bear" "visits" "mouse" "+")) -> ("bear" "visits" "squirrel" "+"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If the cat is round then the cat likes the bear.
((("cat" "is" "round" "+")) -> ("cat" "likes" "bear" "+"))
If something needs the cat then the cat is kind.
((("something" "needs" "cat" "+")) -> ("cat" "is" "kind" "+"))
If something is red then it needs the squirrel.
((("something" "is" "red" "+")) -> ("something" "needs" "squirrel" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
The bear needs the squirrel.
True
1
proof
[(triple3 OR ((triple1) -> rule5))]
("bear" "needs" "squirrel" "+")
triple3
((triple1) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The squirrel is not red.
False
1
inv-proof
[(triple8)]
("squirrel" "is" "red" "-")
triple8
The squirrel needs the squirrel.
True
2
proof
[(((triple8) -> rule5))]
("squirrel" "needs" "squirrel" "+")
((triple8) -> (rule5 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel does not need the squirrel.
False
2
inv-proof
[(((triple8) -> rule5))]
("squirrel" "needs" "squirrel" "-")
((triple8) -> (rule5 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The cat does not need the squirrel.
Unknown
inv-rconc
[@1: The cat needs the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "needs" "squirrel" "-")
The bear visits the squirrel.
Unknown
rconc
[@1: The bear visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "squirrel" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The cat needs the mouse.
Unknown
random
[@0: The cat needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "mouse" "+")
@0: The bear is red.[(triple1)] The bear needs the mouse.[(triple2)] The bear needs the squirrel.[(triple3 OR ((triple1) -> rule5))] The cat visits the bear.[(triple4)] The mouse likes the bear.[(triple5)] The mouse likes the cat.[(triple6)] The squirrel is nice.[(triple7)] The squirrel is red.[(triple8)] The squirrel likes the mouse.[(triple9)] The squirrel needs the mouse.[(triple10)] @1: The squirrel needs the squirrel.[(((triple8) -> rule5))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple3
((triple1) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
triple4
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple5
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple6
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple9
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple10
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple8) -> (rule5 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1