The cat visits the lion. The cow visits the lion. The lion is not young. If the cow eats the lion then the cow visits the lion. If the cow is kind and the cow chases the cat then the cow visits the lion. If someone chases the lion then they chase the cow.
The cat visits the lion.
("cat" "visits" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is not young.
("lion" "is" "young" "-")
If the cow eats the lion then the cow visits the lion.
((("cow" "eats" "lion" "+")) -> ("cow" "visits" "lion" "+"))
If the cow is kind and the cow chases the cat then the cow visits the lion.
((("cow" "is" "kind" "+") ("cow" "chases" "cat" "+")) -> ("cow" "visits" "lion" "+"))
If someone chases the lion then they chase the cow.
((("someone" "chases" "lion" "+")) -> ("someone" "chases" "cow" "+"))
The lion is not young.
True
1
proof
[(triple3)]
("lion" "is" "young" "-")
triple3
The cat does not visit the lion.
False
1
inv-proof
[(triple1)]
("cat" "visits" "lion" "-")
triple1
The cat does not chase the cow.
Unknown
inv-rconc
[@1: The cat chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "cow" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat visits the lion.[(triple1)] The cow visits the lion.[(triple2)] The lion is not young.[(triple3)]
The cat visits the lion.
("cat" "visits" "lion" "+")
triple1
The cow visits the lion.
("cow" "visits" "lion" "+")
triple2
The lion is not young.
("lion" "is" "young" "-")
triple3