The cat chases the dog. The cat eats the dog. The cat is blue. The cat is cold. The cat is kind. The cat is red. The cat is rough. The cat needs the dog. The dog eats the cat. The dog is blue. If something needs the cat then it eats the cat. If something eats the cat then it chases the cat. If something is rough then it needs the cat. If something chases the cat and the cat needs the dog then the dog eats the cat. If something eats the dog and it chases the dog then the dog is rough. If something is red then it chases the cat. If something eats the dog and it needs the dog then the dog eats the cat. If the dog needs the cat then the dog eats the cat.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog is blue.
("dog" "is" "blue" "+")
If something needs the cat then it eats the cat.
((("something" "needs" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something eats the cat then it chases the cat.
((("something" "eats" "cat" "+")) -> ("something" "chases" "cat" "+"))
If something is rough then it needs the cat.
((("something" "is" "rough" "+")) -> ("something" "needs" "cat" "+"))
If something chases the cat and the cat needs the dog then the dog eats the cat.
((("something" "chases" "cat" "+") ("cat" "needs" "dog" "+")) -> ("dog" "eats" "cat" "+"))
If something eats the dog and it chases the dog then the dog is rough.
((("something" "eats" "dog" "+") ("something" "chases" "dog" "+")) -> ("dog" "is" "rough" "+"))
If something is red then it chases the cat.
((("something" "is" "red" "+")) -> ("something" "chases" "cat" "+"))
If something eats the dog and it needs the dog then the dog eats the cat.
((("something" "eats" "dog" "+") ("something" "needs" "dog" "+")) -> ("dog" "eats" "cat" "+"))
If the dog needs the cat then the dog eats the cat.
((("dog" "needs" "cat" "+")) -> ("dog" "eats" "cat" "+"))
The dog is blue.
True
1
proof
[(triple10)]
("dog" "is" "blue" "+")
triple10
The cat is not cold.
False
1
inv-proof
[(triple4)]
("cat" "is" "cold" "-")
triple4
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The cat chases the dog.[(triple1)] The cat eats the dog.[(triple2)] The cat is blue.[(triple3)] The cat is cold.[(triple4)] The cat is kind.[(triple5)] The cat is red.[(triple6)] The cat is rough.[(triple7)] The cat needs the dog.[(triple8)] The dog eats the cat.[(triple9 OR ((triple2 triple8) -> rule7) OR ((((triple6) -> rule6) triple8) -> rule4) OR ((((((triple2 triple1) -> rule5)) -> rule3)) -> rule1) OR ((((((triple2 triple1) -> rule5)) -> rule3)) -> rule8) OR ((((((((triple7) -> rule3)) -> rule1)) -> rule2) triple8) -> rule4))] The dog is blue.[(triple10)] @1: The cat chases the cat.[(((triple6) -> rule6) OR ((((((triple7) -> rule3)) -> rule1)) -> rule2))] The cat needs the cat.[(((triple7) -> rule3))] The dog chases the cat.[(((triple9) -> rule2) OR ((((triple2 triple8) -> rule7)) -> rule2) OR ((((((triple6) -> rule6) triple8) -> rule4)) -> rule2) OR ((((((((triple2 triple1) -> rule5)) -> rule3)) -> rule1)) -> rule2) OR ((((((((triple2 triple1) -> rule5)) -> rule3)) -> rule8)) -> rule2) OR ((((((((((triple7) -> rule3)) -> rule1)) -> rule2) triple8) -> rule4)) -> rule2))] The dog is rough.[(((triple2 triple1) -> rule5))] @2: The cat eats the cat.[(((((triple7) -> rule3)) -> rule1))] The dog needs the cat.[(((((triple2 triple1) -> rule5)) -> rule3))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat eats the dog.
("cat" "eats" "dog" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is cold.
("cat" "is" "cold" "+")
triple4
The cat is kind.
("cat" "is" "kind" "+")
triple5
The cat is red.
("cat" "is" "red" "+")
triple6
The cat is rough.
("cat" "is" "rough" "+")
triple7
The cat needs the dog.
("cat" "needs" "dog" "+")
triple8
The dog eats the cat.
("dog" "eats" "cat" "+")
triple9
((triple2 triple8) -> (rule7 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
((((triple6) -> (rule6 % int2)) triple8) -> (rule4 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
((((((triple2 triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
((((((triple2 triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
((((((((triple7) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int2)) triple8) -> (rule4 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat needs the cat.
("cat" "needs" "cat" "+")
int4
The dog is blue.
("dog" "is" "blue" "+")
triple10
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple6) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
((((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple7) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
((triple9) -> (rule2 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
((((triple2 triple8) -> (rule7 % int2))) -> (rule2 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
((((((triple6) -> (rule6 % int3)) triple8) -> (rule4 % int2))) -> (rule2 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((((((triple2 triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog needs the cat.
("dog" "needs" "cat" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
int4
((((((((triple2 triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog needs the cat.
("dog" "needs" "cat" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
int4
((((((((((triple7) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule2 % int3)) triple8) -> (rule4 % int2))) -> (rule2 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The cat eats the cat.
("cat" "eats" "cat" "+")
int4
The cat needs the cat.
("cat" "needs" "cat" "+")
int5
The dog is rough.
("dog" "is" "rough" "+")
((triple2 triple1) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The dog needs the cat.
("dog" "needs" "cat" "+")
((((triple2 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2