The bald eagle likes the cow. The bald eagle needs the tiger. The cow chases the tiger. The cow needs the tiger. The tiger is green. The tiger likes the bald eagle. The tiger needs the cow. If the cow likes the tiger and the tiger likes the bald eagle then the cow chases the bald eagle. If something needs the tiger and the tiger needs the bald eagle then it likes the bald eagle. If the tiger needs the bald eagle then the bald eagle likes the tiger. If the tiger is nice then the tiger is young. If something likes the bald eagle then it needs the bald eagle. If something is blue then it chases the cow. If something needs the cow and it likes the cow then it is blue. If the cow likes the tiger and the cow is young then the tiger chases the bald eagle.
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If the cow likes the tiger and the tiger likes the bald eagle then the cow chases the bald eagle.
((("cow" "likes" "tiger" "+") ("tiger" "likes" "bald eagle" "+")) -> ("cow" "chases" "bald eagle" "+"))
If something needs the tiger and the tiger needs the bald eagle then it likes the bald eagle.
((("something" "needs" "tiger" "+") ("tiger" "needs" "bald eagle" "+")) -> ("something" "likes" "bald eagle" "+"))
If the tiger needs the bald eagle then the bald eagle likes the tiger.
((("tiger" "needs" "bald eagle" "+")) -> ("bald eagle" "likes" "tiger" "+"))
If the tiger is nice then the tiger is young.
((("tiger" "is" "nice" "+")) -> ("tiger" "is" "young" "+"))
If something likes the bald eagle then it needs the bald eagle.
((("something" "likes" "bald eagle" "+")) -> ("something" "needs" "bald eagle" "+"))
If something is blue then it chases the cow.
((("something" "is" "blue" "+")) -> ("something" "chases" "cow" "+"))
If something needs the cow and it likes the cow then it is blue.
((("something" "needs" "cow" "+") ("something" "likes" "cow" "+")) -> ("something" "is" "blue" "+"))
If the cow likes the tiger and the cow is young then the tiger chases the bald eagle.
((("cow" "likes" "tiger" "+") ("cow" "is" "young" "+")) -> ("tiger" "chases" "bald eagle" "+"))
The cow needs the tiger.
True
1
proof
[(triple4)]
("cow" "needs" "tiger" "+")
triple4
The bald eagle does not need the tiger.
False
1
inv-proof
[(triple2)]
("bald eagle" "needs" "tiger" "-")
triple2
The tiger needs the bald eagle.
True
2
proof
[(((triple6) -> rule5))]
("tiger" "needs" "bald eagle" "+")
((triple6) -> (rule5 % int1))
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int1
The tiger does not need the bald eagle.
False
2
inv-proof
[(((triple6) -> rule5))]
("tiger" "needs" "bald eagle" "-")
((triple6) -> (rule5 % int1))
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int1
The bald eagle likes the tiger.
True
3
proof
[(((((triple6) -> rule5)) -> rule3))]
("bald eagle" "likes" "tiger" "+")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The cow does not like the bald eagle.
False
4
inv-proof
[(((triple4 ((triple6) -> rule5)) -> rule2))]
("cow" "likes" "bald eagle" "-")
((triple4 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The bald eagle needs the bald eagle.
True
5
proof
[(((((triple2 ((triple6) -> rule5)) -> rule2)) -> rule5))]
("bald eagle" "needs" "bald eagle" "+")
((((triple2 ((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle likes the bald eagle.
("bald eagle" "likes" "bald eagle" "+")
int2
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int3
The bald eagle does not need the bald eagle.
False
5
inv-proof
[(((((triple2 ((triple6) -> rule5)) -> rule2)) -> rule5))]
("bald eagle" "needs" "bald eagle" "-")
((((triple2 ((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle likes the bald eagle.
("bald eagle" "likes" "bald eagle" "+")
int2
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int3
The tiger does not chase the bald eagle.
Unknown
inv-rconc
[@1: The tiger chases the bald eagle.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "chases" "bald eagle" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "blue" "+")
The cow does not chase the cow.
Unknown
inv-rconc
[@2: The cow chases the cow.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("cow" "chases" "cow" "-")
The bald eagle is blue.
Unknown
rconc
[@1: The bald eagle is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "is" "blue" "+")
The cow does not like the tiger.
Unknown
inv-random
[@0: The cow likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "tiger" "-")
The bald eagle needs the cow.
Unknown
random
[@0: The bald eagle needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "cow" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The bald eagle likes the cow.[(triple1)] The bald eagle needs the tiger.[(triple2)] The cow chases the tiger.[(triple3)] The cow needs the tiger.[(triple4)] The tiger is green.[(triple5)] The tiger likes the bald eagle.[(triple6)] The tiger needs the cow.[(triple7)] @1: The tiger needs the bald eagle.[(((triple6) -> rule5))] @2: The bald eagle likes the bald eagle.[(((triple2 ((triple6) -> rule5)) -> rule2))] The bald eagle likes the tiger.[(((((triple6) -> rule5)) -> rule3))] The cow likes the bald eagle.[(((triple4 ((triple6) -> rule5)) -> rule2))] @3: The bald eagle needs the bald eagle.[(((((triple2 ((triple6) -> rule5)) -> rule2)) -> rule5))] The cow needs the bald eagle.[(((((triple4 ((triple6) -> rule5)) -> rule2)) -> rule5))]
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
triple1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
triple2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple3
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple4
The tiger is green.
("tiger" "is" "green" "+")
triple5
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
triple6
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple7
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
((triple6) -> (rule5 % int1))
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int1
The bald eagle likes the bald eagle.
("bald eagle" "likes" "bald eagle" "+")
((triple2 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The bald eagle likes the bald eagle.
("bald eagle" "likes" "bald eagle" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
((triple4 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int1
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int2
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
((((triple2 ((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle likes the bald eagle.
("bald eagle" "likes" "bald eagle" "+")
int2
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int3
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
((((triple4 ((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
int1
The cow likes the bald eagle.
("cow" "likes" "bald eagle" "+")
int2
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
int3