The cat chases the squirrel. The cat eats the squirrel. The cat is cold. The cat is kind. The cat is nice. The cat is red. The cat visits the squirrel. The squirrel chases the cat. The squirrel eats the cat. The squirrel is cold. The squirrel is green. The squirrel is kind. The squirrel is nice. The squirrel is red. The squirrel visits the cat. If someone visits the squirrel and the squirrel chases the cat then they are red. If the squirrel is kind then the squirrel chases the cat. If someone is red then they chase the cat. If someone eats the squirrel and they chase the squirrel then the squirrel chases the cat. If the cat visits the squirrel and the squirrel visits the cat then the cat chases the squirrel. If someone eats the cat then the cat is red. If someone chases the squirrel and they are green then the squirrel eats the cat. If someone is green and they chase the squirrel then they are nice.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone visits the squirrel and the squirrel chases the cat then they are red.
((("someone" "visits" "squirrel" "+") ("squirrel" "chases" "cat" "+")) -> ("someone" "is" "red" "+"))
If the squirrel is kind then the squirrel chases the cat.
((("squirrel" "is" "kind" "+")) -> ("squirrel" "chases" "cat" "+"))
If someone is red then they chase the cat.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cat" "+"))
If someone eats the squirrel and they chase the squirrel then the squirrel chases the cat.
((("someone" "eats" "squirrel" "+") ("someone" "chases" "squirrel" "+")) -> ("squirrel" "chases" "cat" "+"))
If the cat visits the squirrel and the squirrel visits the cat then the cat chases the squirrel.
((("cat" "visits" "squirrel" "+") ("squirrel" "visits" "cat" "+")) -> ("cat" "chases" "squirrel" "+"))
If someone eats the cat then the cat is red.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone chases the squirrel and they are green then the squirrel eats the cat.
((("someone" "chases" "squirrel" "+") ("someone" "is" "green" "+")) -> ("squirrel" "eats" "cat" "+"))
If someone is green and they chase the squirrel then they are nice.
((("someone" "is" "green" "+") ("someone" "chases" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
The squirrel is cold.
True
1
proof
[(triple10)]
("squirrel" "is" "cold" "+")
triple10
The squirrel is not cold.
False
1
inv-proof
[(triple10)]
("squirrel" "is" "cold" "-")
triple10
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The cat chases the squirrel.[(triple1 OR ((triple7 triple15) -> rule5))] The cat eats the squirrel.[(triple2)] The cat is cold.[(triple3)] The cat is kind.[(triple4)] The cat is nice.[(triple5)] The cat is red.[(triple6 OR ((triple9) -> rule6) OR ((triple7 triple8) -> rule1) OR ((triple7 ((triple12) -> rule2)) -> rule1) OR ((triple7 ((triple14) -> rule3)) -> rule1) OR ((triple7 ((triple2 triple1) -> rule4)) -> rule1) OR ((triple7 ((triple2 ((triple7 triple15) -> rule5)) -> rule4)) -> rule1))] The cat visits the squirrel.[(triple7)] The squirrel chases the cat.[(triple8 OR ((triple12) -> rule2) OR ((triple14) -> rule3) OR ((triple2 triple1) -> rule4) OR ((triple2 ((triple7 triple15) -> rule5)) -> rule4))] The squirrel eats the cat.[(triple9)] The squirrel is cold.[(triple10)] The squirrel is green.[(triple11)] The squirrel is kind.[(triple12)] The squirrel is nice.[(triple13)] The squirrel is red.[(triple14)] The squirrel visits the cat.[(triple15)] @1: The cat chases the cat.[(((triple6) -> rule3) OR ((((triple9) -> rule6)) -> rule3) OR ((((triple7 triple8) -> rule1)) -> rule3) OR ((((triple7 ((triple12) -> rule2)) -> rule1)) -> rule3) OR ((((triple7 ((triple14) -> rule3)) -> rule1)) -> rule3) OR ((((triple7 ((triple2 triple1) -> rule4)) -> rule1)) -> rule3) OR ((((triple7 ((triple2 ((triple7 triple15) -> rule5)) -> rule4)) -> rule1)) -> rule3))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
((triple7 triple15) -> (rule5 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is red.
("cat" "is" "red" "+")
triple6
((triple9) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple7 triple8) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple7 ((triple12) -> (rule2 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
((triple7 ((triple14) -> (rule3 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
((triple7 ((triple2 triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
((triple7 ((triple2 ((triple7 triple15) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int3
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple7
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple8
((triple12) -> (rule2 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
((triple14) -> (rule3 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
((triple2 triple1) -> (rule4 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
((triple2 ((triple7 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple9
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple10
The squirrel is green.
("squirrel" "is" "green" "+")
triple11
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple12
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple13
The squirrel is red.
("squirrel" "is" "red" "+")
triple14
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple15
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple6) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple7 triple8) -> (rule1 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((triple7 ((triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
((((triple7 ((triple14) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
((((triple7 ((triple2 triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
((((triple7 ((triple2 ((triple7 triple15) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int4