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