The lion chases the mouse. The lion is blue. The lion is cold. The lion is not nice. The lion is not round. The lion is young. The lion sees the mouse. The lion does not visit the mouse. The mouse does not chase the lion. The mouse is not cold. The mouse is not nice. The mouse is round. The mouse is not young. The mouse sees the lion. The mouse does not visit the lion. If the lion visits the mouse and the lion is blue then the mouse does not visit the lion.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion is not round.
("lion" "is" "round" "-")
The lion is young.
("lion" "is" "young" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
The mouse is not cold.
("mouse" "is" "cold" "-")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
If the lion visits the mouse and the lion is blue then the mouse does not visit the lion.
((("lion" "visits" "mouse" "+") ("lion" "is" "blue" "+")) -> ("mouse" "visits" "lion" "-"))
The lion chases the mouse.
True
1
proof
[(triple1)]
("lion" "chases" "mouse" "+")
triple1
The mouse is cold.
False
1
inv-proof
[(triple10)]
("mouse" "is" "cold" "+")
triple10
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 mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The lion chases the mouse.[(triple1)] The lion does not visit the mouse.[(triple8)] The lion is blue.[(triple2)] The lion is cold.[(triple3)] The lion is not nice.[(triple4)] The lion is not round.[(triple5)] The lion is young.[(triple6)] The lion sees the mouse.[(triple7)] The mouse does not chase the lion.[(triple9)] The mouse does not visit the lion.[(triple15)] The mouse is not cold.[(triple10)] The mouse is not nice.[(triple11)] The mouse is not young.[(triple13)] The mouse is round.[(triple12)] The mouse sees the lion.[(triple14)]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
triple8
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion is not nice.
("lion" "is" "nice" "-")
triple4
The lion is not round.
("lion" "is" "round" "-")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple7
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
triple9
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
triple15
The mouse is not cold.
("mouse" "is" "cold" "-")
triple10
The mouse is not nice.
("mouse" "is" "nice" "-")
triple11
The mouse is not young.
("mouse" "is" "young" "-")
triple13
The mouse is round.
("mouse" "is" "round" "+")
triple12
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple14