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