The mouse eats the squirrel. The mouse sees the squirrel. The mouse visits the squirrel. The squirrel is blue. The squirrel is nice. The squirrel sees the mouse. The squirrel visits the mouse. If something visits the squirrel and it visits the mouse then the squirrel eats the mouse. If the mouse is kind then the mouse does not visit the squirrel. If the squirrel does not see the mouse then the mouse visits the squirrel. If something sees the mouse and the mouse is not kind then the mouse does not eat the squirrel. Blue things are not rough. If something is blue and it does not eat the squirrel then the squirrel is nice.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something visits the squirrel and it visits the mouse then the squirrel eats the mouse.
((("something" "visits" "squirrel" "+") ("something" "visits" "mouse" "+")) -> ("squirrel" "eats" "mouse" "+"))
If the mouse is kind then the mouse does not visit the squirrel.
((("mouse" "is" "kind" "+")) -> ("mouse" "visits" "squirrel" "-"))
If the squirrel does not see the mouse then the mouse visits the squirrel.
((("squirrel" "sees" "mouse" "~")) -> ("mouse" "visits" "squirrel" "+"))
If something sees the mouse and the mouse is not kind then the mouse does not eat the squirrel.
((("something" "sees" "mouse" "+") ("mouse" "is" "kind" "~")) -> ("mouse" "eats" "squirrel" "-"))
Blue things are not rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "-"))
If something is blue and it does not eat the squirrel then the squirrel is nice.
((("something" "is" "blue" "+") ("something" "eats" "squirrel" "~")) -> ("squirrel" "is" "nice" "+"))
The squirrel is nice.
True
1
proof
[(triple5)]
("squirrel" "is" "nice" "+")
triple5
The mouse does not visit the squirrel.
False
1
inv-proof
[(triple3)]
("mouse" "visits" "squirrel" "-")
triple3
The squirrel is not rough.
True
2
proof
[(((triple4) -> rule5))]
("squirrel" "is" "rough" "-")
((triple4) -> (rule5 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1
The squirrel is rough.
False
2
inv-proof
[(((triple4) -> rule5))]
("squirrel" "is" "rough" "+")
((triple4) -> (rule5 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1
The squirrel does not eat the mouse.
Unknown
inv-rconc
[@1: The squirrel eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "mouse" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The mouse eats the squirrel.[(triple1)] The mouse sees the squirrel.[(triple2)] The mouse visits the squirrel.[(triple3)] The squirrel is blue.[(triple4)] The squirrel is nice.[(triple5)] The squirrel sees the mouse.[(triple6)] The squirrel visits the mouse.[(triple7)] @1: The squirrel is not rough.[(((triple4) -> rule5))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple4
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple5
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple6
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple7
The squirrel is not rough.
("squirrel" "is" "rough" "-")
((triple4) -> (rule5 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1