The bear needs the mouse. The mouse needs the squirrel. The squirrel is young. If something visits the mouse and it needs the mouse then it visits the squirrel. If something visits the bear and it does not need the squirrel then it does not visit the squirrel. If the mouse needs the squirrel then the squirrel is round. If something is young then it sees the bear. All round things are cold. If the squirrel visits the mouse and the squirrel does not see the bear then the mouse is round.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If something visits the mouse and it needs the mouse then it visits the squirrel.
((("something" "visits" "mouse" "+") ("something" "needs" "mouse" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the bear and it does not need the squirrel then it does not visit the squirrel.
((("something" "visits" "bear" "+") ("something" "needs" "squirrel" "~")) -> ("something" "visits" "squirrel" "-"))
If the mouse needs the squirrel then the squirrel is round.
((("mouse" "needs" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
If something is young then it sees the bear.
((("something" "is" "young" "+")) -> ("something" "sees" "bear" "+"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If the squirrel visits the mouse and the squirrel does not see the bear then the mouse is round.
((("squirrel" "visits" "mouse" "+") ("squirrel" "sees" "bear" "~")) -> ("mouse" "is" "round" "+"))
The squirrel is young.
True
1
proof
[(triple3)]
("squirrel" "is" "young" "+")
triple3
The bear does not need the mouse.
False
1
inv-proof
[(triple1)]
("bear" "needs" "mouse" "-")
triple1
The squirrel sees the bear.
True
2
proof
[(((triple3) -> rule4))]
("squirrel" "sees" "bear" "+")
((triple3) -> (rule4 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel does not see the bear.
False
2
inv-proof
[(((triple3) -> rule4))]
("squirrel" "sees" "bear" "-")
((triple3) -> (rule4 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is cold.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("squirrel" "is" "cold" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is not cold.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("squirrel" "is" "cold" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "round" "-")
The mouse visits the squirrel.
Unknown
rconc
[@1: The mouse visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "squirrel" "+")
The mouse does not see the bear.
Unknown
inv-rconc
[@1: The mouse sees the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "bear" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear needs the mouse.[(triple1)] The mouse needs the squirrel.[(triple2)] The squirrel is young.[(triple3)] @1: The squirrel is round.[(((triple2) -> rule3))] The squirrel sees the bear.[(((triple3) -> rule4))] @2: The squirrel is cold.[(((((triple2) -> rule3)) -> rule5))]
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple2
The squirrel is young.
("squirrel" "is" "young" "+")
triple3
The squirrel is round.
("squirrel" "is" "round" "+")
((triple2) -> (rule3 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
((triple3) -> (rule4 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2