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