The mouse is big. The mouse is cold. The mouse does not like the squirrel. The mouse visits the squirrel. The squirrel is big. The squirrel is cold. The squirrel is round. The squirrel does not like the mouse. The squirrel needs the mouse. The squirrel visits the mouse. If something needs the squirrel and the squirrel needs the mouse then it does not need the mouse. If something visits the squirrel and the squirrel is big then it needs the squirrel. If something likes the mouse and it is not green then the mouse visits the squirrel.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something needs the squirrel and the squirrel needs the mouse then it does not need the mouse.
((("something" "needs" "squirrel" "+") ("squirrel" "needs" "mouse" "+")) -> ("something" "needs" "mouse" "-"))
If something visits the squirrel and the squirrel is big then it needs the squirrel.
((("something" "visits" "squirrel" "+") ("squirrel" "is" "big" "+")) -> ("something" "needs" "squirrel" "+"))
If something likes the mouse and it is not green then the mouse visits the squirrel.
((("something" "likes" "mouse" "+") ("something" "is" "green" "~")) -> ("mouse" "visits" "squirrel" "+"))
The mouse is big.
True
1
proof
[(triple1)]
("mouse" "is" "big" "+")
triple1
The squirrel likes the mouse.
False
1
inv-proof
[(triple8)]
("squirrel" "likes" "mouse" "+")
triple8
The mouse needs the squirrel.
True
3
proof
[(((triple4 triple5) -> rule2))]
("mouse" "needs" "squirrel" "+")
((triple4 triple5) -> (rule2 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse does not need the squirrel.
False
3
inv-proof
[(((triple4 triple5) -> rule2))]
("mouse" "needs" "squirrel" "-")
((triple4 triple5) -> (rule2 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse does not need the mouse.
True
5
proof
[(((((triple4 triple5) -> rule2) triple9) -> rule1))]
("mouse" "needs" "mouse" "-")
((((triple4 triple5) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse needs the mouse.
False
5
inv-proof
[(((((triple4 triple5) -> rule2) triple9) -> rule1))]
("mouse" "needs" "mouse" "+")
((((triple4 triple5) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
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 is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
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 is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The mouse does not like the squirrel.[(triple3)] The mouse is big.[(triple1)] The mouse is cold.[(triple2)] The mouse visits the squirrel.[(triple4)] The squirrel does not like the mouse.[(triple8)] The squirrel is big.[(triple5)] The squirrel is cold.[(triple6)] The squirrel is round.[(triple7)] The squirrel needs the mouse.[(triple9)] The squirrel visits the mouse.[(triple10)] @1: The mouse needs the squirrel.[(((triple4 triple5) -> rule2))] @2: The mouse does not need the mouse.[(((((triple4 triple5) -> rule2) triple9) -> rule1))]
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
triple3
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple4
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple6
The squirrel is round.
("squirrel" "is" "round" "+")
triple7
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple9
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple10
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((triple4 triple5) -> (rule2 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
((((triple4 triple5) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2