The cow chases the lion. The dog is rough. The lion needs the dog. If something needs the lion and the lion chases the dog then the lion does not chase the cow. If something is green then it chases the dog.
The cow chases the lion.
("cow" "chases" "lion" "+")
The dog is rough.
("dog" "is" "rough" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
If something needs the lion and the lion chases the dog then the lion does not chase the cow.
((("something" "needs" "lion" "+") ("lion" "chases" "dog" "+")) -> ("lion" "chases" "cow" "-"))
If something is green then it chases the dog.
((("something" "is" "green" "+")) -> ("something" "chases" "dog" "+"))
The cow chases the lion.
True
1
proof
[(triple1)]
("cow" "chases" "lion" "+")
triple1
The dog is not rough.
False
1
inv-proof
[(triple2)]
("dog" "is" "rough" "-")
triple2
The cow does not chase the dog.
Unknown
inv-rconc
[@1: The cow chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "dog" "-")
The dog chases the lion.
Unknown
random
[@0: The dog chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "lion" "+")
@0: The cow chases the lion.[(triple1)] The dog is rough.[(triple2)] The lion needs the dog.[(triple3)]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The lion needs the dog.
("lion" "needs" "dog" "+")
triple3