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