The mouse likes the squirrel. The squirrel is big. The squirrel is blue. The squirrel is nice. The squirrel likes the mouse. The squirrel needs the mouse. The squirrel sees the mouse. If the mouse needs the squirrel and the squirrel likes the mouse then the mouse is nice. If the mouse is kind then the mouse needs the squirrel. If the mouse needs the squirrel and the mouse likes the squirrel then the mouse is blue. If the mouse likes the squirrel and the squirrel sees the mouse then the mouse is kind. If the squirrel needs the mouse then the mouse is nice. If the squirrel needs the mouse and the mouse likes the squirrel then the mouse sees the squirrel.
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If the mouse needs the squirrel and the squirrel likes the mouse then the mouse is nice.
((("mouse" "needs" "squirrel" "+") ("squirrel" "likes" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If the mouse is kind then the mouse needs the squirrel.
((("mouse" "is" "kind" "+")) -> ("mouse" "needs" "squirrel" "+"))
If the mouse needs the squirrel and the mouse likes the squirrel then the mouse is blue.
((("mouse" "needs" "squirrel" "+") ("mouse" "likes" "squirrel" "+")) -> ("mouse" "is" "blue" "+"))
If the mouse likes the squirrel and the squirrel sees the mouse then the mouse is kind.
((("mouse" "likes" "squirrel" "+") ("squirrel" "sees" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If the squirrel needs the mouse then the mouse is nice.
((("squirrel" "needs" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If the squirrel needs the mouse and the mouse likes the squirrel then the mouse sees the squirrel.
((("squirrel" "needs" "mouse" "+") ("mouse" "likes" "squirrel" "+")) -> ("mouse" "sees" "squirrel" "+"))
The squirrel sees the mouse.
True
1
proof
[(triple7)]
("squirrel" "sees" "mouse" "+")
triple7
The squirrel is not blue.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "blue" "-")
triple3
The mouse sees the squirrel.
True
3
proof
[(((triple6 triple1) -> rule6))]
("mouse" "sees" "squirrel" "+")
((triple6 triple1) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse is not nice.
False
2
inv-proof
[(((triple6) -> rule5) OR ((((((triple1 triple7) -> rule4)) -> rule2) triple5) -> rule1))]
("mouse" "is" "nice" "-")
((triple6) -> (rule5 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
((((((triple1 triple7) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse needs the squirrel.
True
4
proof
[(((((triple1 triple7) -> rule4)) -> rule2))]
("mouse" "needs" "squirrel" "+")
((((triple1 triple7) -> (rule4 % int2))) -> (rule2 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse does not need the squirrel.
False
4
inv-proof
[(((((triple1 triple7) -> rule4)) -> rule2))]
("mouse" "needs" "squirrel" "-")
((((triple1 triple7) -> (rule4 % int2))) -> (rule2 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is blue.
True
6
proof
[(((((((triple1 triple7) -> rule4)) -> rule2) triple1) -> rule3))]
("mouse" "is" "blue" "+")
((((((triple1 triple7) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse is not blue.
False
6
inv-proof
[(((((((triple1 triple7) -> rule4)) -> rule2) triple1) -> rule3))]
("mouse" "is" "blue" "-")
((((((triple1 triple7) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The mouse likes the squirrel.[(triple1)] The squirrel is big.[(triple2)] The squirrel is blue.[(triple3)] The squirrel is nice.[(triple4)] The squirrel likes the mouse.[(triple5)] The squirrel needs the mouse.[(triple6)] The squirrel sees the mouse.[(triple7)] @1: The mouse is kind.[(((triple1 triple7) -> rule4))] The mouse is nice.[(((triple6) -> rule5) OR ((((((triple1 triple7) -> rule4)) -> rule2) triple5) -> rule1))] The mouse sees the squirrel.[(((triple6 triple1) -> rule6))] @2: The mouse needs the squirrel.[(((((triple1 triple7) -> rule4)) -> rule2))] @3: The mouse is blue.[(((((((triple1 triple7) -> rule4)) -> rule2) triple1) -> rule3))]
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple1
The squirrel is big.
("squirrel" "is" "big" "+")
triple2
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple4
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple5
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple6
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
((triple1 triple7) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((triple6) -> (rule5 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
((((((triple1 triple7) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple6 triple1) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((((triple1 triple7) -> (rule4 % int2))) -> (rule2 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((((((triple1 triple7) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3