The cat is cold. The cat is kind. The cat is red. The cat visits the dog. The cat visits the squirrel. The dog does not eat the cat. The dog likes the squirrel. The squirrel eats the dog. The squirrel visits the cat. The squirrel visits the dog. If something likes the squirrel and it does not visit the squirrel then it eats the cat. If something is young then it does not eat the cat. If something is red then it visits the cat. If something visits the cat then it is young. If something eats the squirrel then it does not like the squirrel. If the dog likes the squirrel then the dog visits the cat.
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The dog does not eat the cat.
("dog" "eats" "cat" "-")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If something likes the squirrel and it does not visit the squirrel then it eats the cat.
((("something" "likes" "squirrel" "+") ("something" "visits" "squirrel" "~")) -> ("something" "eats" "cat" "+"))
If something is young then it does not eat the cat.
((("something" "is" "young" "+")) -> ("something" "eats" "cat" "-"))
If something is red then it visits the cat.
((("something" "is" "red" "+")) -> ("something" "visits" "cat" "+"))
If something visits the cat then it is young.
((("something" "visits" "cat" "+")) -> ("something" "is" "young" "+"))
If something eats the squirrel then it does not like the squirrel.
((("something" "eats" "squirrel" "+")) -> ("something" "likes" "squirrel" "-"))
If the dog likes the squirrel then the dog visits the cat.
((("dog" "likes" "squirrel" "+")) -> ("dog" "visits" "cat" "+"))
The cat is kind.
True
1
proof
[(triple2)]
("cat" "is" "kind" "+")
triple2
The cat is not kind.
False
1
inv-proof
[(triple2)]
("cat" "is" "kind" "-")
triple2
The dog visits the cat.
True
2
proof
[(((triple7) -> rule6))]
("dog" "visits" "cat" "+")
((triple7) -> (rule6 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("cat" "visits" "cat" "-")
((triple3) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is young.
True
3
proof
[(((((triple3) -> rule3)) -> rule4))]
("cat" "is" "young" "+")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The dog is not young.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule4))]
("dog" "is" "young" "-")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat does not eat the cat.
True
4
proof
[(((((((triple3) -> rule3)) -> rule4)) -> rule2))]
("cat" "eats" "cat" "-")
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
int3
The cat eats the cat.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule4)) -> rule2))]
("cat" "eats" "cat" "+")
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
int3
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The dog visits the squirrel.
Unknown
random
[@0: The dog visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "squirrel" "+")
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 likes the squirrel.
Unknown
random
[@0: The cat likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "squirrel" "+")
The dog does not like the cat.
Unknown
inv-random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "-")
The cat eats the dog.
Unknown
random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "+")
The cat does not like the dog.
Unknown
inv-random
[@0: The cat likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "dog" "-")
The squirrel likes the cat.
Unknown
random
[@0: The squirrel likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "cat" "+")
@0: The cat is cold.[(triple1)] The cat is kind.[(triple2)] The cat is red.[(triple3)] The cat visits the dog.[(triple4)] The cat visits the squirrel.[(triple5)] The dog does not eat the cat.[(triple6 OR ((((((triple7) -> rule6)) -> rule4)) -> rule2))] The dog likes the squirrel.[(triple7)] The squirrel eats the dog.[(triple8)] The squirrel visits the cat.[(triple9)] The squirrel visits the dog.[(triple10)] @1: The cat visits the cat.[(((triple3) -> rule3))] The dog visits the cat.[(((triple7) -> rule6))] The squirrel is young.[(((triple9) -> rule4))] @2: The cat is young.[(((((triple3) -> rule3)) -> rule4))] The dog is young.[(((((triple7) -> rule6)) -> rule4))] The squirrel does not eat the cat.[(((((triple9) -> rule4)) -> rule2))] @3: The cat does not eat the cat.[(((((((triple3) -> rule3)) -> rule4)) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
triple4
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple5
The dog does not eat the cat.
("dog" "eats" "cat" "-")
triple6
((((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The dog does not eat the cat.
("dog" "eats" "cat" "-")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple7
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple8
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple9
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple10
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple3) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
((triple7) -> (rule6 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
((triple9) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The squirrel does not eat the cat.
("squirrel" "eats" "cat" "-")
((((triple9) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel does not eat the cat.
("squirrel" "eats" "cat" "-")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The cat does not eat the cat.
("cat" "eats" "cat" "-")
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
int3