The cat does not eat the rabbit. The cat is not blue. The cat is green. The cat is kind. The cat is rough. The cat is round. The cat needs the rabbit. The cat sees the rabbit. The rabbit eats the cat. The rabbit is blue. The rabbit is green. The rabbit is kind. The rabbit is rough. The rabbit is round. The rabbit needs the cat. The rabbit sees the cat. If something needs the rabbit then it is not blue. If something eats the cat then it is rough. If something eats the rabbit then the rabbit is kind. If something is rough then it sees the cat. If something sees the rabbit and it is not round then it does not see the cat. If something needs the cat and the cat does not see the rabbit then the cat eats the rabbit.
The cat does not eat the rabbit.
("cat" "eats" "rabbit" "-")
The cat is not blue.
("cat" "is" "blue" "-")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If something needs the rabbit then it is not blue.
((("something" "needs" "rabbit" "+")) -> ("something" "is" "blue" "-"))
If something eats the cat then it is rough.
((("something" "eats" "cat" "+")) -> ("something" "is" "rough" "+"))
If something eats the rabbit then the rabbit is kind.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
If something is rough then it sees the cat.
((("something" "is" "rough" "+")) -> ("something" "sees" "cat" "+"))
If something sees the rabbit and it is not round then it does not see the cat.
((("something" "sees" "rabbit" "+") ("something" "is" "round" "~")) -> ("something" "sees" "cat" "-"))
If something needs the cat and the cat does not see the rabbit then the cat eats the rabbit.
((("something" "needs" "cat" "+") ("cat" "sees" "rabbit" "~")) -> ("cat" "eats" "rabbit" "+"))
The rabbit is green.
True
1
proof
[(triple11)]
("rabbit" "is" "green" "+")
triple11
The rabbit does not see the cat.
False
1
inv-proof
[(triple16 OR ((triple13) -> rule4) OR ((((triple9) -> rule2)) -> rule4))]
("rabbit" "sees" "cat" "-")
triple16
((triple13) -> (rule4 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cat sees the cat.
True
2
proof
[(((triple5) -> rule4))]
("cat" "sees" "cat" "+")
((triple5) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple5) -> rule4))]
("cat" "sees" "cat" "-")
((triple5) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The cat does not eat the rabbit.[(triple1)] The cat is green.[(triple3)] The cat is kind.[(triple4)] The cat is not blue.[(triple2 OR ((triple7) -> rule1))] The cat is rough.[(triple5)] The cat is round.[(triple6)] The cat needs the rabbit.[(triple7)] The cat sees the rabbit.[(triple8)] The rabbit eats the cat.[(triple9)] The rabbit is blue.[(triple10)] The rabbit is green.[(triple11)] The rabbit is kind.[(triple12)] The rabbit is rough.[(triple13 OR ((triple9) -> rule2))] The rabbit is round.[(triple14)] The rabbit needs the cat.[(triple15)] The rabbit sees the cat.[(triple16 OR ((triple13) -> rule4) OR ((((triple9) -> rule2)) -> rule4))] @1: The cat sees the cat.[(((triple5) -> rule4))]
The cat does not eat the rabbit.
("cat" "eats" "rabbit" "-")
triple1
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is not blue.
("cat" "is" "blue" "-")
triple2
((triple7) -> (rule1 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple7
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple8
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple9
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
triple11
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple12
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple13
((triple9) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
triple14
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple15
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple16
((triple13) -> (rule4 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple5) -> (rule4 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1