The lion chases the mouse. The lion is green. The lion is not nice. The lion is red. The lion is round. The lion needs the mouse. The lion visits the mouse. The mouse chases the lion. The mouse is cold. The mouse is nice. The mouse is round. The mouse visits the lion. If the mouse is nice and the mouse is round then the mouse needs the lion. If the lion needs the mouse and the lion does not chase the mouse then the mouse does not need the lion.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If the mouse is nice and the mouse is round then the mouse needs the lion.
((("mouse" "is" "nice" "+") ("mouse" "is" "round" "+")) -> ("mouse" "needs" "lion" "+"))
If the lion needs the mouse and the lion does not chase the mouse then the mouse does not need the lion.
((("lion" "needs" "mouse" "+") ("lion" "chases" "mouse" "~")) -> ("mouse" "needs" "lion" "-"))
The lion needs the mouse.
True
1
proof
[(triple6)]
("lion" "needs" "mouse" "+")
triple6
The lion does not need the mouse.
False
1
inv-proof
[(triple6)]
("lion" "needs" "mouse" "-")
triple6
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The lion chases the mouse.[(triple1)] The lion is green.[(triple2)] The lion is not nice.[(triple3)] The lion is red.[(triple4)] The lion is round.[(triple5)] The lion needs the mouse.[(triple6)] The lion visits the mouse.[(triple7)] The mouse chases the lion.[(triple8)] The mouse is cold.[(triple9)] The mouse is nice.[(triple10)] The mouse is round.[(triple11)] The mouse visits the lion.[(triple12)] @1: The mouse needs the lion.[(((triple10 triple11) -> rule1))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is not nice.
("lion" "is" "nice" "-")
triple3
The lion is red.
("lion" "is" "red" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple6
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple7
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple8
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse is nice.
("mouse" "is" "nice" "+")
triple10
The mouse is round.
("mouse" "is" "round" "+")
triple11
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple12
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple10 triple11) -> (rule1 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1