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