The mouse is big. The mouse is blue. The mouse is green. The mouse sees the squirrel. The squirrel is big. The squirrel is green. The squirrel is red. The squirrel is round. The squirrel needs the mouse. The squirrel sees the mouse. If someone is red and round then they need the squirrel.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone is red and round then they need the squirrel.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "needs" "squirrel" "+"))
The squirrel needs the mouse.
True
1
proof
[(triple9)]
("squirrel" "needs" "mouse" "+")
triple9
The mouse is not green.
False
1
inv-proof
[(triple3)]
("mouse" "is" "green" "-")
triple3
The squirrel needs the squirrel.
True
3
proof
[(((triple7 triple8) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((triple7 triple8) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel does not need the squirrel.
False
3
inv-proof
[(((triple7 triple8) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((triple7 triple8) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The mouse does not need the squirrel.
Unknown
inv-rconc
[@1: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The squirrel does not visit the mouse.
Unknown
inv-random
[@0: The squirrel visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "mouse" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The mouse is big.[(triple1)] The mouse is blue.[(triple2)] The mouse is green.[(triple3)] The mouse sees the squirrel.[(triple4)] The squirrel is big.[(triple5)] The squirrel is green.[(triple6)] The squirrel is red.[(triple7)] The squirrel is round.[(triple8)] The squirrel needs the mouse.[(triple9)] The squirrel sees the mouse.[(triple10)] @1: The squirrel needs the squirrel.[(((triple7 triple8) -> rule1))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple4
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The squirrel is red.
("squirrel" "is" "red" "+")
triple7
The squirrel is round.
("squirrel" "is" "round" "+")
triple8
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple9
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple10
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple7 triple8) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1