The cat does not chase the rabbit. The cat is not blue. The cat is not red. The cat is rough. The cat needs the rabbit. The cat does not see the rabbit. The rabbit chases the cat. The rabbit is big. The rabbit is green. The rabbit is red. The rabbit needs the cat. The rabbit sees the cat. If the rabbit needs the cat then the cat is big. If someone needs the cat and the cat does not chase the rabbit then the rabbit is big.
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
The cat is not blue.
("cat" "is" "blue" "-")
The cat is not red.
("cat" "is" "red" "-")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If the rabbit needs the cat then the cat is big.
((("rabbit" "needs" "cat" "+")) -> ("cat" "is" "big" "+"))
If someone needs the cat and the cat does not chase the rabbit then the rabbit is big.
((("someone" "needs" "cat" "+") ("cat" "chases" "rabbit" "~")) -> ("rabbit" "is" "big" "+"))
The cat is rough.
True
1
proof
[(triple4)]
("cat" "is" "rough" "+")
triple4
The rabbit is not red.
False
1
inv-proof
[(triple10)]
("rabbit" "is" "red" "-")
triple10
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The cat does not chase the rabbit.[(triple1)] The cat does not see the rabbit.[(triple6)] The cat is not blue.[(triple2)] The cat is not red.[(triple3)] The cat is rough.[(triple4)] The cat needs the rabbit.[(triple5)] The rabbit chases the cat.[(triple7)] The rabbit is big.[(triple8 OR ((triple11 triple1) -> rule2))] The rabbit is green.[(triple9)] The rabbit is red.[(triple10)] The rabbit needs the cat.[(triple11)] The rabbit sees the cat.[(triple12)] @1: The cat is big.[(((triple11) -> rule1))]
The cat does not chase the rabbit.
("cat" "chases" "rabbit" "-")
triple1
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
triple6
The cat is not blue.
("cat" "is" "blue" "-")
triple2
The cat is not red.
("cat" "is" "red" "-")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple5
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
((triple11 triple1) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple10
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple11
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple12
The cat is big.
("cat" "is" "big" "+")
((triple11) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1