The mouse does not eat the squirrel. The squirrel eats the mouse. The squirrel is round. If the squirrel eats the mouse then the mouse needs the squirrel. If the mouse needs the squirrel then the mouse is green. If someone is nice and they do not eat the mouse then they need the squirrel. If someone is blue then they need the squirrel. If someone is nice and round then they chase the mouse. If the mouse needs the squirrel and the squirrel eats the mouse then the squirrel is nice. If the mouse needs the squirrel then the squirrel is young. If the mouse does not need the squirrel then the squirrel needs the mouse.
The mouse does not eat the squirrel.
("mouse" "eats" "squirrel" "-")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If the squirrel eats the mouse then the mouse needs the squirrel.
((("squirrel" "eats" "mouse" "+")) -> ("mouse" "needs" "squirrel" "+"))
If the mouse needs the squirrel then the mouse is green.
((("mouse" "needs" "squirrel" "+")) -> ("mouse" "is" "green" "+"))
If someone is nice and they do not eat the mouse then they need the squirrel.
((("someone" "is" "nice" "+") ("someone" "eats" "mouse" "~")) -> ("someone" "needs" "squirrel" "+"))
If someone is blue then they need the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone is nice and round then they chase the mouse.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "chases" "mouse" "+"))
If the mouse needs the squirrel and the squirrel eats the mouse then the squirrel is nice.
((("mouse" "needs" "squirrel" "+") ("squirrel" "eats" "mouse" "+")) -> ("squirrel" "is" "nice" "+"))
If the mouse needs the squirrel then the squirrel is young.
((("mouse" "needs" "squirrel" "+")) -> ("squirrel" "is" "young" "+"))
If the mouse does not need the squirrel then the squirrel needs the mouse.
((("mouse" "needs" "squirrel" "~")) -> ("squirrel" "needs" "mouse" "+"))
The mouse does not eat the squirrel.
True
1
proof
[(triple1)]
("mouse" "eats" "squirrel" "-")
triple1
The squirrel does not eat the mouse.
False
1
inv-proof
[(triple2)]
("squirrel" "eats" "mouse" "-")
triple2
The mouse needs the squirrel.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "needs" "squirrel" "+")
((triple2) -> (rule1 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse does not need the squirrel.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "needs" "squirrel" "-")
((triple2) -> (rule1 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel is nice.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule6))]
("squirrel" "is" "nice" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is not green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("mouse" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel chases the mouse.
True
6
proof
[(((((((triple2) -> rule1) triple2) -> rule6) triple3) -> rule5))]
("squirrel" "chases" "mouse" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule6 % int2)) triple3) -> (rule5 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel does not chase the mouse.
False
6
inv-proof
[(((((((triple2) -> rule1) triple2) -> rule6) triple3) -> rule5))]
("squirrel" "chases" "mouse" "-")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule6 % int2)) triple3) -> (rule5 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel does not need the mouse.
Unknown
inv-rconc
[@1: The squirrel needs the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "needs" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse does not chase the squirrel.
Unknown
inv-random
[@0: The mouse chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "squirrel" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The mouse does not eat the squirrel.[(triple1)] The squirrel eats the mouse.[(triple2)] The squirrel is round.[(triple3)] @1: The mouse needs the squirrel.[(((triple2) -> rule1))] @2: The mouse is green.[(((((triple2) -> rule1)) -> rule2))] The squirrel is nice.[(((((triple2) -> rule1) triple2) -> rule6))] The squirrel is young.[(((((triple2) -> rule1)) -> rule7))] @3: The squirrel chases the mouse.[(((((((triple2) -> rule1) triple2) -> rule6) triple3) -> rule5))]
The mouse does not eat the squirrel.
("mouse" "eats" "squirrel" "-")
triple1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple2
The squirrel is round.
("squirrel" "is" "round" "+")
triple3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((triple2) -> (rule1 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
((((((triple2) -> (rule1 % int3)) triple2) -> (rule6 % int2)) triple3) -> (rule5 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3