The mouse eats the squirrel. The mouse is cold. The mouse is green. The mouse is nice. The mouse needs the squirrel. The mouse sees the squirrel. The squirrel is kind. The squirrel is young. The squirrel needs the mouse. The squirrel does not see the mouse. If the squirrel is kind and the squirrel does not see the mouse then the squirrel eats the mouse. If something eats the mouse then the mouse is green. If something needs the mouse then the mouse needs the squirrel. If the mouse is cold and the mouse is not young then the mouse sees the squirrel. If the squirrel sees the mouse then the mouse sees the squirrel. If something eats the mouse then it is nice.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
If the squirrel is kind and the squirrel does not see the mouse then the squirrel eats the mouse.
((("squirrel" "is" "kind" "+") ("squirrel" "sees" "mouse" "~")) -> ("squirrel" "eats" "mouse" "+"))
If something eats the mouse then the mouse is green.
((("something" "eats" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If something needs the mouse then the mouse needs the squirrel.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "squirrel" "+"))
If the mouse is cold and the mouse is not young then the mouse sees the squirrel.
((("mouse" "is" "cold" "+") ("mouse" "is" "young" "~")) -> ("mouse" "sees" "squirrel" "+"))
If the squirrel sees the mouse then the mouse sees the squirrel.
((("squirrel" "sees" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
If something eats the mouse then it is nice.
((("something" "eats" "mouse" "+")) -> ("something" "is" "nice" "+"))
The mouse eats the squirrel.
True
1
proof
[(triple1)]
("mouse" "eats" "squirrel" "+")
triple1
The squirrel is not young.
False
1
inv-proof
[(triple8)]
("squirrel" "is" "young" "-")
triple8
The squirrel eats the mouse.
True
3
proof
[(((triple7 triple10) -> rule1))]
("squirrel" "eats" "mouse" "+")
((triple7 triple10) -> (rule1 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel does not eat the mouse.
False
3
inv-proof
[(((triple7 triple10) -> rule1))]
("squirrel" "eats" "mouse" "-")
((triple7 triple10) -> (rule1 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel is nice.
True
4
proof
[(((((triple7 triple10) -> rule1)) -> rule6))]
("squirrel" "is" "nice" "+")
((((triple7 triple10) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The squirrel is not nice.
False
4
inv-proof
[(((((triple7 triple10) -> rule1)) -> rule6))]
("squirrel" "is" "nice" "-")
((((triple7 triple10) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
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 kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse eats the squirrel.[(triple1)] The mouse is cold.[(triple2)] The mouse is green.[(triple3 OR ((((triple7 triple10) -> rule1)) -> rule2))] The mouse is nice.[(triple4)] The mouse needs the squirrel.[(triple5 OR ((triple9) -> rule3))] The mouse sees the squirrel.[(triple6)] The squirrel does not see the mouse.[(triple10)] The squirrel is kind.[(triple7)] The squirrel is young.[(triple8)] The squirrel needs the mouse.[(triple9)] @1: The squirrel eats the mouse.[(((triple7 triple10) -> rule1))] @2: The squirrel is nice.[(((((triple7 triple10) -> rule1)) -> rule6))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
((((triple7 triple10) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple5
((triple9) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple6
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
triple10
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple7
The squirrel is young.
("squirrel" "is" "young" "+")
triple8
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple9
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
((triple7 triple10) -> (rule1 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple7 triple10) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2