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