The lion needs the mouse. The mouse sees the lion. If someone sees the lion then the lion does not chase the mouse. If someone chases the mouse then they do not see the mouse.
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If someone sees the lion then the lion does not chase the mouse.
((("someone" "sees" "lion" "+")) -> ("lion" "chases" "mouse" "-"))
If someone chases the mouse then they do not see the mouse.
((("someone" "chases" "mouse" "+")) -> ("someone" "sees" "mouse" "-"))
The mouse sees the lion.
True
1
proof
[(triple2)]
("mouse" "sees" "lion" "+")
triple2
The lion does not need the mouse.
False
1
inv-proof
[(triple1)]
("lion" "needs" "mouse" "-")
triple1
The lion does not chase the mouse.
True
2
proof
[(((triple2) -> rule1))]
("lion" "chases" "mouse" "-")
((triple2) -> (rule1 % int1))
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int1
The lion chases the mouse.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "chases" "mouse" "+")
((triple2) -> (rule1 % int1))
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int1
The mouse does not chase the lion.
Unknown
inv-random
[@0: The mouse chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "lion" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The lion needs the mouse.[(triple1)] The mouse sees the lion.[(triple2)] @1: The lion does not chase the mouse.[(((triple2) -> rule1))]
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple2
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
((triple2) -> (rule1 % int1))
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int1