The cat eats the cow. The cow is nice. The dog eats the cow. If the dog likes the cat then the dog chases the cat. If something chases the cat and the cat is rough then the cat eats the cow. If something likes the cow then it is young. If something eats the cow then the cow chases the cat. If something chases the dog then it eats the dog. If something chases the cat then the cat is nice.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cow is nice.
("cow" "is" "nice" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
If the dog likes the cat then the dog chases the cat.
((("dog" "likes" "cat" "+")) -> ("dog" "chases" "cat" "+"))
If something chases the cat and the cat is rough then the cat eats the cow.
((("something" "chases" "cat" "+") ("cat" "is" "rough" "+")) -> ("cat" "eats" "cow" "+"))
If something likes the cow then it is young.
((("something" "likes" "cow" "+")) -> ("something" "is" "young" "+"))
If something eats the cow then the cow chases the cat.
((("something" "eats" "cow" "+")) -> ("cow" "chases" "cat" "+"))
If something chases the dog then it eats the dog.
((("something" "chases" "dog" "+")) -> ("something" "eats" "dog" "+"))
If something chases the cat then the cat is nice.
((("something" "chases" "cat" "+")) -> ("cat" "is" "nice" "+"))
The cow is nice.
True
1
proof
[(triple2)]
("cow" "is" "nice" "+")
triple2
The dog does not eat the cow.
False
1
inv-proof
[(triple3)]
("dog" "eats" "cow" "-")
triple3
The cow chases the cat.
True
2
proof
[(((triple1) -> rule4) OR ((triple3) -> rule4))]
("cow" "chases" "cat" "+")
((triple1) -> (rule4 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
((triple3) -> (rule4 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow does not chase the cat.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple3) -> rule4))]
("cow" "chases" "cat" "-")
((triple1) -> (rule4 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
((triple3) -> (rule4 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cat is nice.
True
3
proof
[(((((triple1) -> rule4)) -> rule6) OR ((((triple3) -> rule4)) -> rule6))]
("cat" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cat is not nice.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6) OR ((((triple3) -> rule4)) -> rule6))]
("cat" "is" "nice" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "young" "-")
The cat eats the dog.
Unknown
rconc
[@1: The cat eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "dog" "+")
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "dog" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The cat eats the cow.[(triple1)] The cow is nice.[(triple2)] The dog eats the cow.[(triple3)] @1: The cow chases the cat.[(((triple1) -> rule4) OR ((triple3) -> rule4))] @2: The cat is nice.[(((((triple1) -> rule4)) -> rule6) OR ((((triple3) -> rule4)) -> rule6))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The dog eats the cow.
("dog" "eats" "cow" "+")
triple3
The cow chases the cat.
("cow" "chases" "cat" "+")
((triple1) -> (rule4 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
((triple3) -> (rule4 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2