The cat eats the dog. The cat is green. The cat is kind. The cat is rough. The cat is young. The cat likes the dog. The cat needs the dog. The dog is green. The dog is rough. The dog is young. The dog likes the cat. The dog needs the cat. If someone is young and green then they need the dog.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
If someone is young and green then they need the dog.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "needs" "dog" "+"))
The cat needs the dog.
True
1
proof
[(triple7 OR ((triple5 triple2) -> rule1))]
("cat" "needs" "dog" "+")
triple7
((triple5 triple2) -> (rule1 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The dog is not rough.
False
1
inv-proof
[(triple9)]
("dog" "is" "rough" "-")
triple9
The dog needs the dog.
True
3
proof
[(((triple10 triple8) -> rule1))]
("dog" "needs" "dog" "+")
((triple10 triple8) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not need the dog.
False
3
inv-proof
[(((triple10 triple8) -> rule1))]
("dog" "needs" "dog" "-")
((triple10 triple8) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not eat the cat.
Unknown
inv-random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
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 eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The cat eats the dog.[(triple1)] The cat is green.[(triple2)] The cat is kind.[(triple3)] The cat is rough.[(triple4)] The cat is young.[(triple5)] The cat likes the dog.[(triple6)] The cat needs the dog.[(triple7 OR ((triple5 triple2) -> rule1))] The dog is green.[(triple8)] The dog is rough.[(triple9)] The dog is young.[(triple10)] The dog likes the cat.[(triple11)] The dog needs the cat.[(triple12)] @1: The dog needs the dog.[(((triple10 triple8) -> rule1))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the dog.
("cat" "likes" "dog" "+")
triple6
The cat needs the dog.
("cat" "needs" "dog" "+")
triple7
((triple5 triple2) -> (rule1 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The dog is green.
("dog" "is" "green" "+")
triple8
The dog is rough.
("dog" "is" "rough" "+")
triple9
The dog is young.
("dog" "is" "young" "+")
triple10
The dog likes the cat.
("dog" "likes" "cat" "+")
triple11
The dog needs the cat.
("dog" "needs" "cat" "+")
triple12
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple10 triple8) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1