The cat is not big. The cat is blue. The cat is green. The cat is not kind. The cat likes the rabbit. The cat needs the rabbit. The cat sees the rabbit. The rabbit is big. The rabbit is green. The rabbit likes the cat. The rabbit does not need the cat. The rabbit does not see the cat. If something needs the cat then the cat needs the rabbit. If something sees the rabbit and the rabbit is not big then the rabbit sees the cat. If something sees the cat and the cat sees the rabbit then the cat is not big.
The cat is not big.
("cat" "is" "big" "-")
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
If something needs the cat then the cat needs the rabbit.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
If something sees the rabbit and the rabbit is not big then the rabbit sees the cat.
((("something" "sees" "rabbit" "+") ("rabbit" "is" "big" "~")) -> ("rabbit" "sees" "cat" "+"))
If something sees the cat and the cat sees the rabbit then the cat is not big.
((("something" "sees" "cat" "+") ("cat" "sees" "rabbit" "+")) -> ("cat" "is" "big" "-"))
The cat sees the rabbit.
True
1
proof
[(triple7)]
("cat" "sees" "rabbit" "+")
triple7
The cat does not need the rabbit.
False
1
inv-proof
[(triple6)]
("cat" "needs" "rabbit" "-")
triple6
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is blue.[(triple2)] The cat is green.[(triple3)] The cat is not big.[(triple1)] The cat is not kind.[(triple4)] The cat likes the rabbit.[(triple5)] The cat needs the rabbit.[(triple6)] The cat sees the rabbit.[(triple7)] The rabbit does not need the cat.[(triple11)] The rabbit does not see the cat.[(triple12)] The rabbit is big.[(triple8)] The rabbit is green.[(triple9)] The rabbit likes the cat.[(triple10)]
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is not big.
("cat" "is" "big" "-")
triple1
The cat is not kind.
("cat" "is" "kind" "-")
triple4
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple7
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
triple11
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
triple12
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple10