The mouse is not round. The squirrel eats the mouse. If something eats the squirrel and it does not eat the mouse then the mouse visits the squirrel. If something is red and it sees the mouse then the mouse does not see the squirrel. If something eats the squirrel then the squirrel is red. If something is red then it sees the mouse. If something eats the mouse then it eats the squirrel. If something visits the squirrel then the squirrel does not visit the mouse. If something visits the squirrel then the squirrel does not see the mouse. If something eats the squirrel then it sees the squirrel.
The mouse is not round.
("mouse" "is" "round" "-")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
If something eats the squirrel and it does not eat the mouse then the mouse visits the squirrel.
((("something" "eats" "squirrel" "+") ("something" "eats" "mouse" "~")) -> ("mouse" "visits" "squirrel" "+"))
If something is red and it sees the mouse then the mouse does not see the squirrel.
((("something" "is" "red" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "sees" "squirrel" "-"))
If something eats the squirrel then the squirrel is red.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
If something is red then it sees the mouse.
((("something" "is" "red" "+")) -> ("something" "sees" "mouse" "+"))
If something eats the mouse then it eats the squirrel.
((("something" "eats" "mouse" "+")) -> ("something" "eats" "squirrel" "+"))
If something visits the squirrel then the squirrel does not visit the mouse.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "visits" "mouse" "-"))
If something visits the squirrel then the squirrel does not see the mouse.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "sees" "mouse" "-"))
If something eats the squirrel then it sees the squirrel.
((("something" "eats" "squirrel" "+")) -> ("something" "sees" "squirrel" "+"))
The mouse is not round.
True
1
proof
[(triple1)]
("mouse" "is" "round" "-")
triple1
The mouse is round.
False
1
inv-proof
[(triple1)]
("mouse" "is" "round" "+")
triple1
The squirrel eats the squirrel.
True
2
proof
[(((triple2) -> rule5))]
("squirrel" "eats" "squirrel" "+")
((triple2) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel does not eat the squirrel.
False
2
inv-proof
[(((triple2) -> rule5))]
("squirrel" "eats" "squirrel" "-")
((triple2) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is red.
True
3
proof
[(((((triple2) -> rule5)) -> rule3))]
("squirrel" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel does not see the squirrel.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule8))]
("squirrel" "sees" "squirrel" "-")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel sees the mouse.
True
4
proof
[(((((((triple2) -> rule5)) -> rule3)) -> rule4))]
("squirrel" "sees" "mouse" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel does not see the mouse.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule3)) -> rule4))]
("squirrel" "sees" "mouse" "-")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The mouse does not visit the squirrel.
Unknown
inv-rconc
[@1: The mouse visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "squirrel" "-")
The mouse eats the squirrel.
Unknown
rconc
[@1: The mouse eats the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "squirrel" "+")
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The mouse is not round.[(triple1)] The squirrel eats the mouse.[(triple2)] @1: The squirrel eats the squirrel.[(((triple2) -> rule5))] @2: The squirrel is red.[(((((triple2) -> rule5)) -> rule3))] The squirrel sees the squirrel.[(((((triple2) -> rule5)) -> rule8))] @3: The squirrel sees the mouse.[(((((((triple2) -> rule5)) -> rule3)) -> rule4))] @4: The mouse does not see the squirrel.[(((((((triple2) -> rule5)) -> rule3) ((((((triple2) -> rule5)) -> rule3)) -> rule4)) -> rule2))]
The mouse is not round.
("mouse" "is" "round" "-")
triple1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple2) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int4