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