The cat chases the cow. The cat is kind. The cow chases the cat. The cow chases the rabbit. The cow eats the cat. The cow eats the rabbit. The cow is green. The cow needs the cat. The rabbit eats the cat. The rabbit is kind. If someone eats the rabbit and the rabbit needs the cat then the rabbit eats the cat. If someone eats the cat and the cat chases the cow then they are green. If the cat chases the cow then the cow chases the rabbit. If someone is green then they are big. If someone needs the cow then the cow needs the rabbit. If someone eats the cow then the cow chases the rabbit.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is green.
("cow" "is" "green" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
If someone eats the rabbit and the rabbit needs the cat then the rabbit eats the cat.
((("someone" "eats" "rabbit" "+") ("rabbit" "needs" "cat" "+")) -> ("rabbit" "eats" "cat" "+"))
If someone eats the cat and the cat chases the cow then they are green.
((("someone" "eats" "cat" "+") ("cat" "chases" "cow" "+")) -> ("someone" "is" "green" "+"))
If the cat chases the cow then the cow chases the rabbit.
((("cat" "chases" "cow" "+")) -> ("cow" "chases" "rabbit" "+"))
If someone is green then they are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone needs the cow then the cow needs the rabbit.
((("someone" "needs" "cow" "+")) -> ("cow" "needs" "rabbit" "+"))
If someone eats the cow then the cow chases the rabbit.
((("someone" "eats" "cow" "+")) -> ("cow" "chases" "rabbit" "+"))
The cow chases the rabbit.
True
1
proof
[(triple4 OR ((triple1) -> rule3))]
("cow" "chases" "rabbit" "+")
triple4
((triple1) -> (rule3 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is not green.
False
1
inv-proof
[(triple7 OR ((triple5 triple1) -> rule2))]
("cow" "is" "green" "-")
triple7
((triple5 triple1) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is big.
True
2
proof
[(((triple7) -> rule4) OR ((((triple5 triple1) -> rule2)) -> rule4))]
("cow" "is" "big" "+")
((triple7) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
((((triple5 triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is not big.
False
2
inv-proof
[(((triple7) -> rule4) OR ((((triple5 triple1) -> rule2)) -> rule4))]
("cow" "is" "big" "-")
((triple7) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
((((triple5 triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The rabbit is big.
True
4
proof
[(((((triple9 triple1) -> rule2)) -> rule4))]
("rabbit" "is" "big" "+")
((((triple9 triple1) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is not big.
False
4
inv-proof
[(((((triple9 triple1) -> rule2)) -> rule4))]
("rabbit" "is" "big" "-")
((((triple9 triple1) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The cow does not need the rabbit.
Unknown
inv-rconc
[@1: The cow needs the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "needs" "rabbit" "-")
The cat is big.
Unknown
rconc
[@2: The cat is big.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("cat" "is" "big" "+")
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "green" "-")
The rabbit needs the cat.
Unknown
random
[@0: The rabbit needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cat" "+")
The rabbit does not need the cow.
Unknown
inv-random
[@0: The rabbit needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cow" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cat chases the cow.[(triple1)] The cat is kind.[(triple2)] The cow chases the cat.[(triple3)] The cow chases the rabbit.[(triple4 OR ((triple1) -> rule3))] The cow eats the cat.[(triple5)] The cow eats the rabbit.[(triple6)] The cow is green.[(triple7 OR ((triple5 triple1) -> rule2))] The cow needs the cat.[(triple8)] The rabbit eats the cat.[(triple9)] The rabbit is kind.[(triple10)] @1: The cow is big.[(((triple7) -> rule4) OR ((((triple5 triple1) -> rule2)) -> rule4))] The rabbit is green.[(((triple9 triple1) -> rule2))] @2: The rabbit is big.[(((((triple9 triple1) -> rule2)) -> rule4))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cow chases the cat.
("cow" "chases" "cat" "+")
triple3
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple4
((triple1) -> (rule3 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
triple5
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple6
The cow is green.
("cow" "is" "green" "+")
triple7
((triple5 triple1) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
triple8
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The cow is big.
("cow" "is" "big" "+")
((triple7) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
((((triple5 triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
((triple9 triple1) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple9 triple1) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2