The cat does not see the cow. The cow sees the dog. The dog is not young. The rabbit visits the cat. If something chases the cow and it is not young then it does not chase the dog. If something chases the rabbit then the rabbit chases the dog.
The cat does not see the cow.
("cat" "sees" "cow" "-")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is not young.
("dog" "is" "young" "-")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If something chases the cow and it is not young then it does not chase the dog.
((("something" "chases" "cow" "+") ("something" "is" "young" "~")) -> ("something" "chases" "dog" "-"))
If something chases the rabbit then the rabbit chases the dog.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "dog" "+"))
The rabbit visits the cat.
True
1
proof
[(triple4)]
("rabbit" "visits" "cat" "+")
triple4
The cow does not see the dog.
False
1
inv-proof
[(triple2)]
("cow" "sees" "dog" "-")
triple2
The rabbit does not chase the dog.
Unknown
inv-rconc
[@1: The rabbit chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "dog" "-")
The cow chases the dog.
Unknown
random
[@0: The cow chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "dog" "+")
@0: The cat does not see the cow.[(triple1)] The cow sees the dog.[(triple2)] The dog is not young.[(triple3)] The rabbit visits the cat.[(triple4)]
The cat does not see the cow.
("cat" "sees" "cow" "-")
triple1
The cow sees the dog.
("cow" "sees" "dog" "+")
triple2
The dog is not young.
("dog" "is" "young" "-")
triple3
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple4