The bald eagle is green. The bear needs the rabbit. The dog eats the bald eagle. The dog does not eat the rabbit. The dog is big. The dog needs the bald eagle. The dog needs the bear. The dog does not need the rabbit. The dog visits the bear. The rabbit is big. The rabbit is green. The rabbit is nice. If the bald eagle needs the rabbit then the rabbit does not need the dog. If someone visits the dog and the dog needs the bald eagle then the bald eagle is nice. If someone is nice then they do not need the bear. If someone is green then they visit the dog. If someone needs the bald eagle then the bald eagle is green. If the dog visits the rabbit then the rabbit visits the dog.
The bald eagle is green.
("bald eagle" "is" "green" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
The dog does not eat the rabbit.
("dog" "eats" "rabbit" "-")
The dog is big.
("dog" "is" "big" "+")
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog does not need the rabbit.
("dog" "needs" "rabbit" "-")
The dog visits the bear.
("dog" "visits" "bear" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
If the bald eagle needs the rabbit then the rabbit does not need the dog.
((("bald eagle" "needs" "rabbit" "+")) -> ("rabbit" "needs" "dog" "-"))
If someone visits the dog and the dog needs the bald eagle then the bald eagle is nice.
((("someone" "visits" "dog" "+") ("dog" "needs" "bald eagle" "+")) -> ("bald eagle" "is" "nice" "+"))
If someone is nice then they do not need the bear.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "bear" "-"))
If someone is green then they visit the dog.
((("someone" "is" "green" "+")) -> ("someone" "visits" "dog" "+"))
If someone needs the bald eagle then the bald eagle is green.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "is" "green" "+"))
If the dog visits the rabbit then the rabbit visits the dog.
((("dog" "visits" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
The rabbit is green.
True
1
proof
[(triple11)]
("rabbit" "is" "green" "+")
triple11
The bear does not need the rabbit.
False
1
inv-proof
[(triple2)]
("bear" "needs" "rabbit" "-")
triple2
The rabbit does not need the bear.
True
2
proof
[(((triple12) -> rule3))]
("rabbit" "needs" "bear" "-")
((triple12) -> (rule3 % int1))
The rabbit does not need the bear.
("rabbit" "needs" "bear" "-")
int1
The bald eagle does not visit the dog.
False
2
inv-proof
[(((triple1) -> rule4) OR ((((triple6) -> rule5)) -> rule4))]
("bald eagle" "visits" "dog" "-")
((triple1) -> (rule4 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The bald eagle is green.
("bald eagle" "is" "green" "+")
int2
The bald eagle is nice.
True
4
proof
[(((((triple1) -> rule4) triple6) -> rule2) OR ((((triple11) -> rule4) triple6) -> rule2) OR ((((((triple6) -> rule5)) -> rule4) triple6) -> rule2))]
("bald eagle" "is" "nice" "+")
((((triple1) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
((((triple11) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The bald eagle is green.
("bald eagle" "is" "green" "+")
int3
The bald eagle is not nice.
False
4
inv-proof
[(((((triple1) -> rule4) triple6) -> rule2) OR ((((triple11) -> rule4) triple6) -> rule2) OR ((((((triple6) -> rule5)) -> rule4) triple6) -> rule2))]
("bald eagle" "is" "nice" "-")
((((triple1) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
((((triple11) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The bald eagle is green.
("bald eagle" "is" "green" "+")
int3
The bald eagle does not need the bear.
True
5
proof
[(((((((triple1) -> rule4) triple6) -> rule2)) -> rule3) OR ((((((triple11) -> rule4) triple6) -> rule2)) -> rule3) OR ((((((((triple6) -> rule5)) -> rule4) triple6) -> rule2)) -> rule3))]
("bald eagle" "needs" "bear" "-")
((((((triple1) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int3
((((((triple11) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int3
((((((((triple6) -> (rule5 % int4))) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int3
The bald eagle is green.
("bald eagle" "is" "green" "+")
int4
The bald eagle needs the bear.
False
5
inv-proof
[(((((((triple1) -> rule4) triple6) -> rule2)) -> rule3) OR ((((((triple11) -> rule4) triple6) -> rule2)) -> rule3) OR ((((((((triple6) -> rule5)) -> rule4) triple6) -> rule2)) -> rule3))]
("bald eagle" "needs" "bear" "+")
((((((triple1) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int3
((((((triple11) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int3
((((((((triple6) -> (rule5 % int4))) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int3
The bald eagle is green.
("bald eagle" "is" "green" "+")
int4
The bear does not visit the dog.
Unknown
inv-rconc
[@1: The bear visits the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "dog" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "visits" "dog" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog visits the rabbit.
Unknown
random
[@0: The dog visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "rabbit" "+")
@0: The bald eagle is green.[(triple1 OR ((triple6) -> rule5))] The bear needs the rabbit.[(triple2)] The dog does not eat the rabbit.[(triple4)] The dog does not need the rabbit.[(triple8)] The dog eats the bald eagle.[(triple3)] The dog is big.[(triple5)] The dog needs the bald eagle.[(triple6)] The dog needs the bear.[(triple7)] The dog visits the bear.[(triple9)] The rabbit is big.[(triple10)] The rabbit is green.[(triple11)] The rabbit is nice.[(triple12)] @1: The bald eagle visits the dog.[(((triple1) -> rule4) OR ((((triple6) -> rule5)) -> rule4))] The rabbit does not need the bear.[(((triple12) -> rule3))] The rabbit visits the dog.[(((triple11) -> rule4))] @2: The bald eagle is nice.[(((((triple1) -> rule4) triple6) -> rule2) OR ((((triple11) -> rule4) triple6) -> rule2) OR ((((((triple6) -> rule5)) -> rule4) triple6) -> rule2))] @3: The bald eagle does not need the bear.[(((((((triple1) -> rule4) triple6) -> rule2)) -> rule3) OR ((((((triple11) -> rule4) triple6) -> rule2)) -> rule3) OR ((((((((triple6) -> rule5)) -> rule4) triple6) -> rule2)) -> rule3))]
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple1
((triple6) -> (rule5 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple2
The dog does not eat the rabbit.
("dog" "eats" "rabbit" "-")
triple4
The dog does not need the rabbit.
("dog" "needs" "rabbit" "-")
triple8
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
triple3
The dog is big.
("dog" "is" "big" "+")
triple5
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
triple6
The dog needs the bear.
("dog" "needs" "bear" "+")
triple7
The dog visits the bear.
("dog" "visits" "bear" "+")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
triple11
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple12
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
((triple1) -> (rule4 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int1
The bald eagle is green.
("bald eagle" "is" "green" "+")
int2
The rabbit does not need the bear.
("rabbit" "needs" "bear" "-")
((triple12) -> (rule3 % int1))
The rabbit does not need the bear.
("rabbit" "needs" "bear" "-")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((triple11) -> (rule4 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
((((triple1) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
((((triple11) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int2
The bald eagle is green.
("bald eagle" "is" "green" "+")
int3
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
((((((triple1) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int3
((((((triple11) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int3
((((((((triple6) -> (rule5 % int4))) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The bald eagle does not need the bear.
("bald eagle" "needs" "bear" "-")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
int3
The bald eagle is green.
("bald eagle" "is" "green" "+")
int4