The cat likes the cow. The cow likes the dog. The dog visits the cat. If something visits the cat then the cat visits the dog. If the cow is blue and the cow is young then the cow visits the cat. If something likes the cow then the cow is blue.
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If something visits the cat then the cat visits the dog.
((("something" "visits" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If the cow is blue and the cow is young then the cow visits the cat.
((("cow" "is" "blue" "+") ("cow" "is" "young" "+")) -> ("cow" "visits" "cat" "+"))
If something likes the cow then the cow is blue.
((("something" "likes" "cow" "+")) -> ("cow" "is" "blue" "+"))
The dog visits the cat.
True
1
proof
[(triple3)]
("dog" "visits" "cat" "+")
triple3
The dog does not visit the cat.
False
1
inv-proof
[(triple3)]
("dog" "visits" "cat" "-")
triple3
The cow is blue.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow does not visit the cat.
Unknown
inv-rconc
[@1: The cow visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "cat" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The dog does not like the cow.
Unknown
inv-random
[@0: The dog likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cow" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The cat likes the cow.[(triple1)] The cow likes the dog.[(triple2)] The dog visits the cat.[(triple3)] @1: The cat visits the dog.[(((triple3) -> rule1))] The cow is blue.[(((triple1) -> rule3))]
The cat likes the cow.
("cat" "likes" "cow" "+")
triple1
The cow likes the dog.
("cow" "likes" "dog" "+")
triple2
The dog visits the cat.
("dog" "visits" "cat" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple3) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1