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