The cat chases the rabbit. The cat eats the rabbit. The cat is big. The cat is kind. The cat is red. The cat is rough. The cat is young. The cat needs the rabbit. The rabbit chases the cat. The rabbit eats the cat. The rabbit is big. The rabbit is red. The rabbit is rough. The rabbit is not young. The rabbit needs the cat. If the cat is young and the cat does not eat the rabbit then the cat does not chase the rabbit. If the cat eats the rabbit then the rabbit is red. If the rabbit is red then the rabbit eats the cat. If something is rough and red then it chases the rabbit. If the cat eats the rabbit and the cat chases the rabbit then the cat needs the rabbit. If the cat does not need the rabbit then the cat is not kind.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is not young.
("rabbit" "is" "young" "-")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If the cat is young and the cat does not eat the rabbit then the cat does not chase the rabbit.
((("cat" "is" "young" "+") ("cat" "eats" "rabbit" "~")) -> ("cat" "chases" "rabbit" "-"))
If the cat eats the rabbit then the rabbit is red.
((("cat" "eats" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If the rabbit is red then the rabbit eats the cat.
((("rabbit" "is" "red" "+")) -> ("rabbit" "eats" "cat" "+"))
If something is rough and red then it chases the rabbit.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "chases" "rabbit" "+"))
If the cat eats the rabbit and the cat chases the rabbit then the cat needs the rabbit.
((("cat" "eats" "rabbit" "+") ("cat" "chases" "rabbit" "+")) -> ("cat" "needs" "rabbit" "+"))
If the cat does not need the rabbit then the cat is not kind.
((("cat" "needs" "rabbit" "~")) -> ("cat" "is" "kind" "-"))
The rabbit is not young.
True
1
proof
[(triple14)]
("rabbit" "is" "young" "-")
triple14
The rabbit does not eat the cat.
False
1
inv-proof
[(triple10 OR ((triple12) -> rule3) OR ((((triple2) -> rule2)) -> rule3))]
("rabbit" "eats" "cat" "-")
triple10
((triple12) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit chases the rabbit.
True
3
proof
[(((triple13 triple12) -> rule4) OR ((triple13 ((triple2) -> rule2)) -> rule4))]
("rabbit" "chases" "rabbit" "+")
((triple13 triple12) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((triple13 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit does not chase the rabbit.
False
3
inv-proof
[(((triple13 triple12) -> rule4) OR ((triple13 ((triple2) -> rule2)) -> rule4))]
("rabbit" "chases" "rabbit" "-")
((triple13 triple12) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((triple13 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
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 cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat chases the rabbit.[(triple1 OR ((triple6 triple5) -> rule4))] The cat eats the rabbit.[(triple2)] The cat is big.[(triple3)] The cat is kind.[(triple4)] The cat is red.[(triple5)] The cat is rough.[(triple6)] The cat is young.[(triple7)] The cat needs the rabbit.[(triple8 OR ((triple2 triple1) -> rule5) OR ((triple2 ((triple6 triple5) -> rule4)) -> rule5))] The rabbit chases the cat.[(triple9)] The rabbit eats the cat.[(triple10 OR ((triple12) -> rule3) OR ((((triple2) -> rule2)) -> rule3))] The rabbit is big.[(triple11)] The rabbit is not young.[(triple14)] The rabbit is red.[(triple12 OR ((triple2) -> rule2))] The rabbit is rough.[(triple13)] The rabbit needs the cat.[(triple15)] @1: The rabbit chases the rabbit.[(((triple13 triple12) -> rule4) OR ((triple13 ((triple2) -> rule2)) -> rule4))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
((triple6 triple5) -> (rule4 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat is young.
("cat" "is" "young" "+")
triple7
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple8
((triple2 triple1) -> (rule5 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
((triple2 ((triple6 triple5) -> (rule4 % int2))) -> (rule5 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple9
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple10
((triple12) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The rabbit is not young.
("rabbit" "is" "young" "-")
triple14
The rabbit is red.
("rabbit" "is" "red" "+")
triple12
((triple2) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple13
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple15
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple13 triple12) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((triple13 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2