The mouse chases the squirrel. The mouse is not green. The mouse is round. The mouse needs the squirrel. The mouse sees the squirrel. The squirrel chases the mouse. The squirrel does not need the mouse. If someone is green then they are round. Big people are young. If the squirrel is green and the squirrel sees the mouse then the squirrel does not need the mouse. If someone is round then they need the squirrel. If someone is blue and they chase the squirrel then they see the squirrel. If someone chases the squirrel then the squirrel does not see the mouse. If the mouse chases the squirrel then the squirrel is round. If the mouse is blue and the squirrel does not see the mouse then the mouse is not young.
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If the squirrel is green and the squirrel sees the mouse then the squirrel does not need the mouse.
((("squirrel" "is" "green" "+") ("squirrel" "sees" "mouse" "+")) -> ("squirrel" "needs" "mouse" "-"))
If someone is round then they need the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone is blue and they chase the squirrel then they see the squirrel.
((("someone" "is" "blue" "+") ("someone" "chases" "squirrel" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone chases the squirrel then the squirrel does not see the mouse.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "sees" "mouse" "-"))
If the mouse chases the squirrel then the squirrel is round.
((("mouse" "chases" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
If the mouse is blue and the squirrel does not see the mouse then the mouse is not young.
((("mouse" "is" "blue" "+") ("squirrel" "sees" "mouse" "~")) -> ("mouse" "is" "young" "-"))
The squirrel does not need the mouse.
True
1
proof
[(triple7)]
("squirrel" "needs" "mouse" "-")
triple7
The mouse does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("mouse" "chases" "squirrel" "-")
triple1
The squirrel does not see the mouse.
True
2
proof
[(((triple1) -> rule6))]
("squirrel" "sees" "mouse" "-")
((triple1) -> (rule6 % int1))
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
int1
The squirrel is not round.
False
2
inv-proof
[(((triple1) -> rule7))]
("squirrel" "is" "round" "-")
((triple1) -> (rule7 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel needs the squirrel.
True
3
proof
[(((((triple1) -> rule7)) -> rule4))]
("squirrel" "needs" "squirrel" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel does not need the squirrel.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule4))]
("squirrel" "needs" "squirrel" "-")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel is young.
Unknown
rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "young" "+")
The mouse is not young.
Unknown
inv-rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "young" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The mouse chases the squirrel.[(triple1)] The mouse is not green.[(triple2)] The mouse is round.[(triple3)] The mouse needs the squirrel.[(triple4 OR ((triple3) -> rule4))] The mouse sees the squirrel.[(triple5)] The squirrel chases the mouse.[(triple6)] The squirrel does not need the mouse.[(triple7)] @1: The squirrel does not see the mouse.[(((triple1) -> rule6))] The squirrel is round.[(((triple1) -> rule7))] @2: The squirrel needs the squirrel.[(((((triple1) -> rule7)) -> rule4))]
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple1
The mouse is not green.
("mouse" "is" "green" "-")
triple2
The mouse is round.
("mouse" "is" "round" "+")
triple3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple4
((triple3) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple5
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple6
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
triple7
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
((triple1) -> (rule6 % int1))
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
((triple1) -> (rule7 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2