The mouse eats the squirrel. The mouse is nice. The mouse is rough. The mouse needs the squirrel. The mouse sees the squirrel. The squirrel eats the mouse. The squirrel is red. The squirrel is rough. The squirrel needs the mouse. The squirrel sees the mouse. If someone is red then they need the mouse. If someone eats the mouse and the mouse is big then the mouse is red. If someone needs the squirrel and they are rough then they need the mouse. If someone is red then they see the squirrel. If someone is rough and they eat the mouse then the mouse needs the squirrel. If someone eats the squirrel then the squirrel eats the mouse. If someone eats the mouse and the mouse is rough then the mouse eats the squirrel. If the squirrel is nice then the squirrel sees the mouse.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone is red then they need the mouse.
((("someone" "is" "red" "+")) -> ("someone" "needs" "mouse" "+"))
If someone eats the mouse and the mouse is big then the mouse is red.
((("someone" "eats" "mouse" "+") ("mouse" "is" "big" "+")) -> ("mouse" "is" "red" "+"))
If someone needs the squirrel and they are rough then they need the mouse.
((("someone" "needs" "squirrel" "+") ("someone" "is" "rough" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is red then they see the squirrel.
((("someone" "is" "red" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is rough and they eat the mouse then the mouse needs the squirrel.
((("someone" "is" "rough" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "needs" "squirrel" "+"))
If someone eats the squirrel then the squirrel eats the mouse.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "eats" "mouse" "+"))
If someone eats the mouse and the mouse is rough then the mouse eats the squirrel.
((("someone" "eats" "mouse" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "eats" "squirrel" "+"))
If the squirrel is nice then the squirrel sees the mouse.
((("squirrel" "is" "nice" "+")) -> ("squirrel" "sees" "mouse" "+"))
The squirrel eats the mouse.
True
1
proof
[(triple6 OR ((triple1) -> rule6))]
("squirrel" "eats" "mouse" "+")
triple6
((triple1) -> (rule6 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse is not nice.
False
1
inv-proof
[(triple2)]
("mouse" "is" "nice" "-")
triple2
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "red" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The mouse eats the squirrel.[(triple1 OR ((triple6 triple3) -> rule7))] The mouse is nice.[(triple2)] The mouse is rough.[(triple3)] The mouse needs the squirrel.[(triple4 OR ((triple8 triple6) -> rule5) OR ((triple8 ((triple1) -> rule6)) -> rule5))] The mouse sees the squirrel.[(triple5)] The squirrel eats the mouse.[(triple6 OR ((triple1) -> rule6))] The squirrel is red.[(triple7)] The squirrel is rough.[(triple8)] The squirrel needs the mouse.[(triple9 OR ((triple7) -> rule1))] The squirrel sees the mouse.[(triple10)] @1: The mouse needs the mouse.[(((triple4 triple3) -> rule3) OR ((((triple8 triple6) -> rule5) triple3) -> rule3) OR ((((triple8 ((triple1) -> rule6)) -> rule5) triple3) -> rule3))] The squirrel sees the squirrel.[(((triple7) -> rule4))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
((triple6 triple3) -> (rule7 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple4
((triple8 triple6) -> (rule5 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
((triple8 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple5
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple6
((triple1) -> (rule6 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
triple7
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple8
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple9
((triple7) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple10
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple4 triple3) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple8 triple6) -> (rule5 % int2)) triple3) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
((((triple8 ((triple1) -> (rule6 % int3))) -> (rule5 % int2)) triple3) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple7) -> (rule4 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1