The cat does not chase the squirrel. The cat eats the squirrel. The cat is blue. The cat is not kind. The cat is nice. The cat is not young. The cat likes the squirrel. The squirrel chases the cat. The squirrel does not eat the cat. The squirrel is blue. The squirrel is not green. The squirrel is kind. The squirrel is nice. The squirrel is young. The squirrel likes the cat. If something eats the squirrel then the squirrel likes the cat. If something is young then it eats the squirrel. If something likes the cat then it does not like the squirrel. If the squirrel chases the cat and the cat does not chase the squirrel then the cat is blue. If something chases the squirrel and the squirrel likes the cat then it is blue. If the cat does not like the squirrel then the squirrel is nice.
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat is not young.
("cat" "is" "young" "-")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel does not eat the cat.
("squirrel" "eats" "cat" "-")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is not green.
("squirrel" "is" "green" "-")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If something eats the squirrel then the squirrel likes the cat.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "likes" "cat" "+"))
If something is young then it eats the squirrel.
((("something" "is" "young" "+")) -> ("something" "eats" "squirrel" "+"))
If something likes the cat then it does not like the squirrel.
((("something" "likes" "cat" "+")) -> ("something" "likes" "squirrel" "-"))
If the squirrel chases the cat and the cat does not chase the squirrel then the cat is blue.
((("squirrel" "chases" "cat" "+") ("cat" "chases" "squirrel" "~")) -> ("cat" "is" "blue" "+"))
If something chases the squirrel and the squirrel likes the cat then it is blue.
((("something" "chases" "squirrel" "+") ("squirrel" "likes" "cat" "+")) -> ("something" "is" "blue" "+"))
If the cat does not like the squirrel then the squirrel is nice.
((("cat" "likes" "squirrel" "~")) -> ("squirrel" "is" "nice" "+"))
The squirrel is young.
True
1
proof
[(triple14)]
("squirrel" "is" "young" "+")
triple14
The squirrel is not kind.
False
1
inv-proof
[(triple12)]
("squirrel" "is" "kind" "-")
triple12
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat does not chase the squirrel.[(triple1)] The cat eats the squirrel.[(triple2)] The cat is blue.[(triple3 OR ((triple8 triple1) -> rule4))] The cat is nice.[(triple5)] The cat is not kind.[(triple4)] The cat is not young.[(triple6)] The cat likes the squirrel.[(triple7)] The squirrel chases the cat.[(triple8)] The squirrel does not eat the cat.[(triple9)] The squirrel is blue.[(triple10)] The squirrel is kind.[(triple12)] The squirrel is nice.[(triple13)] The squirrel is not green.[(triple11)] The squirrel is young.[(triple14)] The squirrel likes the cat.[(triple15 OR ((triple2) -> rule1) OR ((((triple14) -> rule2)) -> rule1))] @1: The squirrel does not like the squirrel.[(((triple15) -> rule3) OR ((((triple2) -> rule1)) -> rule3) OR ((((((triple14) -> rule2)) -> rule1)) -> rule3))] The squirrel eats the squirrel.[(((triple14) -> rule2))]
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
((triple8 triple1) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is not kind.
("cat" "is" "kind" "-")
triple4
The cat is not young.
("cat" "is" "young" "-")
triple6
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple7
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple8
The squirrel does not eat the cat.
("squirrel" "eats" "cat" "-")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple12
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple13
The squirrel is not green.
("squirrel" "is" "green" "-")
triple11
The squirrel is young.
("squirrel" "is" "young" "+")
triple14
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple15
((triple2) -> (rule1 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
((((triple14) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel does not like the squirrel.
("squirrel" "likes" "squirrel" "-")
((triple15) -> (rule3 % int1))
The squirrel does not like the squirrel.
("squirrel" "likes" "squirrel" "-")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel does not like the squirrel.
("squirrel" "likes" "squirrel" "-")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
((((((triple14) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel does not like the squirrel.
("squirrel" "likes" "squirrel" "-")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple14) -> (rule2 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1