The mouse chases the squirrel. The mouse does not eat the squirrel. The mouse is big. The mouse is not nice. The mouse is red. The mouse is not rough. The mouse does not need the squirrel. The squirrel chases the mouse. The squirrel eats the mouse. The squirrel is big. The squirrel is nice. The squirrel is red. The squirrel is rough. The squirrel is round. The squirrel needs the mouse. If something is nice then it does not chase the squirrel. If something needs the mouse then the mouse is not rough. If something chases the squirrel then the squirrel needs the mouse. All rough things are round. If something chases the mouse and it is red then it is rough. If something chases the mouse and the mouse is nice then it is not rough. If the mouse needs the squirrel and the mouse chases the squirrel then the squirrel eats the mouse. If the mouse eats the squirrel and the mouse is round then the mouse needs the squirrel.
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse does not eat the squirrel.
("mouse" "eats" "squirrel" "-")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something is nice then it does not chase the squirrel.
((("something" "is" "nice" "+")) -> ("something" "chases" "squirrel" "-"))
If something needs the mouse then the mouse is not rough.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "rough" "-"))
If something chases the squirrel then the squirrel needs the mouse.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "+"))
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something chases the mouse and it is red then it is rough.
((("something" "chases" "mouse" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something chases the mouse and the mouse is nice then it is not rough.
((("something" "chases" "mouse" "+") ("mouse" "is" "nice" "+")) -> ("something" "is" "rough" "-"))
If the mouse needs the squirrel and the mouse chases the squirrel then the squirrel eats the mouse.
((("mouse" "needs" "squirrel" "+") ("mouse" "chases" "squirrel" "+")) -> ("squirrel" "eats" "mouse" "+"))
If the mouse eats the squirrel and the mouse is round then the mouse needs the squirrel.
((("mouse" "eats" "squirrel" "+") ("mouse" "is" "round" "+")) -> ("mouse" "needs" "squirrel" "+"))
The mouse is not rough.
True
1
proof
[(triple6 OR ((triple15) -> rule2) OR ((((triple1) -> rule3)) -> rule2))]
("mouse" "is" "rough" "-")
triple6
((triple15) -> (rule2 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The squirrel is not round.
False
1
inv-proof
[(triple14 OR ((triple13) -> rule4) OR ((((triple8 triple12) -> rule5)) -> rule4))]
("squirrel" "is" "round" "-")
triple14
((triple13) -> (rule4 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
((((triple8 triple12) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "round" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The mouse chases the squirrel.[(triple1)] The mouse does not eat the squirrel.[(triple2)] The mouse does not need the squirrel.[(triple7)] The mouse is big.[(triple3)] The mouse is not nice.[(triple4)] The mouse is not rough.[(triple6 OR ((triple15) -> rule2) OR ((((triple1) -> rule3)) -> rule2))] The mouse is red.[(triple5)] The squirrel chases the mouse.[(triple8)] The squirrel eats the mouse.[(triple9)] The squirrel is big.[(triple10)] The squirrel is nice.[(triple11)] The squirrel is red.[(triple12)] The squirrel is rough.[(triple13 OR ((triple8 triple12) -> rule5))] The squirrel is round.[(triple14 OR ((triple13) -> rule4) OR ((((triple8 triple12) -> rule5)) -> rule4))] The squirrel needs the mouse.[(triple15 OR ((triple1) -> rule3))] @1: The squirrel does not chase the squirrel.[(((triple11) -> rule1))]
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple1
The mouse does not eat the squirrel.
("mouse" "eats" "squirrel" "-")
triple2
The mouse does not need the squirrel.
("mouse" "needs" "squirrel" "-")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse is not nice.
("mouse" "is" "nice" "-")
triple4
The mouse is not rough.
("mouse" "is" "rough" "-")
triple6
((triple15) -> (rule2 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
triple5
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple8
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple9
The squirrel is big.
("squirrel" "is" "big" "+")
triple10
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple11
The squirrel is red.
("squirrel" "is" "red" "+")
triple12
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple13
((triple8 triple12) -> (rule5 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
triple14
((triple13) -> (rule4 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
((((triple8 triple12) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple15
((triple1) -> (rule3 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
((triple11) -> (rule1 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1