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