The cat chases the mouse. The cat chases the tiger. The cat is green. The cat is red. The cat is young. The cat does not need the mouse. The cat needs the tiger. The cat sees the mouse. The cat sees the tiger. The mouse is cold. The mouse is green. The mouse is young. The mouse does not need the cat. The mouse needs the tiger. The tiger is young. The tiger needs the mouse. If someone chases the tiger and the tiger does not chase the mouse then the mouse is green.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is young.
("cat" "is" "young" "+")
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If someone chases the tiger and the tiger does not chase the mouse then the mouse is green.
((("someone" "chases" "tiger" "+") ("tiger" "chases" "mouse" "~")) -> ("mouse" "is" "green" "+"))
The cat chases the mouse.
True
1
proof
[(triple1)]
("cat" "chases" "mouse" "+")
triple1
The cat does not chase the mouse.
False
1
inv-proof
[(triple1)]
("cat" "chases" "mouse" "-")
triple1
The tiger does not see the mouse.
Unknown
inv-random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "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 cat chases the mouse.[(triple1)] The cat chases the tiger.[(triple2)] The cat does not need the mouse.[(triple6)] The cat is green.[(triple3)] The cat is red.[(triple4)] The cat is young.[(triple5)] The cat needs the tiger.[(triple7)] The cat sees the mouse.[(triple8)] The cat sees the tiger.[(triple9)] The mouse does not need the cat.[(triple13)] The mouse is cold.[(triple10)] The mouse is green.[(triple11)] The mouse is young.[(triple12)] The mouse needs the tiger.[(triple14)] The tiger is young.[(triple15)] The tiger needs the mouse.[(triple16)]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
triple6
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple7
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple8
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple9
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
triple13
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse is young.
("mouse" "is" "young" "+")
triple12
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple14
The tiger is young.
("tiger" "is" "young" "+")
triple15
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple16