The cat chases the cow. The cow likes the cat. If the cat is round and the cat is not blue then the cat is not green. If someone is green and round then they like the cat. If someone likes the cow then they do not eat the cow. If the cow chases the cat then the cat likes the cow. If someone eats the cow and the cow is not green then they do not chase the cat. If someone eats the cat and they eat the cow then the cow chases the cat. If the cow eats the cat and the cow does not like the cat then the cow chases the cat. If someone chases the cow then the cow chases the cat.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
If the cat is round and the cat is not blue then the cat is not green.
((("cat" "is" "round" "+") ("cat" "is" "blue" "~")) -> ("cat" "is" "green" "-"))
If someone is green and round then they like the cat.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "likes" "cat" "+"))
If someone likes the cow then they do not eat the cow.
((("someone" "likes" "cow" "+")) -> ("someone" "eats" "cow" "-"))
If the cow chases the cat then the cat likes the cow.
((("cow" "chases" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If someone eats the cow and the cow is not green then they do not chase the cat.
((("someone" "eats" "cow" "+") ("cow" "is" "green" "~")) -> ("someone" "chases" "cat" "-"))
If someone eats the cat and they eat the cow then the cow chases the cat.
((("someone" "eats" "cat" "+") ("someone" "eats" "cow" "+")) -> ("cow" "chases" "cat" "+"))
If the cow eats the cat and the cow does not like the cat then the cow chases the cat.
((("cow" "eats" "cat" "+") ("cow" "likes" "cat" "~")) -> ("cow" "chases" "cat" "+"))
If someone chases the cow then the cow chases the cat.
((("someone" "chases" "cow" "+")) -> ("cow" "chases" "cat" "+"))
The cow likes the cat.
True
1
proof
[(triple2)]
("cow" "likes" "cat" "+")
triple2
The cat does not chase the cow.
False
1
inv-proof
[(triple1)]
("cat" "chases" "cow" "-")
triple1
The cow chases the cat.
True
2
proof
[(((triple1) -> rule8))]
("cow" "chases" "cat" "+")
((triple1) -> (rule8 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow does not chase the cat.
False
2
inv-proof
[(((triple1) -> rule8))]
("cow" "chases" "cat" "-")
((triple1) -> (rule8 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cat likes the cow.
True
3
proof
[(((((triple1) -> rule8)) -> rule4))]
("cat" "likes" "cow" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cat does not like the cow.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("cat" "likes" "cow" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cat does not eat the cow.
True
4
proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule3))]
("cat" "eats" "cow" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat does not eat the cow.
("cat" "eats" "cow" "-")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3
The cat eats the cow.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule3))]
("cat" "eats" "cow" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat does not eat the cow.
("cat" "eats" "cow" "-")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "cat" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat chases the cow.[(triple1)] The cow likes the cat.[(triple2)] @1: The cow chases the cat.[(((triple1) -> rule8))] @2: The cat likes the cow.[(((((triple1) -> rule8)) -> rule4))] @3: The cat does not eat the cow.[(((((((triple1) -> rule8)) -> rule4)) -> rule3))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cow likes the cat.
("cow" "likes" "cat" "+")
triple2
The cow chases the cat.
("cow" "chases" "cat" "+")
((triple1) -> (rule8 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cat does not eat the cow.
("cat" "eats" "cow" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat does not eat the cow.
("cat" "eats" "cow" "-")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3