The bald eagle chases the cat. The cat chases the dog. The dog chases the bald eagle. If something sees the cat and it chases the bald eagle then it eats the bald eagle. If something eats the bald eagle then it sees the cat. If something chases the dog then the dog eats the bald eagle. If something chases the dog and it sees the dog then it eats the cat. If something sees the cat then the cat sees the bald eagle. If something eats the bald eagle and it chases the dog then the dog eats the cat.
The bald eagle chases the cat.
("bald eagle" "chases" "cat" "+")
The cat chases the dog.
("cat" "chases" "dog" "+")
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
If something sees the cat and it chases the bald eagle then it eats the bald eagle.
((("something" "sees" "cat" "+") ("something" "chases" "bald eagle" "+")) -> ("something" "eats" "bald eagle" "+"))
If something eats the bald eagle then it sees the cat.
((("something" "eats" "bald eagle" "+")) -> ("something" "sees" "cat" "+"))
If something chases the dog then the dog eats the bald eagle.
((("something" "chases" "dog" "+")) -> ("dog" "eats" "bald eagle" "+"))
If something chases the dog and it sees the dog then it eats the cat.
((("something" "chases" "dog" "+") ("something" "sees" "dog" "+")) -> ("something" "eats" "cat" "+"))
If something sees the cat then the cat sees the bald eagle.
((("something" "sees" "cat" "+")) -> ("cat" "sees" "bald eagle" "+"))
If something eats the bald eagle and it chases the dog then the dog eats the cat.
((("something" "eats" "bald eagle" "+") ("something" "chases" "dog" "+")) -> ("dog" "eats" "cat" "+"))
The bald eagle chases the cat.
True
1
proof
[(triple1)]
("bald eagle" "chases" "cat" "+")
triple1
The cat does not chase the dog.
False
1
inv-proof
[(triple2)]
("cat" "chases" "dog" "-")
triple2
The dog eats the bald eagle.
True
2
proof
[(((triple2) -> rule3))]
("dog" "eats" "bald eagle" "+")
((triple2) -> (rule3 % int1))
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int1
The dog does not eat the bald eagle.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "eats" "bald eagle" "-")
((triple2) -> (rule3 % int1))
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int1
The dog sees the cat.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("dog" "sees" "cat" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int2
The dog does not see the cat.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("dog" "sees" "cat" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int2
The cat sees the bald eagle.
True
4
proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule5))]
("cat" "sees" "bald eagle" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int3
The cat does not see the bald eagle.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule5))]
("cat" "sees" "bald eagle" "-")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int3
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "cat" "-")
The dog eats the cat.
Unknown
rconc
[@2: The dog eats the cat.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("dog" "eats" "cat" "+")
The cat does not eat the bald eagle.
Unknown
inv-rconc
[@1: The cat eats the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "bald eagle" "-")
The bald eagle eats the bald eagle.
Unknown
rconc
[@1: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The bald eagle chases the cat.[(triple1)] The cat chases the dog.[(triple2)] The dog chases the bald eagle.[(triple3)] @1: The dog eats the bald eagle.[(((triple2) -> rule3))] @2: The dog sees the cat.[(((((triple2) -> rule3)) -> rule2))] @3: The cat sees the bald eagle.[(((((((triple2) -> rule3)) -> rule2)) -> rule5))]
The bald eagle chases the cat.
("bald eagle" "chases" "cat" "+")
triple1
The cat chases the dog.
("cat" "chases" "dog" "+")
triple2
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
triple3
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
((triple2) -> (rule3 % int1))
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
int3