The cat does not eat the dog. The cat is blue. The cat is green. The cat is nice. The cat is rough. The cat is not young. The cat likes the dog. The cat visits the dog. The dog eats the cat. The dog is blue. The dog is green. The dog is nice. The dog is rough. The dog is young. The dog likes the cat. The dog visits the cat. If someone visits the cat then the cat visits the dog. If the cat is not green then the cat is rough. If someone is nice then they like the cat.
The cat does not eat the dog.
("cat" "eats" "dog" "-")
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is not young.
("cat" "is" "young" "-")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If someone visits the cat then the cat visits the dog.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If the cat is not green then the cat is rough.
((("cat" "is" "green" "~")) -> ("cat" "is" "rough" "+"))
If someone is nice then they like the cat.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "cat" "+"))
The cat likes the dog.
True
1
proof
[(triple7)]
("cat" "likes" "dog" "+")
triple7
The dog is not rough.
False
1
inv-proof
[(triple13)]
("dog" "is" "rough" "-")
triple13
The cat likes the cat.
True
2
proof
[(((triple4) -> rule3))]
("cat" "likes" "cat" "+")
((triple4) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat does not like the cat.
False
2
inv-proof
[(((triple4) -> rule3))]
("cat" "likes" "cat" "-")
((triple4) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat does not eat the dog.[(triple1)] The cat is blue.[(triple2)] The cat is green.[(triple3)] The cat is nice.[(triple4)] The cat is not young.[(triple6)] The cat is rough.[(triple5)] The cat likes the dog.[(triple7)] The cat visits the dog.[(triple8 OR ((triple16) -> rule1))] The dog eats the cat.[(triple9)] The dog is blue.[(triple10)] The dog is green.[(triple11)] The dog is nice.[(triple12)] The dog is rough.[(triple13)] The dog is young.[(triple14)] The dog likes the cat.[(triple15 OR ((triple12) -> rule3))] The dog visits the cat.[(triple16)] @1: The cat likes the cat.[(((triple4) -> rule3))]
The cat does not eat the dog.
("cat" "eats" "dog" "-")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is not young.
("cat" "is" "young" "-")
triple6
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat likes the dog.
("cat" "likes" "dog" "+")
triple7
The cat visits the dog.
("cat" "visits" "dog" "+")
triple8
((triple16) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
triple9
The dog is blue.
("dog" "is" "blue" "+")
triple10
The dog is green.
("dog" "is" "green" "+")
triple11
The dog is nice.
("dog" "is" "nice" "+")
triple12
The dog is rough.
("dog" "is" "rough" "+")
triple13
The dog is young.
("dog" "is" "young" "+")
triple14
The dog likes the cat.
("dog" "likes" "cat" "+")
triple15
((triple12) -> (rule3 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
triple16
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple4) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1