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