The bald eagle chases the squirrel. The bald eagle is blue. The bald eagle is kind. The bald eagle needs the cow. The bald eagle needs the squirrel. The bald eagle needs the tiger. The cow needs the squirrel. The squirrel chases the tiger. The squirrel does not like the cow. The tiger does not chase the cow. The tiger needs the cow. The tiger does not need the squirrel. If someone needs the squirrel then they chase the squirrel. If someone chases the squirrel then they need the tiger. If someone chases the bald eagle then they need the tiger. If someone needs the tiger then they chase the cow. If someone chases the cow and they like the squirrel then the squirrel does not like the tiger. If someone chases the bald eagle and the bald eagle likes the squirrel then they like the cow.
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
If someone needs the squirrel then they chase the squirrel.
((("someone" "needs" "squirrel" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone chases the squirrel then they need the tiger.
((("someone" "chases" "squirrel" "+")) -> ("someone" "needs" "tiger" "+"))
If someone chases the bald eagle then they need the tiger.
((("someone" "chases" "bald eagle" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the tiger then they chase the cow.
((("someone" "needs" "tiger" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the cow and they like the squirrel then the squirrel does not like the tiger.
((("someone" "chases" "cow" "+") ("someone" "likes" "squirrel" "+")) -> ("squirrel" "likes" "tiger" "-"))
If someone chases the bald eagle and the bald eagle likes the squirrel then they like the cow.
((("someone" "chases" "bald eagle" "+") ("bald eagle" "likes" "squirrel" "+")) -> ("someone" "likes" "cow" "+"))
The bald eagle needs the cow.
True
1
proof
[(triple4)]
("bald eagle" "needs" "cow" "+")
triple4
The bald eagle does not need the tiger.
False
1
inv-proof
[(triple6 OR ((triple1) -> rule2) OR ((((triple5) -> rule1)) -> rule2))]
("bald eagle" "needs" "tiger" "-")
triple6
((triple1) -> (rule2 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
int2
The bald eagle chases the cow.
True
2
proof
[(((triple6) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((((triple5) -> rule1)) -> rule2)) -> rule4))]
("bald eagle" "chases" "cow" "+")
((triple6) -> (rule4 % int1))
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
int3
The bald eagle does not chase the cow.
False
2
inv-proof
[(((triple6) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((((triple5) -> rule1)) -> rule2)) -> rule4))]
("bald eagle" "chases" "cow" "-")
((triple6) -> (rule4 % int1))
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
int3
The cow needs the tiger.
True
3
proof
[(((((triple7) -> rule1)) -> rule2))]
("cow" "needs" "tiger" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow does not need the tiger.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("cow" "needs" "tiger" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow chases the cow.
True
4
proof
[(((((((triple7) -> rule1)) -> rule2)) -> rule4))]
("cow" "chases" "cow" "+")
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int3
The cow does not chase the cow.
False
4
inv-proof
[(((((((triple7) -> rule1)) -> rule2)) -> rule4))]
("cow" "chases" "cow" "-")
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int3
The bald eagle does not like the cow.
Unknown
inv-rconc
[@1: The bald eagle likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "likes" "cow" "-")
The squirrel chases the cow.
Unknown
rconc
[@3: The squirrel chases the cow.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- FAIL)]]
("squirrel" "chases" "cow" "+")
The tiger does not like the cow.
Unknown
inv-rconc
[@1: The tiger likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "cow" "-")
The tiger chases the squirrel.
Unknown
rconc
[@1: The tiger chases the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "squirrel" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The cow does not chase the tiger.
Unknown
inv-random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "-")
The cow chases the bald eagle.
Unknown
random
[@0: The cow chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "bald eagle" "+")
@0: The bald eagle chases the squirrel.[(triple1 OR ((triple5) -> rule1))] The bald eagle is blue.[(triple2)] The bald eagle is kind.[(triple3)] The bald eagle needs the cow.[(triple4)] The bald eagle needs the squirrel.[(triple5)] The bald eagle needs the tiger.[(triple6 OR ((triple1) -> rule2) OR ((((triple5) -> rule1)) -> rule2))] The cow needs the squirrel.[(triple7)] The squirrel chases the tiger.[(triple8)] The squirrel does not like the cow.[(triple9)] The tiger does not chase the cow.[(triple10)] The tiger does not need the squirrel.[(triple12)] The tiger needs the cow.[(triple11)] @1: The bald eagle chases the cow.[(((triple6) -> rule4) OR ((((triple1) -> rule2)) -> rule4) OR ((((((triple5) -> rule1)) -> rule2)) -> rule4))] The cow chases the squirrel.[(((triple7) -> rule1))] @2: The cow needs the tiger.[(((((triple7) -> rule1)) -> rule2))] @3: The cow chases the cow.[(((((((triple7) -> rule1)) -> rule2)) -> rule4))]
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
triple1
((triple5) -> (rule1 % int1))
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple3
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
triple4
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
triple5
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
triple6
((triple1) -> (rule2 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple7
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple8
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
triple9
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
triple10
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple12
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple11
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
((triple6) -> (rule4 % int1))
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
int3
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
((triple7) -> (rule1 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int3