The mouse is cold. The mouse needs the squirrel. The squirrel likes the mouse. If someone is nice then they see the mouse. If someone needs the squirrel and they see the squirrel then they need the mouse. If someone needs the mouse then the mouse is blue. If someone is big and they need the squirrel then they like the squirrel. If the mouse likes the squirrel then the mouse sees the squirrel. If someone needs the squirrel and the squirrel likes the mouse then they see the squirrel.
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
If someone is nice then they see the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "mouse" "+"))
If someone needs the squirrel and they see the squirrel then they need the mouse.
((("someone" "needs" "squirrel" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the mouse then the mouse is blue.
((("someone" "needs" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If someone is big and they need the squirrel then they like the squirrel.
((("someone" "is" "big" "+") ("someone" "needs" "squirrel" "+")) -> ("someone" "likes" "squirrel" "+"))
If the mouse likes the squirrel then the mouse sees the squirrel.
((("mouse" "likes" "squirrel" "+")) -> ("mouse" "sees" "squirrel" "+"))
If someone needs the squirrel and the squirrel likes the mouse then they see the squirrel.
((("someone" "needs" "squirrel" "+") ("squirrel" "likes" "mouse" "+")) -> ("someone" "sees" "squirrel" "+"))
The mouse is cold.
True
1
proof
[(triple1)]
("mouse" "is" "cold" "+")
triple1
The mouse is not cold.
False
1
inv-proof
[(triple1)]
("mouse" "is" "cold" "-")
triple1
The mouse sees the squirrel.
True
3
proof
[(((triple2 triple3) -> rule6))]
("mouse" "sees" "squirrel" "+")
((triple2 triple3) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse does not see the squirrel.
False
3
inv-proof
[(((triple2 triple3) -> rule6))]
("mouse" "sees" "squirrel" "-")
((triple2 triple3) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse needs the mouse.
True
5
proof
[(((triple2 ((triple2 triple3) -> rule6)) -> rule2))]
("mouse" "needs" "mouse" "+")
((triple2 ((triple2 triple3) -> (rule6 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse does not need the mouse.
False
5
inv-proof
[(((triple2 ((triple2 triple3) -> rule6)) -> rule2))]
("mouse" "needs" "mouse" "-")
((triple2 ((triple2 triple3) -> (rule6 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse is blue.
True
6
proof
[(((((triple2 ((triple2 triple3) -> rule6)) -> rule2)) -> rule3))]
("mouse" "is" "blue" "+")
((((triple2 ((triple2 triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The mouse is not blue.
False
6
inv-proof
[(((((triple2 ((triple2 triple3) -> rule6)) -> rule2)) -> rule3))]
("mouse" "is" "blue" "-")
((((triple2 ((triple2 triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The squirrel does not see the mouse.
Unknown
inv-rconc
[@1: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "mouse" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The mouse likes the squirrel.
Unknown
rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "squirrel" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The mouse is cold.[(triple1)] The mouse needs the squirrel.[(triple2)] The squirrel likes the mouse.[(triple3)] @1: The mouse sees the squirrel.[(((triple2 triple3) -> rule6))] @2: The mouse needs the mouse.[(((triple2 ((triple2 triple3) -> rule6)) -> rule2))] @3: The mouse is blue.[(((((triple2 ((triple2 triple3) -> rule6)) -> rule2)) -> rule3))]
The mouse is cold.
("mouse" "is" "cold" "+")
triple1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple2 triple3) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple2 ((triple2 triple3) -> (rule6 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((((triple2 ((triple2 triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3