The bald eagle is young. The bear eats the tiger. The bear is rough. The bear is young. The bear needs the bald eagle. The dog eats the bald eagle. The dog eats the tiger. The dog visits the tiger. The tiger is young. The tiger needs the bear. If someone visits the dog then they visit the bald eagle. If someone eats the bald eagle and they eat the tiger then they eat the bear. If someone visits the bald eagle then they eat the bear. If someone needs the bear then the bear eats the tiger. If someone visits the dog then the dog needs the tiger. If the bear eats the tiger then the tiger is round. If someone is round then they visit the dog. If someone is blue and they need the dog then they visit the dog. If someone eats the bear then they eat the dog.
The bald eagle is young.
("bald eagle" "is" "young" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the bald eagle.
("bear" "needs" "bald eagle" "+")
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If someone visits the dog then they visit the bald eagle.
((("someone" "visits" "dog" "+")) -> ("someone" "visits" "bald eagle" "+"))
If someone eats the bald eagle and they eat the tiger then they eat the bear.
((("someone" "eats" "bald eagle" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "eats" "bear" "+"))
If someone visits the bald eagle then they eat the bear.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "eats" "bear" "+"))
If someone needs the bear then the bear eats the tiger.
((("someone" "needs" "bear" "+")) -> ("bear" "eats" "tiger" "+"))
If someone visits the dog then the dog needs the tiger.
((("someone" "visits" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If the bear eats the tiger then the tiger is round.
((("bear" "eats" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If someone is round then they visit the dog.
((("someone" "is" "round" "+")) -> ("someone" "visits" "dog" "+"))
If someone is blue and they need the dog then they visit the dog.
((("someone" "is" "blue" "+") ("someone" "needs" "dog" "+")) -> ("someone" "visits" "dog" "+"))
If someone eats the bear then they eat the dog.
((("someone" "eats" "bear" "+")) -> ("someone" "eats" "dog" "+"))
The bear needs the bald eagle.
True
1
proof
[(triple5)]
("bear" "needs" "bald eagle" "+")
triple5
The dog does not eat the tiger.
False
1
inv-proof
[(triple7)]
("dog" "eats" "tiger" "-")
triple7
The tiger is round.
True
2
proof
[(((triple2) -> rule6) OR ((((triple10) -> rule4)) -> rule6))]
("tiger" "is" "round" "+")
((triple2) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The dog does not eat the bear.
False
3
inv-proof
[(((triple6 triple7) -> rule2))]
("dog" "eats" "bear" "-")
((triple6 triple7) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog eats the dog.
True
4
proof
[(((((triple6 triple7) -> rule2)) -> rule9))]
("dog" "eats" "dog" "+")
((((triple6 triple7) -> (rule2 % int2))) -> (rule9 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The tiger does not visit the dog.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule7) OR ((((((triple10) -> rule4)) -> rule6)) -> rule7))]
("tiger" "visits" "dog" "-")
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
((((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3
The tiger visits the bald eagle.
True
4
proof
[(((((((triple2) -> rule6)) -> rule7)) -> rule1) OR ((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule1))]
("tiger" "visits" "bald eagle" "+")
((((((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
((((((((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int4
The tiger does not visit the bald eagle.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule7)) -> rule1) OR ((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule1))]
("tiger" "visits" "bald eagle" "-")
((((((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
((((((((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int4
The tiger eats the bear.
True
5
proof
[(((((((((triple2) -> rule6)) -> rule7)) -> rule1)) -> rule3) OR ((((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule1)) -> rule3))]
("tiger" "eats" "bear" "+")
((((((((triple2) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
((((((((((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int5
The tiger does not eat the bear.
False
5
inv-proof
[(((((((((triple2) -> rule6)) -> rule7)) -> rule1)) -> rule3) OR ((((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule1)) -> rule3))]
("tiger" "eats" "bear" "-")
((((((((triple2) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
((((((((((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int5
The tiger eats the dog.
True
6
proof
[(((((((((((triple2) -> rule6)) -> rule7)) -> rule1)) -> rule3)) -> rule9) OR ((((((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule1)) -> rule3)) -> rule9))]
("tiger" "eats" "dog" "+")
((((((((((triple2) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
int5
((((((((((((triple10) -> (rule4 % int6))) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
int5
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int6
The tiger does not eat the dog.
False
6
inv-proof
[(((((((((((triple2) -> rule6)) -> rule7)) -> rule1)) -> rule3)) -> rule9) OR ((((((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule1)) -> rule3)) -> rule9))]
("tiger" "eats" "dog" "-")
((((((((((triple2) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
int5
((((((((((((triple10) -> (rule4 % int6))) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
int5
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int6
The dog does not visit the bald eagle.
Unknown
inv-rconc
[@2: The dog visits the bald eagle.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("dog" "visits" "bald eagle" "-")
The bald eagle eats the dog.
Unknown
rconc
[@4: The bald eagle eats the dog.[CWA. Example of deepest failure = (rule9 <- rule3 <- rule1 <- rule7 <- FAIL)]]
("bald eagle" "eats" "dog" "+")
The bald eagle does not visit the dog.
Unknown
inv-rconc
[@1: The bald eagle visits the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "visits" "dog" "-")
The bear eats the bear.
Unknown
rconc
[@3: The bear eats the bear.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule7 <- FAIL)]]
("bear" "eats" "bear" "+")
The bald eagle does not visit the bald eagle.
Unknown
inv-rconc
[@2: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("bald eagle" "visits" "bald eagle" "-")
The bear eats the dog.
Unknown
rconc
[@4: The bear eats the dog.[CWA. Example of deepest failure = (rule9 <- rule3 <- rule1 <- rule7 <- FAIL)]]
("bear" "eats" "dog" "+")
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 bald eagle is blue.
Unknown
random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The bald eagle is young.[(triple1)] The bear eats the tiger.[(triple2 OR ((triple10) -> rule4))] The bear is rough.[(triple3)] The bear is young.[(triple4)] The bear needs the bald eagle.[(triple5)] The dog eats the bald eagle.[(triple6)] The dog eats the tiger.[(triple7)] The dog visits the tiger.[(triple8)] The tiger is young.[(triple9)] The tiger needs the bear.[(triple10)] @1: The dog eats the bear.[(((triple6 triple7) -> rule2))] The tiger is round.[(((triple2) -> rule6) OR ((((triple10) -> rule4)) -> rule6))] @2: The dog eats the dog.[(((((triple6 triple7) -> rule2)) -> rule9))] The tiger visits the dog.[(((((triple2) -> rule6)) -> rule7) OR ((((((triple10) -> rule4)) -> rule6)) -> rule7))] @3: The dog needs the tiger.[(((((((triple2) -> rule6)) -> rule7)) -> rule5) OR ((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule5))] The tiger visits the bald eagle.[(((((((triple2) -> rule6)) -> rule7)) -> rule1) OR ((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule1))] @4: The tiger eats the bear.[(((((((((triple2) -> rule6)) -> rule7)) -> rule1)) -> rule3) OR ((((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule1)) -> rule3))] @5: The tiger eats the dog.[(((((((((((triple2) -> rule6)) -> rule7)) -> rule1)) -> rule3)) -> rule9) OR ((((((((((((triple10) -> rule4)) -> rule6)) -> rule7)) -> rule1)) -> rule3)) -> rule9))]
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
((triple10) -> (rule4 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
triple4
The bear needs the bald eagle.
("bear" "needs" "bald eagle" "+")
triple5
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
triple6
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple7
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple8
The tiger is young.
("tiger" "is" "young" "+")
triple9
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple10
The dog eats the bear.
("dog" "eats" "bear" "+")
((triple6 triple7) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple2) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
((((triple6 triple7) -> (rule2 % int2))) -> (rule9 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
((((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((((((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
((((((((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int4
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
((((((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
((((((((triple10) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int4
The tiger eats the bear.
("tiger" "eats" "bear" "+")
((((((((triple2) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
((((((((((triple10) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int5
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((((((((((triple2) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
int5
((((((((((((triple10) -> (rule4 % int6))) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
int5
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int6