The cat is big. The cat is cold. The cat is green. The cat is rough. The cat is round. The cat needs the rabbit. The rabbit eats the cat. The rabbit is cold. The rabbit likes the cat. The rabbit needs the cat. If something is green then it does not need the cat. If something likes the rabbit and the rabbit needs the cat then the rabbit is not big.
The cat is big.
("cat" "is" "big" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something is green then it does not need the cat.
((("something" "is" "green" "+")) -> ("something" "needs" "cat" "-"))
If something likes the rabbit and the rabbit needs the cat then the rabbit is not big.
((("something" "likes" "rabbit" "+") ("rabbit" "needs" "cat" "+")) -> ("rabbit" "is" "big" "-"))
The cat is big.
True
1
proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The rabbit does not eat the cat.
False
1
inv-proof
[(triple7)]
("rabbit" "eats" "cat" "-")
triple7
The cat does not need the cat.
True
2
proof
[(((triple3) -> rule1))]
("cat" "needs" "cat" "-")
((triple3) -> (rule1 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat needs the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "needs" "cat" "+")
((triple3) -> (rule1 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The cat does not eat the rabbit.
Unknown
inv-random
[@0: The cat eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The cat is big.[(triple1)] The cat is cold.[(triple2)] The cat is green.[(triple3)] The cat is rough.[(triple4)] The cat is round.[(triple5)] The cat needs the rabbit.[(triple6)] The rabbit eats the cat.[(triple7)] The rabbit is cold.[(triple8)] The rabbit likes the cat.[(triple9)] The rabbit needs the cat.[(triple10)] @1: The cat does not need the cat.[(((triple3) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple9
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple10
The cat does not need the cat.
("cat" "needs" "cat" "-")
((triple3) -> (rule1 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1