The cat is blue. The cat is green. The cat is rough. The cat likes the mouse. The cat needs the mouse. The cat sees the mouse. The mouse is green. The mouse is red. The mouse is rough. The mouse likes the cat. The mouse needs the cat. The mouse sees the cat. If someone likes the mouse then the mouse is rough. If the mouse likes the cat and the mouse needs the cat then the cat needs the mouse. If someone is red and they like the mouse then the mouse sees the cat. If someone likes the mouse and they need the mouse then the mouse is blue. If someone likes the cat and they see the mouse then the cat needs the mouse. If someone needs the mouse and they need the cat then they like the mouse. If the mouse is cold then the mouse needs the cat. If someone is blue then they need the mouse.
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone likes the mouse then the mouse is rough.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If the mouse likes the cat and the mouse needs the cat then the cat needs the mouse.
((("mouse" "likes" "cat" "+") ("mouse" "needs" "cat" "+")) -> ("cat" "needs" "mouse" "+"))
If someone is red and they like the mouse then the mouse sees the cat.
((("someone" "is" "red" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If someone likes the mouse and they need the mouse then the mouse is blue.
((("someone" "likes" "mouse" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If someone likes the cat and they see the mouse then the cat needs the mouse.
((("someone" "likes" "cat" "+") ("someone" "sees" "mouse" "+")) -> ("cat" "needs" "mouse" "+"))
If someone needs the mouse and they need the cat then they like the mouse.
((("someone" "needs" "mouse" "+") ("someone" "needs" "cat" "+")) -> ("someone" "likes" "mouse" "+"))
If the mouse is cold then the mouse needs the cat.
((("mouse" "is" "cold" "+")) -> ("mouse" "needs" "cat" "+"))
If someone is blue then they need the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "mouse" "+"))
The cat likes the mouse.
True
1
proof
[(triple4)]
("cat" "likes" "mouse" "+")
triple4
The mouse does not like the cat.
False
1
inv-proof
[(triple10)]
("mouse" "likes" "cat" "-")
triple10
The mouse is blue.
True
3
proof
[(((triple4 triple5) -> rule4) OR ((triple4 ((triple1) -> rule8)) -> rule4) OR ((triple4 ((triple10 triple11) -> rule2)) -> rule4))]
("mouse" "is" "blue" "+")
((triple4 triple5) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple4 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
((triple4 ((triple10 triple11) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The mouse is not blue.
False
3
inv-proof
[(((triple4 triple5) -> rule4) OR ((triple4 ((triple1) -> rule8)) -> rule4) OR ((triple4 ((triple10 triple11) -> rule2)) -> rule4))]
("mouse" "is" "blue" "-")
((triple4 triple5) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple4 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
((triple4 ((triple10 triple11) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The mouse needs the mouse.
True
4
proof
[(((((triple4 triple5) -> rule4)) -> rule8) OR ((((triple4 ((triple1) -> rule8)) -> rule4)) -> rule8) OR ((((triple4 ((triple10 triple11) -> rule2)) -> rule4)) -> rule8))]
("mouse" "needs" "mouse" "+")
((((triple4 triple5) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple4 ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
((((triple4 ((triple10 triple11) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
The mouse does not need the mouse.
False
4
inv-proof
[(((((triple4 triple5) -> rule4)) -> rule8) OR ((((triple4 ((triple1) -> rule8)) -> rule4)) -> rule8) OR ((((triple4 ((triple10 triple11) -> rule2)) -> rule4)) -> rule8))]
("mouse" "needs" "mouse" "-")
((((triple4 triple5) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple4 ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
((((triple4 ((triple10 triple11) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
The mouse likes the mouse.
True
6
proof
[(((((((triple4 triple5) -> rule4)) -> rule8) triple11) -> rule6) OR ((((((triple4 ((triple1) -> rule8)) -> rule4)) -> rule8) triple11) -> rule6) OR ((((((triple4 ((triple10 triple11) -> rule2)) -> rule4)) -> rule8) triple11) -> rule6))]
("mouse" "likes" "mouse" "+")
((((((triple4 triple5) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple4 ((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
((((((triple4 ((triple10 triple11) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
The mouse does not like the mouse.
False
6
inv-proof
[(((((((triple4 triple5) -> rule4)) -> rule8) triple11) -> rule6) OR ((((((triple4 ((triple1) -> rule8)) -> rule4)) -> rule8) triple11) -> rule6) OR ((((((triple4 ((triple10 triple11) -> rule2)) -> rule4)) -> rule8) triple11) -> rule6))]
("mouse" "likes" "mouse" "-")
((((((triple4 triple5) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple4 ((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
((((((triple4 ((triple10 triple11) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
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 cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is blue.[(triple1)] The cat is green.[(triple2)] The cat is rough.[(triple3)] The cat likes the mouse.[(triple4)] The cat needs the mouse.[(triple5 OR ((triple1) -> rule8) OR ((triple10 triple11) -> rule2))] The cat sees the mouse.[(triple6)] The mouse is green.[(triple7)] The mouse is red.[(triple8)] The mouse is rough.[(triple9 OR ((triple4) -> rule1) OR ((((((((triple4 triple5) -> rule4)) -> rule8) triple11) -> rule6)) -> rule1) OR ((((((((triple4 ((triple1) -> rule8)) -> rule4)) -> rule8) triple11) -> rule6)) -> rule1) OR ((((((((triple4 ((triple10 triple11) -> rule2)) -> rule4)) -> rule8) triple11) -> rule6)) -> rule1))] The mouse likes the cat.[(triple10)] The mouse needs the cat.[(triple11)] The mouse sees the cat.[(triple12 OR ((triple8 ((((((triple4 triple5) -> rule4)) -> rule8) triple11) -> rule6)) -> rule3) OR ((triple8 ((((((triple4 ((triple1) -> rule8)) -> rule4)) -> rule8) triple11) -> rule6)) -> rule3) OR ((triple8 ((((((triple4 ((triple10 triple11) -> rule2)) -> rule4)) -> rule8) triple11) -> rule6)) -> rule3))] @1: The mouse is blue.[(((triple4 triple5) -> rule4) OR ((triple4 ((triple1) -> rule8)) -> rule4) OR ((triple4 ((triple10 triple11) -> rule2)) -> rule4))] @2: The mouse needs the mouse.[(((((triple4 triple5) -> rule4)) -> rule8) OR ((((triple4 ((triple1) -> rule8)) -> rule4)) -> rule8) OR ((((triple4 ((triple10 triple11) -> rule2)) -> rule4)) -> rule8))] @3: The mouse likes the mouse.[(((((((triple4 triple5) -> rule4)) -> rule8) triple11) -> rule6) OR ((((((triple4 ((triple1) -> rule8)) -> rule4)) -> rule8) triple11) -> rule6) OR ((((((triple4 ((triple10 triple11) -> rule2)) -> rule4)) -> rule8) triple11) -> rule6))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple5
((triple1) -> (rule8 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
((triple10 triple11) -> (rule2 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The mouse is red.
("mouse" "is" "red" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
((triple4) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((((((((triple4 triple5) -> (rule4 % int4))) -> (rule8 % int3)) triple11) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
((((((((triple4 ((triple1) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) triple11) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int5
((((((((triple4 ((triple10 triple11) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) triple11) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int5
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple10
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple11
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple12
((triple8 ((((((triple4 triple5) -> (rule4 % int4))) -> (rule8 % int3)) triple11) -> (rule6 % int2))) -> (rule3 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
((triple8 ((((((triple4 ((triple1) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) triple11) -> (rule6 % int2))) -> (rule3 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int5
((triple8 ((((((triple4 ((triple10 triple11) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule8 % int3)) triple11) -> (rule6 % int2))) -> (rule3 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int5
The mouse is blue.
("mouse" "is" "blue" "+")
((triple4 triple5) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple4 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
((triple4 ((triple10 triple11) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple4 triple5) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple4 ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
((((triple4 ((triple10 triple11) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple4 triple5) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple4 ((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
((((((triple4 ((triple10 triple11) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple11) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4