The cat chases the rabbit. The cat is big. The cat likes the rabbit. The rabbit chases the cat. The rabbit is big. The rabbit is rough. The rabbit likes the cat. If the cat likes the rabbit then the cat eats the rabbit. If something likes the rabbit then the rabbit likes the cat. If something eats the cat then the cat chases the rabbit. If something eats the rabbit then it eats the cat. If the cat is rough then the cat is green. If something eats the rabbit and it is big then it chases the rabbit. If something chases the cat and the cat is rough then it is green. If something eats the cat and it chases the rabbit then the rabbit eats the cat.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is big.
("cat" "is" "big" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
If the cat likes the rabbit then the cat eats the rabbit.
((("cat" "likes" "rabbit" "+")) -> ("cat" "eats" "rabbit" "+"))
If something likes the rabbit then the rabbit likes the cat.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "cat" "+"))
If something eats the cat then the cat chases the rabbit.
((("something" "eats" "cat" "+")) -> ("cat" "chases" "rabbit" "+"))
If something eats the rabbit then it eats the cat.
((("something" "eats" "rabbit" "+")) -> ("something" "eats" "cat" "+"))
If the cat is rough then the cat is green.
((("cat" "is" "rough" "+")) -> ("cat" "is" "green" "+"))
If something eats the rabbit and it is big then it chases the rabbit.
((("something" "eats" "rabbit" "+") ("something" "is" "big" "+")) -> ("something" "chases" "rabbit" "+"))
If something chases the cat and the cat is rough then it is green.
((("something" "chases" "cat" "+") ("cat" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something eats the cat and it chases the rabbit then the rabbit eats the cat.
((("something" "eats" "cat" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "eats" "cat" "+"))
The rabbit chases the cat.
True
1
proof
[(triple4)]
("rabbit" "chases" "cat" "+")
triple4
The cat is not big.
False
1
inv-proof
[(triple2)]
("cat" "is" "big" "-")
triple2
The cat eats the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("cat" "eats" "rabbit" "+")
((triple3) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat does not eat the rabbit.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "eats" "rabbit" "-")
((triple3) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat eats the cat.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("cat" "eats" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
The cat does not eat the cat.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("cat" "eats" "cat" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
The rabbit eats the cat.
True
5
proof
[(((((((triple3) -> rule1)) -> rule4) triple1) -> rule8) OR ((((((triple3) -> rule1)) -> rule4) ((((triple3) -> rule1) triple2) -> rule6)) -> rule8) OR ((((((triple3) -> rule1)) -> rule4) ((((((triple3) -> rule1)) -> rule4)) -> rule3)) -> rule8))]
("rabbit" "eats" "cat" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int3
((((((triple3) -> (rule1 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule1 % int4)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int4
((((((triple3) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple3) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int4
The rabbit does not eat the cat.
False
5
inv-proof
[(((((((triple3) -> rule1)) -> rule4) triple1) -> rule8) OR ((((((triple3) -> rule1)) -> rule4) ((((triple3) -> rule1) triple2) -> rule6)) -> rule8) OR ((((((triple3) -> rule1)) -> rule4) ((((((triple3) -> rule1)) -> rule4)) -> rule3)) -> rule8))]
("rabbit" "eats" "cat" "-")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int3
((((((triple3) -> (rule1 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule1 % int4)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int4
((((((triple3) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple3) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int4
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "green" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "green" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
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 cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
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 is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The cat chases the rabbit.[(triple1 OR ((((triple3) -> rule1) triple2) -> rule6) OR ((((((triple3) -> rule1)) -> rule4)) -> rule3))] The cat is big.[(triple2)] The cat likes the rabbit.[(triple3)] The rabbit chases the cat.[(triple4)] The rabbit is big.[(triple5)] The rabbit is rough.[(triple6)] The rabbit likes the cat.[(triple7 OR ((triple3) -> rule2))] @1: The cat eats the rabbit.[(((triple3) -> rule1))] @2: The cat eats the cat.[(((((triple3) -> rule1)) -> rule4))] @3: The rabbit eats the cat.[(((((((triple3) -> rule1)) -> rule4) triple1) -> rule8) OR ((((((triple3) -> rule1)) -> rule4) ((((triple3) -> rule1) triple2) -> rule6)) -> rule8) OR ((((((triple3) -> rule1)) -> rule4) ((((((triple3) -> rule1)) -> rule4)) -> rule3)) -> rule8))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
((((triple3) -> (rule1 % int2)) triple2) -> (rule6 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int3
The cat is big.
("cat" "is" "big" "+")
triple2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple4
The rabbit is big.
("rabbit" "is" "big" "+")
triple5
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple6
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple7
((triple3) -> (rule2 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
((triple3) -> (rule1 % int1))
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int2
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int3
((((((triple3) -> (rule1 % int4))) -> (rule4 % int3)) ((((triple3) -> (rule1 % int4)) triple2) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int4
((((((triple3) -> (rule1 % int4))) -> (rule4 % int3)) ((((((triple3) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
int4