The bear sees the lion. The lion chases the bear. If the bear is big and the bear sees the lion then the lion visits the bear. If the lion chases the bear and the bear visits the lion then the bear is green. If something is rough and it does not visit the bear then the bear is nice.
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
If the bear is big and the bear sees the lion then the lion visits the bear.
((("bear" "is" "big" "+") ("bear" "sees" "lion" "+")) -> ("lion" "visits" "bear" "+"))
If the lion chases the bear and the bear visits the lion then the bear is green.
((("lion" "chases" "bear" "+") ("bear" "visits" "lion" "+")) -> ("bear" "is" "green" "+"))
If something is rough and it does not visit the bear then the bear is nice.
((("something" "is" "rough" "+") ("something" "visits" "bear" "~")) -> ("bear" "is" "nice" "+"))
The lion chases the bear.
True
1
proof
[(triple2)]
("lion" "chases" "bear" "+")
triple2
The lion does not chase the bear.
False
1
inv-proof
[(triple2)]
("lion" "chases" "bear" "-")
triple2
The lion does not visit the bear.
Unknown
inv-rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "bear" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
@0: The bear sees the lion.[(triple1)] The lion chases the bear.[(triple2)]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The lion chases the bear.
("lion" "chases" "bear" "+")
triple2