The bald eagle eats the cow. The cow needs the dog. The dog needs the bald eagle. Young things are blue. If something needs the dog then the dog needs the cow. If the cow is young then the cow needs the dog. If something needs the cow then it eats the cow. If something eats the cow then it likes the dog. If something eats the dog and it is young then it eats the cow.
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
Young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something needs the dog then the dog needs the cow.
((("something" "needs" "dog" "+")) -> ("dog" "needs" "cow" "+"))
If the cow is young then the cow needs the dog.
((("cow" "is" "young" "+")) -> ("cow" "needs" "dog" "+"))
If something needs the cow then it eats the cow.
((("something" "needs" "cow" "+")) -> ("something" "eats" "cow" "+"))
If something eats the cow then it likes the dog.
((("something" "eats" "cow" "+")) -> ("something" "likes" "dog" "+"))
If something eats the dog and it is young then it eats the cow.
((("something" "eats" "dog" "+") ("something" "is" "young" "+")) -> ("something" "eats" "cow" "+"))
The cow needs the dog.
True
1
proof
[(triple2)]
("cow" "needs" "dog" "+")
triple2
The cow does not need the dog.
False
1
inv-proof
[(triple2)]
("cow" "needs" "dog" "-")
triple2
The bald eagle likes the dog.
True
2
proof
[(((triple1) -> rule5))]
("bald eagle" "likes" "dog" "+")
((triple1) -> (rule5 % int1))
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
int1
The bald eagle does not like the dog.
False
2
inv-proof
[(((triple1) -> rule5))]
("bald eagle" "likes" "dog" "-")
((triple1) -> (rule5 % int1))
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
int1
The dog eats the cow.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("dog" "eats" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog does not eat the cow.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("dog" "eats" "cow" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog likes the dog.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule5))]
("dog" "likes" "dog" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
int3
The dog does not like the dog.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule5))]
("dog" "likes" "dog" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
int3
The cow is not blue.
Unknown
inv-rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "blue" "-")
The cow eats the cow.
Unknown
rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "cow" "+")
The cow does not like the dog.
Unknown
inv-rconc
[@2: The cow likes the dog.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("cow" "likes" "dog" "-")
The bald eagle is blue.
Unknown
rconc
[@1: The bald eagle is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "blue" "+")
The cow does not like the bald eagle.
Unknown
inv-random
[@0: The cow likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "bald eagle" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The bald eagle needs the bald eagle.
Unknown
random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "+")
@0: The bald eagle eats the cow.[(triple1)] The cow needs the dog.[(triple2)] The dog needs the bald eagle.[(triple3)] @1: The bald eagle likes the dog.[(((triple1) -> rule5))] The dog needs the cow.[(((triple2) -> rule2))] @2: The dog eats the cow.[(((((triple2) -> rule2)) -> rule4))] @3: The dog likes the dog.[(((((((triple2) -> rule2)) -> rule4)) -> rule5))]
The bald eagle eats the cow.
("bald eagle" "eats" "cow" "+")
triple1
The cow needs the dog.
("cow" "needs" "dog" "+")
triple2
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
triple3
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
((triple1) -> (rule5 % int1))
The bald eagle likes the dog.
("bald eagle" "likes" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
((triple2) -> (rule2 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
int3