The mouse is cold. The mouse is green. The mouse is rough. The mouse sees the squirrel. The squirrel chases the mouse. The squirrel is cold. The squirrel is green. The squirrel is kind. The squirrel is rough. The squirrel is round. The squirrel sees the mouse. The squirrel visits the mouse. If the mouse visits the squirrel then the squirrel chases the mouse. If the squirrel is green and the squirrel is kind then the squirrel sees the mouse. If someone visits the mouse and the mouse visits the squirrel then the mouse is round. If someone sees the mouse and the mouse sees the squirrel then the mouse visits the squirrel. If someone is kind and they see the squirrel then they visit the mouse. If someone visits the mouse and the mouse visits the squirrel then the squirrel chases the mouse. If someone is round then they chase the squirrel. If someone visits the squirrel and the squirrel is round then they chase the mouse.
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If the mouse visits the squirrel then the squirrel chases the mouse.
((("mouse" "visits" "squirrel" "+")) -> ("squirrel" "chases" "mouse" "+"))
If the squirrel is green and the squirrel is kind then the squirrel sees the mouse.
((("squirrel" "is" "green" "+") ("squirrel" "is" "kind" "+")) -> ("squirrel" "sees" "mouse" "+"))
If someone visits the mouse and the mouse visits the squirrel then the mouse is round.
((("someone" "visits" "mouse" "+") ("mouse" "visits" "squirrel" "+")) -> ("mouse" "is" "round" "+"))
If someone sees the mouse and the mouse sees the squirrel then the mouse visits the squirrel.
((("someone" "sees" "mouse" "+") ("mouse" "sees" "squirrel" "+")) -> ("mouse" "visits" "squirrel" "+"))
If someone is kind and they see the squirrel then they visit the mouse.
((("someone" "is" "kind" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "mouse" "+"))
If someone visits the mouse and the mouse visits the squirrel then the squirrel chases the mouse.
((("someone" "visits" "mouse" "+") ("mouse" "visits" "squirrel" "+")) -> ("squirrel" "chases" "mouse" "+"))
If someone is round then they chase the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone visits the squirrel and the squirrel is round then they chase the mouse.
((("someone" "visits" "squirrel" "+") ("squirrel" "is" "round" "+")) -> ("someone" "chases" "mouse" "+"))
The squirrel is round.
True
1
proof
[(triple10)]
("squirrel" "is" "round" "+")
triple10
The mouse is not rough.
False
1
inv-proof
[(triple3)]
("mouse" "is" "rough" "-")
triple3
The squirrel chases the squirrel.
True
2
proof
[(((triple10) -> rule7))]
("squirrel" "chases" "squirrel" "+")
((triple10) -> (rule7 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The mouse does not visit the squirrel.
False
3
inv-proof
[(((triple11 triple4) -> rule4) OR ((((triple7 triple8) -> rule2) triple4) -> rule4))]
("mouse" "visits" "squirrel" "-")
((triple11 triple4) -> (rule4 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
((((triple7 triple8) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The mouse chases the mouse.
True
5
proof
[(((((triple11 triple4) -> rule4) triple10) -> rule8) OR ((((((triple7 triple8) -> rule2) triple4) -> rule4) triple10) -> rule8))]
("mouse" "chases" "mouse" "+")
((((triple11 triple4) -> (rule4 % int2)) triple10) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((((triple7 triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2)) triple10) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The mouse does not chase the mouse.
False
5
inv-proof
[(((((triple11 triple4) -> rule4) triple10) -> rule8) OR ((((((triple7 triple8) -> rule2) triple4) -> rule4) triple10) -> rule8))]
("mouse" "chases" "mouse" "-")
((((triple11 triple4) -> (rule4 % int2)) triple10) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((((triple7 triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2)) triple10) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The mouse chases the squirrel.
True
6
proof
[(((((triple12 ((triple11 triple4) -> rule4)) -> rule3)) -> rule7) OR ((((triple12 ((((triple7 triple8) -> rule2) triple4) -> rule4)) -> rule3)) -> rule7))]
("mouse" "chases" "squirrel" "+")
((((triple12 ((triple11 triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
((((triple12 ((((triple7 triple8) -> (rule2 % int4)) triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int4
The mouse does not chase the squirrel.
False
6
inv-proof
[(((((triple12 ((triple11 triple4) -> rule4)) -> rule3)) -> rule7) OR ((((triple12 ((((triple7 triple8) -> rule2) triple4) -> rule4)) -> rule3)) -> rule7))]
("mouse" "chases" "squirrel" "-")
((((triple12 ((triple11 triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
((((triple12 ((((triple7 triple8) -> (rule2 % int4)) triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int4
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The mouse is cold.[(triple1)] The mouse is green.[(triple2)] The mouse is rough.[(triple3)] The mouse sees the squirrel.[(triple4)] The squirrel chases the mouse.[(triple5 OR ((((triple11 triple4) -> rule4)) -> rule1) OR ((triple12 ((triple11 triple4) -> rule4)) -> rule6) OR ((((((triple7 triple8) -> rule2) triple4) -> rule4)) -> rule1) OR ((triple12 ((((triple7 triple8) -> rule2) triple4) -> rule4)) -> rule6))] The squirrel is cold.[(triple6)] The squirrel is green.[(triple7)] The squirrel is kind.[(triple8)] The squirrel is rough.[(triple9)] The squirrel is round.[(triple10)] The squirrel sees the mouse.[(triple11 OR ((triple7 triple8) -> rule2))] The squirrel visits the mouse.[(triple12)] @1: The mouse visits the squirrel.[(((triple11 triple4) -> rule4) OR ((((triple7 triple8) -> rule2) triple4) -> rule4))] The squirrel chases the squirrel.[(((triple10) -> rule7))] @2: The mouse chases the mouse.[(((((triple11 triple4) -> rule4) triple10) -> rule8) OR ((((((triple7 triple8) -> rule2) triple4) -> rule4) triple10) -> rule8))] The mouse is round.[(((triple12 ((triple11 triple4) -> rule4)) -> rule3) OR ((triple12 ((((triple7 triple8) -> rule2) triple4) -> rule4)) -> rule3))] @3: The mouse chases the squirrel.[(((((triple12 ((triple11 triple4) -> rule4)) -> rule3)) -> rule7) OR ((((triple12 ((((triple7 triple8) -> rule2) triple4) -> rule4)) -> rule3)) -> rule7))]
The mouse is cold.
("mouse" "is" "cold" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple4
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple5
((((triple11 triple4) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((triple12 ((triple11 triple4) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((((triple7 triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
((triple12 ((((triple7 triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple8
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple9
The squirrel is round.
("squirrel" "is" "round" "+")
triple10
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple11
((triple7 triple8) -> (rule2 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple12
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((triple11 triple4) -> (rule4 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
((((triple7 triple8) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple10) -> (rule7 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((triple11 triple4) -> (rule4 % int2)) triple10) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((((triple7 triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2)) triple10) -> (rule8 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The mouse is round.
("mouse" "is" "round" "+")
((triple12 ((triple11 triple4) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((triple12 ((((triple7 triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
((((triple12 ((triple11 triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
((((triple12 ((((triple7 triple8) -> (rule2 % int4)) triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int4