The mouse is red. The mouse is not rough. The mouse likes the squirrel. The mouse sees the squirrel. The squirrel is rough. The squirrel does not like the mouse. The squirrel sees the mouse. If someone is rough and big then they see the squirrel. If someone likes the squirrel then they need the mouse. If someone needs the mouse and they are not rough then they are round. If someone likes the mouse then they see the mouse. If someone sees the squirrel then they like the squirrel. Round people are big. If the squirrel does not see the mouse then the mouse needs the squirrel. If the squirrel likes the mouse then the mouse does not need the squirrel.
The mouse is red.
("mouse" "is" "red" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone is rough and big then they see the squirrel.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone likes the squirrel then they need the mouse.
((("someone" "likes" "squirrel" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the mouse and they are not rough then they are round.
((("someone" "needs" "mouse" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "round" "+"))
If someone likes the mouse then they see the mouse.
((("someone" "likes" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the squirrel then they like the squirrel.
((("someone" "sees" "squirrel" "+")) -> ("someone" "likes" "squirrel" "+"))
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If the squirrel does not see the mouse then the mouse needs the squirrel.
((("squirrel" "sees" "mouse" "~")) -> ("mouse" "needs" "squirrel" "+"))
If the squirrel likes the mouse then the mouse does not need the squirrel.
((("squirrel" "likes" "mouse" "+")) -> ("mouse" "needs" "squirrel" "-"))
The mouse likes the squirrel.
True
1
proof
[(triple3 OR ((triple4) -> rule5))]
("mouse" "likes" "squirrel" "+")
triple3
((triple4) -> (rule5 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse is not red.
False
1
inv-proof
[(triple1)]
("mouse" "is" "red" "-")
triple1
The mouse needs the mouse.
True
2
proof
[(((triple3) -> rule2) OR ((((triple4) -> rule5)) -> rule2))]
("mouse" "needs" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse does not need the mouse.
False
2
inv-proof
[(((triple3) -> rule2) OR ((((triple4) -> rule5)) -> rule2))]
("mouse" "needs" "mouse" "-")
((triple3) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse is round.
True
4
proof
[(((((triple3) -> rule2) triple2) -> rule3) OR ((((((triple4) -> rule5)) -> rule2) triple2) -> rule3))]
("mouse" "is" "round" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The mouse is not round.
False
4
inv-proof
[(((((triple3) -> rule2) triple2) -> rule3) OR ((((((triple4) -> rule5)) -> rule2) triple2) -> rule3))]
("mouse" "is" "round" "-")
((((triple3) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The mouse is big.
True
5
proof
[(((((((triple3) -> rule2) triple2) -> rule3)) -> rule6) OR ((((((((triple4) -> rule5)) -> rule2) triple2) -> rule3)) -> rule6))]
("mouse" "is" "big" "+")
((((((triple3) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
((((((((triple4) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int4
The mouse is not big.
False
5
inv-proof
[(((((((triple3) -> rule2) triple2) -> rule3)) -> rule6) OR ((((((((triple4) -> rule5)) -> rule2) triple2) -> rule3)) -> rule6))]
("mouse" "is" "big" "-")
((((((triple3) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
((((((((triple4) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int4
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@3: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@4: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule6 <- rule3 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The mouse needs the squirrel.
Unknown
rconc
[@1: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "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 mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The mouse is not rough.[(triple2)] The mouse is red.[(triple1)] The mouse likes the squirrel.[(triple3 OR ((triple4) -> rule5))] The mouse sees the squirrel.[(triple4)] The squirrel does not like the mouse.[(triple6)] The squirrel is rough.[(triple5)] The squirrel sees the mouse.[(triple7)] @1: The mouse needs the mouse.[(((triple3) -> rule2) OR ((((triple4) -> rule5)) -> rule2))] @2: The mouse is round.[(((((triple3) -> rule2) triple2) -> rule3) OR ((((((triple4) -> rule5)) -> rule2) triple2) -> rule3))] @3: The mouse is big.[(((((((triple3) -> rule2) triple2) -> rule3)) -> rule6) OR ((((((((triple4) -> rule5)) -> rule2) triple2) -> rule3)) -> rule6))]
The mouse is not rough.
("mouse" "is" "rough" "-")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple3
((triple4) -> (rule5 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple4
The squirrel does not like the mouse.
("squirrel" "likes" "mouse" "-")
triple6
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple5
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple7
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
((((((triple3) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
((((((((triple4) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int4