The bald eagle eats the dog. The dog is big. If someone eats the dog then the dog sees the bald eagle. If someone eats the dog then the dog sees the bald eagle. If someone is blue then they do not see the dog. If someone eats the bald eagle and they eat the dog then they do not see the dog. If someone eats the bald eagle then they see the dog. If someone needs the bald eagle then they are young. If someone sees the bald eagle then the bald eagle is blue. If someone eats the dog then the dog is big.
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
If someone eats the dog then the dog sees the bald eagle.
((("someone" "eats" "dog" "+")) -> ("dog" "sees" "bald eagle" "+"))
If someone eats the dog then the dog sees the bald eagle.
((("someone" "eats" "dog" "+")) -> ("dog" "sees" "bald eagle" "+"))
If someone is blue then they do not see the dog.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "dog" "-"))
If someone eats the bald eagle and they eat the dog then they do not see the dog.
((("someone" "eats" "bald eagle" "+") ("someone" "eats" "dog" "+")) -> ("someone" "sees" "dog" "-"))
If someone eats the bald eagle then they see the dog.
((("someone" "eats" "bald eagle" "+")) -> ("someone" "sees" "dog" "+"))
If someone needs the bald eagle then they are young.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "is" "young" "+"))
If someone sees the bald eagle then the bald eagle is blue.
((("someone" "sees" "bald eagle" "+")) -> ("bald eagle" "is" "blue" "+"))
If someone eats the dog then the dog is big.
((("someone" "eats" "dog" "+")) -> ("dog" "is" "big" "+"))
The bald eagle eats the dog.
True
1
proof
[(triple1)]
("bald eagle" "eats" "dog" "+")
triple1
The dog is not big.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule8))]
("dog" "is" "big" "-")
triple2
((triple1) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog sees the bald eagle.
True
2
proof
[(((triple1) -> rule1) OR ((triple1) -> rule2))]
("dog" "sees" "bald eagle" "+")
((triple1) -> (rule1 % int1))
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int1
((triple1) -> (rule2 % int1))
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int1
The dog does not see the bald eagle.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule2))]
("dog" "sees" "bald eagle" "-")
((triple1) -> (rule1 % int1))
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int1
((triple1) -> (rule2 % int1))
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int1
The bald eagle is blue.
True
3
proof
[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule2)) -> rule7))]
("bald eagle" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int2
The bald eagle is not blue.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule2)) -> rule7))]
("bald eagle" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int2
The bald eagle does not see the dog.
True
4
proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule3) OR ((((((triple1) -> rule2)) -> rule7)) -> rule3))]
("bald eagle" "sees" "dog" "-")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bald eagle does not see the dog.
("bald eagle" "sees" "dog" "-")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bald eagle does not see the dog.
("bald eagle" "sees" "dog" "-")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int3
The bald eagle sees the dog.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule3) OR ((((((triple1) -> rule2)) -> rule7)) -> rule3))]
("bald eagle" "sees" "dog" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bald eagle does not see the dog.
("bald eagle" "sees" "dog" "-")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bald eagle does not see the dog.
("bald eagle" "sees" "dog" "-")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int3
The bald eagle is not young.
Unknown
inv-rconc
[@1: The bald eagle is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "young" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "young" "+")
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The bald eagle is not big.
Unknown
inv-random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
The bald eagle does not need the dog.
Unknown
inv-random
[@0: The bald eagle needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "dog" "-")
The dog needs the bald eagle.
Unknown
random
[@0: The dog needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "bald eagle" "+")
@0: The bald eagle eats the dog.[(triple1)] The dog is big.[(triple2 OR ((triple1) -> rule8))] @1: The dog sees the bald eagle.[(((triple1) -> rule1) OR ((triple1) -> rule2))] @2: The bald eagle is blue.[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule2)) -> rule7))] @3: The bald eagle does not see the dog.[(((((((triple1) -> rule1)) -> rule7)) -> rule3) OR ((((((triple1) -> rule2)) -> rule7)) -> rule3))]
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
((triple1) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
((triple1) -> (rule1 % int1))
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int1
((triple1) -> (rule2 % int1))
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int2
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int1
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int2
The bald eagle does not see the dog.
("bald eagle" "sees" "dog" "-")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bald eagle does not see the dog.
("bald eagle" "sees" "dog" "-")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The bald eagle does not see the dog.
("bald eagle" "sees" "dog" "-")
int1
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
int3