The cat chases the rabbit. The cat eats the rabbit. The cat is big. The cat is nice. The cat likes the rabbit. The rabbit chases the cat. The rabbit eats the cat. The rabbit is big. The rabbit is blue. The rabbit is green. The rabbit is nice. The rabbit likes the cat. If the rabbit chases the cat and the rabbit is round then the rabbit is nice. Blue people are round. If someone chases the cat and they are nice then they like the rabbit. If someone eats the cat and the cat chases the rabbit then they chase the cat. If someone is big and they chase the cat then the cat likes the rabbit. If someone eats the rabbit and the rabbit is nice then they are big.
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 nice.
("cat" "is" "nice" "+")
The cat likes the rabbit.
("cat" "likes" "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 blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
If the rabbit chases the cat and the rabbit is round then the rabbit is nice.
((("rabbit" "chases" "cat" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "is" "nice" "+"))
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone chases the cat and they are nice then they like the rabbit.
((("someone" "chases" "cat" "+") ("someone" "is" "nice" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone eats the cat and the cat chases the rabbit then they chase the cat.
((("someone" "eats" "cat" "+") ("cat" "chases" "rabbit" "+")) -> ("someone" "chases" "cat" "+"))
If someone is big and they chase the cat then the cat likes the rabbit.
((("someone" "is" "big" "+") ("someone" "chases" "cat" "+")) -> ("cat" "likes" "rabbit" "+"))
If someone eats the rabbit and the rabbit is nice then they are big.
((("someone" "eats" "rabbit" "+") ("rabbit" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
The rabbit is big.
True
1
proof
[(triple8)]
("rabbit" "is" "big" "+")
triple8
The rabbit is not nice.
False
1
inv-proof
[(triple11 OR ((triple6 ((triple9) -> rule2)) -> rule1) OR ((((triple7 triple1) -> rule4) ((triple9) -> rule2)) -> rule1))]
("rabbit" "is" "nice" "-")
triple11
((triple6 ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
((((triple7 triple1) -> (rule4 % int3)) ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int3
The rabbit is round.
True
2
proof
[(((triple9) -> rule2))]
("rabbit" "is" "round" "+")
((triple9) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit does not like the rabbit.
False
3
inv-proof
[(((triple6 triple11) -> rule3) OR ((((triple7 triple1) -> rule4) triple11) -> rule3) OR ((triple6 ((triple6 ((triple9) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple7 triple1) -> rule4) ((triple9) -> rule2)) -> rule1)) -> rule3) OR ((((triple7 triple1) -> rule4) ((triple6 ((triple9) -> rule2)) -> rule1)) -> rule3) OR ((((triple7 triple1) -> rule4) ((((triple7 triple1) -> rule4) ((triple9) -> rule2)) -> rule1)) -> rule3))]
("rabbit" "likes" "rabbit" "-")
((triple6 triple11) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
((((triple7 triple1) -> (rule4 % int2)) triple11) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
((triple6 ((triple6 ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
((triple6 ((((triple7 triple1) -> (rule4 % int4)) ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4
((((triple7 triple1) -> (rule4 % int4)) ((triple6 ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4
((((triple7 triple1) -> (rule4 % int4)) ((((triple7 triple1) -> (rule4 % int4)) ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "cat" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "round" "+")
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 eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The cat chases the rabbit.[(triple1)] The cat eats the rabbit.[(triple2)] The cat is big.[(triple3 OR ((triple2 triple11) -> rule6) OR ((triple2 ((triple6 ((triple9) -> rule2)) -> rule1)) -> rule6) OR ((triple2 ((((triple7 triple1) -> rule4) ((triple9) -> rule2)) -> rule1)) -> rule6))] The cat is nice.[(triple4)] The cat likes the rabbit.[(triple5 OR ((triple8 triple6) -> rule5) OR ((triple8 ((triple7 triple1) -> rule4)) -> rule5))] The rabbit chases the cat.[(triple6 OR ((triple7 triple1) -> rule4))] The rabbit eats the cat.[(triple7)] The rabbit is big.[(triple8)] The rabbit is blue.[(triple9)] The rabbit is green.[(triple10)] The rabbit is nice.[(triple11 OR ((triple6 ((triple9) -> rule2)) -> rule1) OR ((((triple7 triple1) -> rule4) ((triple9) -> rule2)) -> rule1))] The rabbit likes the cat.[(triple12)] @1: The rabbit is round.[(((triple9) -> rule2))] The rabbit likes the rabbit.[(((triple6 triple11) -> rule3) OR ((((triple7 triple1) -> rule4) triple11) -> rule3) OR ((triple6 ((triple6 ((triple9) -> rule2)) -> rule1)) -> rule3) OR ((triple6 ((((triple7 triple1) -> rule4) ((triple9) -> rule2)) -> rule1)) -> rule3) OR ((((triple7 triple1) -> rule4) ((triple6 ((triple9) -> rule2)) -> rule1)) -> rule3) OR ((((triple7 triple1) -> rule4) ((((triple7 triple1) -> rule4) ((triple9) -> rule2)) -> rule1)) -> rule3))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
((triple2 triple11) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
((triple2 ((triple6 ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
((triple2 ((((triple7 triple1) -> (rule4 % int4)) ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple5
((triple8 triple6) -> (rule5 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
((triple8 ((triple7 triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple6
((triple7 triple1) -> (rule4 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is green.
("rabbit" "is" "green" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
((triple6 ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
((((triple7 triple1) -> (rule4 % int3)) ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int3
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple12
The rabbit is round.
("rabbit" "is" "round" "+")
((triple9) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple6 triple11) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
((((triple7 triple1) -> (rule4 % int2)) triple11) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
((triple6 ((triple6 ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
((triple6 ((((triple7 triple1) -> (rule4 % int4)) ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4
((((triple7 triple1) -> (rule4 % int4)) ((triple6 ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4
((((triple7 triple1) -> (rule4 % int4)) ((((triple7 triple1) -> (rule4 % int4)) ((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int4