The bear visits the lion. The lion chases the mouse. The mouse chases the lion. If something is round and young then it chases the bear. If something likes the lion and it is rough then the lion visits the bear.
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
If something is round and young then it chases the bear.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "chases" "bear" "+"))
If something likes the lion and it is rough then the lion visits the bear.
((("something" "likes" "lion" "+") ("something" "is" "rough" "+")) -> ("lion" "visits" "bear" "+"))
The lion chases the mouse.
True
1
proof
[(triple2)]
("lion" "chases" "mouse" "+")
triple2
The mouse does not chase the lion.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "lion" "-")
triple3
The lion does not chase the bear.
Unknown
inv-rconc
[@1: The lion chases the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "chases" "bear" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The bear visits the lion.[(triple1)] The lion chases the mouse.[(triple2)] The mouse chases the lion.[(triple3)]
The bear visits the lion.
("bear" "visits" "lion" "+")
triple1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3