The cat does not see the lion. The lion sees the cat. If someone chases the lion then they are green. If someone is nice then they are green. If someone chases the lion and they see the lion then they are rough.
The cat does not see the lion.
("cat" "sees" "lion" "-")
The lion sees the cat.
("lion" "sees" "cat" "+")
If someone chases the lion then they are green.
((("someone" "chases" "lion" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone chases the lion and they see the lion then they are rough.
((("someone" "chases" "lion" "+") ("someone" "sees" "lion" "+")) -> ("someone" "is" "rough" "+"))
The cat does not see the lion.
True
1
proof
[(triple1)]
("cat" "sees" "lion" "-")
triple1
The lion does not see the cat.
False
1
inv-proof
[(triple2)]
("lion" "sees" "cat" "-")
triple2
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "green" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The cat does not see the lion.[(triple1)] The lion sees the cat.[(triple2)]
The cat does not see the lion.
("cat" "sees" "lion" "-")
triple1
The lion sees the cat.
("lion" "sees" "cat" "+")
triple2