The bald eagle is green. The bald eagle is young. The bald eagle likes the squirrel. The bald eagle needs the mouse. The cat is nice. The cat is not round. The cat needs the bald eagle. The cat needs the mouse. The cat sees the mouse. The cat sees the squirrel. The mouse is not big. The mouse likes the bald eagle. The mouse sees the bald eagle. The squirrel is big. The squirrel sees the cat. If something needs the bald eagle then the bald eagle does not need the cat. If something is young and it sees the cat then it is big. If the cat is nice then the cat is young. If something is young then it sees the cat. If something is big and it needs the mouse then the mouse does not see the cat. If something sees the cat then the cat likes the squirrel.
The bald eagle is green.
("bald eagle" "is" "green" "+")
The bald eagle is young.
("bald eagle" "is" "young" "+")
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is not round.
("cat" "is" "round" "-")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If something needs the bald eagle then the bald eagle does not need the cat.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "needs" "cat" "-"))
If something is young and it sees the cat then it is big.
((("something" "is" "young" "+") ("something" "sees" "cat" "+")) -> ("something" "is" "big" "+"))
If the cat is nice then the cat is young.
((("cat" "is" "nice" "+")) -> ("cat" "is" "young" "+"))
If something is young then it sees the cat.
((("something" "is" "young" "+")) -> ("something" "sees" "cat" "+"))
If something is big and it needs the mouse then the mouse does not see the cat.
((("something" "is" "big" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "sees" "cat" "-"))
If something sees the cat then the cat likes the squirrel.
((("something" "sees" "cat" "+")) -> ("cat" "likes" "squirrel" "+"))
The mouse sees the bald eagle.
True
1
proof
[(triple13)]
("mouse" "sees" "bald eagle" "+")
triple13
The cat does not see the mouse.
False
1
inv-proof
[(triple9)]
("cat" "sees" "mouse" "-")
triple9
The bald eagle does not need the cat.
True
2
proof
[(((triple7) -> rule1))]
("bald eagle" "needs" "cat" "-")
((triple7) -> (rule1 % int1))
The bald eagle does not need the cat.
("bald eagle" "needs" "cat" "-")
int1
The cat does not like the squirrel.
False
2
inv-proof
[(((triple15) -> rule6) OR ((((triple2) -> rule4)) -> rule6) OR ((((((triple5) -> rule3)) -> rule4)) -> rule6))]
("cat" "likes" "squirrel" "-")
((triple15) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat sees the cat.
True
3
proof
[(((((triple5) -> rule3)) -> rule4))]
("cat" "sees" "cat" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The bald eagle is not big.
False
4
inv-proof
[(((triple2 ((triple2) -> rule4)) -> rule2))]
("bald eagle" "is" "big" "-")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The mouse does not see the cat.
True
6
proof
[(((((triple2 ((triple2) -> rule4)) -> rule2) triple4) -> rule5) OR ((((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule4)) -> rule2) triple8) -> rule5))]
("mouse" "sees" "cat" "-")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2)) triple4) -> (rule5 % int1))
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
int1
The bald eagle is big.
("bald eagle" "is" "big" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
((((((triple5) -> (rule3 % int4)) ((((triple5) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
The cat is not big.
False
6
inv-proof
[(((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule4)) -> rule2))]
("cat" "is" "big" "-")
((((triple5) -> (rule3 % int3)) ((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat does not need the squirrel.
Unknown
inv-random
[@0: The cat needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "squirrel" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The bald eagle sees the squirrel.
Unknown
random
[@0: The bald eagle sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "squirrel" "+")
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" "+")
The cat does not like the mouse.
Unknown
inv-random
[@0: The cat likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "mouse" "-")
The squirrel likes the cat.
Unknown
random
[@0: The squirrel likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "cat" "+")
@0: The bald eagle is green.[(triple1)] The bald eagle is young.[(triple2)] The bald eagle likes the squirrel.[(triple3)] The bald eagle needs the mouse.[(triple4)] The cat is nice.[(triple5)] The cat is not round.[(triple6)] The cat needs the bald eagle.[(triple7)] The cat needs the mouse.[(triple8)] The cat sees the mouse.[(triple9)] The cat sees the squirrel.[(triple10)] The mouse is not big.[(triple11)] The mouse likes the bald eagle.[(triple12)] The mouse sees the bald eagle.[(triple13)] The squirrel is big.[(triple14)] The squirrel sees the cat.[(triple15)] @1: The bald eagle does not need the cat.[(((triple7) -> rule1))] The bald eagle sees the cat.[(((triple2) -> rule4))] The cat is young.[(((triple5) -> rule3))] The cat likes the squirrel.[(((triple15) -> rule6) OR ((((triple2) -> rule4)) -> rule6) OR ((((((triple5) -> rule3)) -> rule4)) -> rule6))] @2: The bald eagle is big.[(((triple2 ((triple2) -> rule4)) -> rule2))] The cat sees the cat.[(((((triple5) -> rule3)) -> rule4))] @3: The cat is big.[(((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule4)) -> rule2))] The mouse does not see the cat.[(((((triple2 ((triple2) -> rule4)) -> rule2) triple4) -> rule5) OR ((((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule4)) -> rule2) triple8) -> rule5))]
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple1
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple2
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
triple3
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is not round.
("cat" "is" "round" "-")
triple6
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple7
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple8
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple9
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple10
The mouse is not big.
("mouse" "is" "big" "-")
triple11
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
triple12
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
triple13
The squirrel is big.
("squirrel" "is" "big" "+")
triple14
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple15
The bald eagle does not need the cat.
("bald eagle" "needs" "cat" "-")
((triple7) -> (rule1 % int1))
The bald eagle does not need the cat.
("bald eagle" "needs" "cat" "-")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
((triple2) -> (rule4 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((triple5) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((triple15) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The bald eagle is big.
("bald eagle" "is" "big" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is big.
("cat" "is" "big" "+")
((((triple5) -> (rule3 % int3)) ((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2)) triple4) -> (rule5 % int1))
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
int1
The bald eagle is big.
("bald eagle" "is" "big" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
((((((triple5) -> (rule3 % int4)) ((((triple5) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) triple8) -> (rule5 % int1))
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4