The cat is big. The cat likes the cow. The cat visits the rabbit. The cow is green. The cow likes the cat. The rabbit chases the cat. The rabbit is nice. The rabbit likes the cat. The rabbit likes the cow. The rabbit visits the cat. If something chases the rabbit then the rabbit chases the cow. If something chases the cow then the cow is kind. If something is nice and it chases the cat then it chases the rabbit. If the cow visits the cat and the cat visits the rabbit then the cow chases the cat. If something visits the cow and the cow chases the cat then the cat likes the cow. If something visits the cat then it likes the cat.
The cat is big.
("cat" "is" "big" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The cow is green.
("cow" "is" "green" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If something chases the rabbit then the rabbit chases the cow.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "cow" "+"))
If something chases the cow then the cow is kind.
((("something" "chases" "cow" "+")) -> ("cow" "is" "kind" "+"))
If something is nice and it chases the cat then it chases the rabbit.
((("something" "is" "nice" "+") ("something" "chases" "cat" "+")) -> ("something" "chases" "rabbit" "+"))
If the cow visits the cat and the cat visits the rabbit then the cow chases the cat.
((("cow" "visits" "cat" "+") ("cat" "visits" "rabbit" "+")) -> ("cow" "chases" "cat" "+"))
If something visits the cow and the cow chases the cat then the cat likes the cow.
((("something" "visits" "cow" "+") ("cow" "chases" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If something visits the cat then it likes the cat.
((("something" "visits" "cat" "+")) -> ("something" "likes" "cat" "+"))
The rabbit chases the cat.
True
1
proof
[(triple6)]
("rabbit" "chases" "cat" "+")
triple6
The rabbit does not chase the cat.
False
1
inv-proof
[(triple6)]
("rabbit" "chases" "cat" "-")
triple6
The rabbit chases the rabbit.
True
3
proof
[(((triple7 triple6) -> rule3))]
("rabbit" "chases" "rabbit" "+")
((triple7 triple6) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
3
inv-proof
[(((triple7 triple6) -> rule3))]
("rabbit" "chases" "rabbit" "-")
((triple7 triple6) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the cow.
True
4
proof
[(((((triple7 triple6) -> rule3)) -> rule1))]
("rabbit" "chases" "cow" "+")
((((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit does not chase the cow.
False
4
inv-proof
[(((((triple7 triple6) -> rule3)) -> rule1))]
("rabbit" "chases" "cow" "-")
((((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The cow is kind.
True
5
proof
[(((((((triple7 triple6) -> rule3)) -> rule1)) -> rule2))]
("cow" "is" "kind" "+")
((((((triple7 triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The cow is not kind.
False
5
inv-proof
[(((((((triple7 triple6) -> rule3)) -> rule1)) -> rule2))]
("cow" "is" "kind" "-")
((((((triple7 triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The cow does not chase the cat.
Unknown
inv-rconc
[@1: The cow chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cat" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "likes" "cat" "+")
The cow does not chase the rabbit.
Unknown
inv-rconc
[@1: The cow chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "chases" "rabbit" "-")
The cat chases the rabbit.
Unknown
rconc
[@1: The cat chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cat is big.[(triple1)] The cat likes the cow.[(triple2)] The cat visits the rabbit.[(triple3)] The cow is green.[(triple4)] The cow likes the cat.[(triple5)] The rabbit chases the cat.[(triple6)] The rabbit is nice.[(triple7)] The rabbit likes the cat.[(triple8 OR ((triple10) -> rule6))] The rabbit likes the cow.[(triple9)] The rabbit visits the cat.[(triple10)] @1: The rabbit chases the rabbit.[(((triple7 triple6) -> rule3))] @2: The rabbit chases the cow.[(((((triple7 triple6) -> rule3)) -> rule1))] @3: The cow is kind.[(((((((triple7 triple6) -> rule3)) -> rule1)) -> rule2))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
triple4
The cow likes the cat.
("cow" "likes" "cat" "+")
triple5
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple8
((triple10) -> (rule6 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple9
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple10
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple7 triple6) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((((triple7 triple6) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
((((((triple7 triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3