The cat chases the squirrel. The cat is kind. The cat likes the squirrel. The squirrel chases the cat. The squirrel is big. The squirrel is green. The squirrel is red. The squirrel is young. The squirrel likes the cat. The squirrel does not see the cat. If someone likes the cat then they see the squirrel. If someone is green then they see the squirrel. If someone likes the cat then they chase the cat. If the squirrel chases the cat and the cat is red then the cat does not chase the squirrel. If someone sees the cat then the cat sees the squirrel. If someone sees the squirrel and the squirrel does not see the cat then they are young. If someone likes the squirrel then they are green. If someone sees the cat and the cat is not young then they chase the squirrel.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
If someone likes the cat then they see the squirrel.
((("someone" "likes" "cat" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is green then they see the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone likes the cat then they chase the cat.
((("someone" "likes" "cat" "+")) -> ("someone" "chases" "cat" "+"))
If the squirrel chases the cat and the cat is red then the cat does not chase the squirrel.
((("squirrel" "chases" "cat" "+") ("cat" "is" "red" "+")) -> ("cat" "chases" "squirrel" "-"))
If someone sees the cat then the cat sees the squirrel.
((("someone" "sees" "cat" "+")) -> ("cat" "sees" "squirrel" "+"))
If someone sees the squirrel and the squirrel does not see the cat then they are young.
((("someone" "sees" "squirrel" "+") ("squirrel" "sees" "cat" "~")) -> ("someone" "is" "young" "+"))
If someone likes the squirrel then they are green.
((("someone" "likes" "squirrel" "+")) -> ("someone" "is" "green" "+"))
If someone sees the cat and the cat is not young then they chase the squirrel.
((("someone" "sees" "cat" "+") ("cat" "is" "young" "~")) -> ("someone" "chases" "squirrel" "+"))
The squirrel is green.
True
1
proof
[(triple6)]
("squirrel" "is" "green" "+")
triple6
The squirrel is not red.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "red" "-")
triple7
The cat is green.
True
2
proof
[(((triple3) -> rule7))]
("cat" "is" "green" "+")
((triple3) -> (rule7 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is not green.
False
2
inv-proof
[(((triple3) -> rule7))]
("cat" "is" "green" "-")
((triple3) -> (rule7 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat sees the squirrel.
True
3
proof
[(((((triple3) -> rule7)) -> rule2))]
("cat" "sees" "squirrel" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat does not see the squirrel.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule2))]
("cat" "sees" "squirrel" "-")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is young.
True
5
proof
[(((((((triple3) -> rule7)) -> rule2) triple10) -> rule6))]
("cat" "is" "young" "+")
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2)) triple10) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The cat is not young.
False
5
inv-proof
[(((((((triple3) -> rule7)) -> rule2) triple10) -> rule6))]
("cat" "is" "young" "-")
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2)) triple10) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "cat" "+")
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 squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat chases the squirrel.[(triple1)] The cat is kind.[(triple2)] The cat likes the squirrel.[(triple3)] The squirrel chases the cat.[(triple4 OR ((triple9) -> rule3))] The squirrel does not see the cat.[(triple10)] The squirrel is big.[(triple5)] The squirrel is green.[(triple6)] The squirrel is red.[(triple7)] The squirrel is young.[(triple8 OR ((((triple6) -> rule2) triple10) -> rule6) OR ((((triple9) -> rule1) triple10) -> rule6))] The squirrel likes the cat.[(triple9)] @1: The cat is green.[(((triple3) -> rule7))] The squirrel sees the squirrel.[(((triple6) -> rule2) OR ((triple9) -> rule1))] @2: The cat sees the squirrel.[(((((triple3) -> rule7)) -> rule2))] @3: The cat is young.[(((((((triple3) -> rule7)) -> rule2) triple10) -> rule6))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple3
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple4
((triple9) -> (rule3 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
triple10
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The squirrel is red.
("squirrel" "is" "red" "+")
triple7
The squirrel is young.
("squirrel" "is" "young" "+")
triple8
((((triple6) -> (rule2 % int2)) triple10) -> (rule6 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
((((triple9) -> (rule1 % int2)) triple10) -> (rule6 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple9
The cat is green.
("cat" "is" "green" "+")
((triple3) -> (rule7 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple6) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
((triple9) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is young.
("cat" "is" "young" "+")
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2)) triple10) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3