The bald eagle eats the dog. The bald eagle is round. The bald eagle sees the dog. The bear eats the squirrel. The dog eats the bald eagle. The dog eats the squirrel. The dog needs the bald eagle. The dog sees the bear. The squirrel eats the dog. The squirrel is cold. The squirrel is rough. The squirrel needs the bald eagle. If someone needs the bear then they are green. If someone needs the dog then the dog needs the squirrel. If someone needs the bear then the bear needs the squirrel. If someone needs the bald eagle then the bald eagle needs the bear. If someone needs the bear then they see the squirrel. If the bald eagle is round and the bald eagle sees the bear then the bald eagle needs the squirrel.
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
The bald eagle is round.
("bald eagle" "is" "round" "+")
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the bald eagle.
("squirrel" "needs" "bald eagle" "+")
If someone needs the bear then they are green.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "green" "+"))
If someone needs the dog then the dog needs the squirrel.
((("someone" "needs" "dog" "+")) -> ("dog" "needs" "squirrel" "+"))
If someone needs the bear then the bear needs the squirrel.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "squirrel" "+"))
If someone needs the bald eagle then the bald eagle needs the bear.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "needs" "bear" "+"))
If someone needs the bear then they see the squirrel.
((("someone" "needs" "bear" "+")) -> ("someone" "sees" "squirrel" "+"))
If the bald eagle is round and the bald eagle sees the bear then the bald eagle needs the squirrel.
((("bald eagle" "is" "round" "+") ("bald eagle" "sees" "bear" "+")) -> ("bald eagle" "needs" "squirrel" "+"))
The bear eats the squirrel.
True
1
proof
[(triple4)]
("bear" "eats" "squirrel" "+")
triple4
The bald eagle does not eat the dog.
False
1
inv-proof
[(triple1)]
("bald eagle" "eats" "dog" "-")
triple1
The bald eagle needs the bear.
True
2
proof
[(((triple12) -> rule4) OR ((triple7) -> rule4))]
("bald eagle" "needs" "bear" "+")
((triple12) -> (rule4 % int1))
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int1
((triple7) -> (rule4 % int1))
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int1
The bald eagle does not need the bear.
False
2
inv-proof
[(((triple12) -> rule4) OR ((triple7) -> rule4))]
("bald eagle" "needs" "bear" "-")
((triple12) -> (rule4 % int1))
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int1
((triple7) -> (rule4 % int1))
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int1
The bald eagle is green.
True
3
proof
[(((((triple12) -> rule4)) -> rule1) OR ((((triple7) -> rule4)) -> rule1))]
("bald eagle" "is" "green" "+")
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2
The bald eagle does not see the squirrel.
False
3
inv-proof
[(((((triple12) -> rule4)) -> rule5) OR ((((triple7) -> rule4)) -> rule5))]
("bald eagle" "sees" "squirrel" "-")
((((triple12) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The dog sees the squirrel.
Unknown
rconc
[@1: The dog sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "squirrel" "+")
The dog does not need the squirrel.
Unknown
inv-rconc
[@1: The dog needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "squirrel" "-")
The bald eagle eats the bald eagle.
Unknown
random
[@0: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
The bear does not need the dog.
Unknown
inv-random
[@0: The bear needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "dog" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bald eagle eats the dog.[(triple1)] The bald eagle is round.[(triple2)] The bald eagle sees the dog.[(triple3)] The bear eats the squirrel.[(triple4)] The dog eats the bald eagle.[(triple5)] The dog eats the squirrel.[(triple6)] The dog needs the bald eagle.[(triple7)] The dog sees the bear.[(triple8)] The squirrel eats the dog.[(triple9)] The squirrel is cold.[(triple10)] The squirrel is rough.[(triple11)] The squirrel needs the bald eagle.[(triple12)] @1: The bald eagle needs the bear.[(((triple12) -> rule4) OR ((triple7) -> rule4))] @2: The bald eagle is green.[(((((triple12) -> rule4)) -> rule1) OR ((((triple7) -> rule4)) -> rule1))] The bald eagle sees the squirrel.[(((((triple12) -> rule4)) -> rule5) OR ((((triple7) -> rule4)) -> rule5))] The bear needs the squirrel.[(((((triple12) -> rule4)) -> rule3) OR ((((triple7) -> rule4)) -> rule3))]
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
triple1
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple2
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
triple3
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple4
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
triple5
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple6
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
triple7
The dog sees the bear.
("dog" "sees" "bear" "+")
triple8
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple9
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel needs the bald eagle.
("squirrel" "needs" "bald eagle" "+")
triple12
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
((triple12) -> (rule4 % int1))
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int1
((triple7) -> (rule4 % int1))
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int1
The bald eagle is green.
("bald eagle" "is" "green" "+")
((((triple12) -> (rule4 % int2))) -> (rule1 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
((((triple12) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((((triple12) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bald eagle needs the bear.
("bald eagle" "needs" "bear" "+")
int2