The mouse is cold. The mouse is green. The mouse is nice. The mouse is not round. The mouse is young. The mouse does not like the squirrel. The mouse needs the squirrel. The mouse sees the squirrel. The squirrel is cold. The squirrel is not nice. The squirrel is round. The squirrel is young. The squirrel does not like the mouse. The squirrel does not need the mouse. The squirrel does not see the mouse. If someone is nice then they see the mouse. If the mouse is not nice and the mouse is not round then the mouse is not cold. If someone likes the mouse and they are not round then the mouse likes the squirrel. If someone is green and they do not need the squirrel then they do not like the mouse. If someone is green and they do not like the mouse then they need the mouse. If someone sees the mouse then they need the mouse.
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is not nice.
("squirrel" "is" "nice" "-")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
If someone is nice then they see the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "mouse" "+"))
If the mouse is not nice and the mouse is not round then the mouse is not cold.
((("mouse" "is" "nice" "~") ("mouse" "is" "round" "~")) -> ("mouse" "is" "cold" "-"))
If someone likes the mouse and they are not round then the mouse likes the squirrel.
((("someone" "likes" "mouse" "+") ("someone" "is" "round" "~")) -> ("mouse" "likes" "squirrel" "+"))
If someone is green and they do not need the squirrel then they do not like the mouse.
((("someone" "is" "green" "+") ("someone" "needs" "squirrel" "~")) -> ("someone" "likes" "mouse" "-"))
If someone is green and they do not like the mouse then they need the mouse.
((("someone" "is" "green" "+") ("someone" "likes" "mouse" "~")) -> ("someone" "needs" "mouse" "+"))
If someone sees the mouse then they need the mouse.
((("someone" "sees" "mouse" "+")) -> ("someone" "needs" "mouse" "+"))
The squirrel is not nice.
True
1
proof
[(triple10)]
("squirrel" "is" "nice" "-")
triple10
The squirrel is not young.
False
1
inv-proof
[(triple12)]
("squirrel" "is" "young" "-")
triple12
The mouse sees the mouse.
True
2
proof
[(((triple3) -> rule1))]
("mouse" "sees" "mouse" "+")
((triple3) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("mouse" "sees" "mouse" "-")
((triple3) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse needs the mouse.
True
3
proof
[(((((triple3) -> rule1)) -> rule6))]
("mouse" "needs" "mouse" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse does not need the mouse.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6))]
("mouse" "needs" "mouse" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The mouse does not like the squirrel.[(triple6)] The mouse is cold.[(triple1)] The mouse is green.[(triple2)] The mouse is nice.[(triple3)] The mouse is not round.[(triple4)] The mouse is young.[(triple5)] The mouse needs the squirrel.[(triple7)] The mouse sees the squirrel.[(triple8)] The squirrel does not like the mouse.[(triple13)] The squirrel does not need the mouse.[(triple14)] The squirrel does not see the mouse.[(triple15)] The squirrel is cold.[(triple9)] The squirrel is not nice.[(triple10)] The squirrel is round.[(triple11)] The squirrel is young.[(triple12)] @1: The mouse sees the mouse.[(((triple3) -> rule1))] @2: The mouse needs the mouse.[(((((triple3) -> rule1)) -> rule6))]
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse is not round.
("mouse" "is" "round" "-")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple7
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple8
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
triple13
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
triple14
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
triple15
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is not nice.
("squirrel" "is" "nice" "-")
triple10
The squirrel is round.
("squirrel" "is" "round" "+")
triple11
The squirrel is young.
("squirrel" "is" "young" "+")
triple12
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple3) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2