The dog needs the lion. The lion is red. The lion needs the dog. The lion sees the dog. The lion visits the mouse. The mouse is young. The mouse needs the dog. The mouse needs the lion. The mouse sees the lion. The mouse does not visit the dog. If something needs the mouse and it is not young then the mouse needs the lion.
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
If something needs the mouse and it is not young then the mouse needs the lion.
((("something" "needs" "mouse" "+") ("something" "is" "young" "~")) -> ("mouse" "needs" "lion" "+"))
The mouse needs the lion.
True
1
proof
[(triple8)]
("mouse" "needs" "lion" "+")
triple8
The mouse does not need the dog.
False
1
inv-proof
[(triple7)]
("mouse" "needs" "dog" "-")
triple7
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The dog needs the lion.[(triple1)] The lion is red.[(triple2)] The lion needs the dog.[(triple3)] The lion sees the dog.[(triple4)] The lion visits the mouse.[(triple5)] The mouse does not visit the dog.[(triple10)] The mouse is young.[(triple6)] The mouse needs the dog.[(triple7)] The mouse needs the lion.[(triple8)] The mouse sees the lion.[(triple9)]
The dog needs the lion.
("dog" "needs" "lion" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion needs the dog.
("lion" "needs" "dog" "+")
triple3
The lion sees the dog.
("lion" "sees" "dog" "+")
triple4
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple5
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
triple10
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple7
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple8
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple9