The cat likes the dog. The cat visits the squirrel. The cow is nice. The cow does not like the squirrel. The dog eats the squirrel. The squirrel is young. The squirrel does not like the dog. If the dog is green and the dog visits the cow then the cow is not nice. If the cat is nice and the cat likes the squirrel then the cat is red. If someone is young then they visit the cow.
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow does not like the squirrel.
("cow" "likes" "squirrel" "-")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
If the dog is green and the dog visits the cow then the cow is not nice.
((("dog" "is" "green" "+") ("dog" "visits" "cow" "+")) -> ("cow" "is" "nice" "-"))
If the cat is nice and the cat likes the squirrel then the cat is red.
((("cat" "is" "nice" "+") ("cat" "likes" "squirrel" "+")) -> ("cat" "is" "red" "+"))
If someone is young then they visit the cow.
((("someone" "is" "young" "+")) -> ("someone" "visits" "cow" "+"))
The cat visits the squirrel.
True
1
proof
[(triple2)]
("cat" "visits" "squirrel" "+")
triple2
The cat does not like the dog.
False
1
inv-proof
[(triple1)]
("cat" "likes" "dog" "-")
triple1
The squirrel visits the cow.
True
2
proof
[(((triple6) -> rule3))]
("squirrel" "visits" "cow" "+")
((triple6) -> (rule3 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not visit the cow.
False
2
inv-proof
[(((triple6) -> rule3))]
("squirrel" "visits" "cow" "-")
((triple6) -> (rule3 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The cat does not visit the cow.
Unknown
inv-rconc
[@1: The cat visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "visits" "cow" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "cow" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cat eats the squirrel.
Unknown
random
[@0: The cat eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "squirrel" "+")
@0: The cat likes the dog.[(triple1)] The cat visits the squirrel.[(triple2)] The cow does not like the squirrel.[(triple4)] The cow is nice.[(triple3)] The dog eats the squirrel.[(triple5)] The squirrel does not like the dog.[(triple7)] The squirrel is young.[(triple6)] @1: The squirrel visits the cow.[(((triple6) -> rule3))]
The cat likes the dog.
("cat" "likes" "dog" "+")
triple1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple2
The cow does not like the squirrel.
("cow" "likes" "squirrel" "-")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple5
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
triple7
The squirrel is young.
("squirrel" "is" "young" "+")
triple6
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
((triple6) -> (rule3 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1