The bear chases the lion. The bear chases the mouse. The bear does not need the lion. The lion eats the bear. The mouse chases the lion. The mouse eats the lion. The mouse is green. If the bear is kind then the bear is not green. If something eats the mouse and the mouse eats the bear then the bear needs the lion. If something needs the lion and the lion is not young then the lion needs the bear. If the bear needs the lion then the lion does not need the mouse. If something chases the bear and it is young then it does not need the mouse. If something is green then it needs the mouse. If the lion is round and the lion does not chase the mouse then the mouse is green. If the lion needs the mouse and the lion chases the bear then the mouse chases the lion.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear does not need the lion.
("bear" "needs" "lion" "-")
The lion eats the bear.
("lion" "eats" "bear" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is green.
("mouse" "is" "green" "+")
If the bear is kind then the bear is not green.
((("bear" "is" "kind" "+")) -> ("bear" "is" "green" "-"))
If something eats the mouse and the mouse eats the bear then the bear needs the lion.
((("something" "eats" "mouse" "+") ("mouse" "eats" "bear" "+")) -> ("bear" "needs" "lion" "+"))
If something needs the lion and the lion is not young then the lion needs the bear.
((("something" "needs" "lion" "+") ("lion" "is" "young" "~")) -> ("lion" "needs" "bear" "+"))
If the bear needs the lion then the lion does not need the mouse.
((("bear" "needs" "lion" "+")) -> ("lion" "needs" "mouse" "-"))
If something chases the bear and it is young then it does not need the mouse.
((("something" "chases" "bear" "+") ("something" "is" "young" "+")) -> ("something" "needs" "mouse" "-"))
If something is green then it needs the mouse.
((("something" "is" "green" "+")) -> ("something" "needs" "mouse" "+"))
If the lion is round and the lion does not chase the mouse then the mouse is green.
((("lion" "is" "round" "+") ("lion" "chases" "mouse" "~")) -> ("mouse" "is" "green" "+"))
If the lion needs the mouse and the lion chases the bear then the mouse chases the lion.
((("lion" "needs" "mouse" "+") ("lion" "chases" "bear" "+")) -> ("mouse" "chases" "lion" "+"))
The mouse chases the lion.
True
1
proof
[(triple5)]
("mouse" "chases" "lion" "+")
triple5
The mouse is not green.
False
1
inv-proof
[(triple7)]
("mouse" "is" "green" "-")
triple7
The lion does not need the bear.
Unknown
inv-rconc
[@1: The lion needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "needs" "bear" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The bear chases the lion.[(triple1)] The bear chases the mouse.[(triple2)] The bear does not need the lion.[(triple3)] The lion eats the bear.[(triple4)] The mouse chases the lion.[(triple5)] The mouse eats the lion.[(triple6)] The mouse is green.[(triple7)] @1: The mouse needs the mouse.[(((triple7) -> rule6))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple2
The bear does not need the lion.
("bear" "needs" "lion" "-")
triple3
The lion eats the bear.
("lion" "eats" "bear" "+")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple5
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple7) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1