The bald eagle eats the cow. The cow needs the bald eagle. The dog needs the bald eagle. If the cow eats the dog then the dog sees the cow. If the cow needs the bald eagle then the cow sees the dog. If something sees the dog then it needs the cow.
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
If the cow eats the dog then the dog sees the cow.
((("cow" "eats" "dog" "+")) -> ("dog" "sees" "cow" "+"))
If the cow needs the bald eagle then the cow sees the dog.
((("cow" "needs" "bald eagle" "+")) -> ("cow" "sees" "dog" "+"))
If something sees the dog then it needs the cow.
((("something" "sees" "dog" "+")) -> ("something" "needs" "cow" "+"))
The bald eagle eats the cow.
True
1
proof
[(triple1)]
("bald eagle" "eats" "cow" "+")
triple1
The cow does not need the bald eagle.
False
1
inv-proof
[(triple2)]
("cow" "needs" "bald eagle" "-")
triple2
The cow sees the dog.
True
2
proof
[(((triple2) -> rule2))]
("cow" "sees" "dog" "+")
((triple2) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow does not see the dog.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "sees" "dog" "-")
((triple2) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow needs the cow.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("cow" "needs" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow does not need the cow.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("cow" "needs" "cow" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The dog does not need the cow.
Unknown
inv-rconc
[@1: The dog needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "cow" "-")
The bald eagle needs the cow.
Unknown
rconc
[@1: The bald eagle needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "needs" "cow" "+")
The dog does not see the cow.
Unknown
inv-rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "cow" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The bald eagle does not see the dog.
Unknown
inv-random
[@0: The bald eagle sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "dog" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The bald eagle eats the cow.[(triple1)] The cow needs the bald eagle.[(triple2)] The dog needs the bald eagle.[(triple3)] @1: The cow sees the dog.[(((triple2) -> rule2))] @2: The cow needs the cow.[(((((triple2) -> rule2)) -> rule3))]
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
triple1
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
triple2
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
triple3
The cow sees the dog.
("cow" "sees" "dog" "+")
((triple2) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2