The bald eagle does not eat the squirrel. The bald eagle is green. The bald eagle is young. The bald eagle likes the squirrel. The bald eagle likes the tiger. The bear does not eat the bald eagle. The bear is big. The bear is young. The bear likes the squirrel. The squirrel eats the bear. The squirrel does not like the bald eagle. The squirrel does not see the bear. The tiger is not rough. The tiger likes the bald eagle. If something sees the bald eagle then it sees the squirrel. If something is young and it eats the bear then the bear eats the tiger. If the bear sees the squirrel then the squirrel sees the bald eagle. If something sees the bear then the bear sees the bald eagle. If something is young then it sees the bear.
The bald eagle does not eat the squirrel.
("bald eagle" "eats" "squirrel" "-")
The bald eagle is green.
("bald eagle" "is" "green" "+")
The bald eagle is young.
("bald eagle" "is" "young" "+")
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
The bear does not eat the bald eagle.
("bear" "eats" "bald eagle" "-")
The bear is big.
("bear" "is" "big" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
If something sees the bald eagle then it sees the squirrel.
((("something" "sees" "bald eagle" "+")) -> ("something" "sees" "squirrel" "+"))
If something is young and it eats the bear then the bear eats the tiger.
((("something" "is" "young" "+") ("something" "eats" "bear" "+")) -> ("bear" "eats" "tiger" "+"))
If the bear sees the squirrel then the squirrel sees the bald eagle.
((("bear" "sees" "squirrel" "+")) -> ("squirrel" "sees" "bald eagle" "+"))
If something sees the bear then the bear sees the bald eagle.
((("something" "sees" "bear" "+")) -> ("bear" "sees" "bald eagle" "+"))
If something is young then it sees the bear.
((("something" "is" "young" "+")) -> ("something" "sees" "bear" "+"))
The bear is big.
True
1
proof
[(triple7)]
("bear" "is" "big" "+")
triple7
The bald eagle is not green.
False
1
inv-proof
[(triple2)]
("bald eagle" "is" "green" "-")
triple2
The bald eagle sees the bear.
True
2
proof
[(((triple3) -> rule5))]
("bald eagle" "sees" "bear" "+")
((triple3) -> (rule5 % int1))
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int1
The bear does not see the bear.
False
2
inv-proof
[(((triple8) -> rule5))]
("bear" "sees" "bear" "-")
((triple8) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear sees the bald eagle.
True
3
proof
[(((((triple3) -> rule5)) -> rule4) OR ((((triple8) -> rule5)) -> rule4))]
("bear" "sees" "bald eagle" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule4 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear does not see the bald eagle.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule4) OR ((((triple8) -> rule5)) -> rule4))]
("bear" "sees" "bald eagle" "-")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule4 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear sees the squirrel.
True
4
proof
[(((((((triple3) -> rule5)) -> rule4)) -> rule1) OR ((((((triple8) -> rule5)) -> rule4)) -> rule1))]
("bear" "sees" "squirrel" "+")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int2
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int3
((((((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The bear does not see the squirrel.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule4)) -> rule1) OR ((((((triple8) -> rule5)) -> rule4)) -> rule1))]
("bear" "sees" "squirrel" "-")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int2
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int3
((((((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The squirrel sees the bald eagle.
True
5
proof
[(((((((((triple3) -> rule5)) -> rule4)) -> rule1)) -> rule3) OR ((((((((triple8) -> rule5)) -> rule4)) -> rule1)) -> rule3))]
("squirrel" "sees" "bald eagle" "+")
((((((((triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int3
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int4
((((((((triple8) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4
The squirrel does not see the bald eagle.
False
5
inv-proof
[(((((((((triple3) -> rule5)) -> rule4)) -> rule1)) -> rule3) OR ((((((((triple8) -> rule5)) -> rule4)) -> rule1)) -> rule3))]
("squirrel" "sees" "bald eagle" "-")
((((((((triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int3
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int4
((((((((triple8) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4
The squirrel sees the squirrel.
True
6
proof
[(((((((((((triple3) -> rule5)) -> rule4)) -> rule1)) -> rule3)) -> rule1) OR ((((((((((triple8) -> rule5)) -> rule4)) -> rule1)) -> rule3)) -> rule1))]
("squirrel" "sees" "squirrel" "+")
((((((((((triple3) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int3
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int4
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int5
((((((((((triple8) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int3
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int4
The bear sees the bear.
("bear" "sees" "bear" "+")
int5
The squirrel does not see the squirrel.
False
6
inv-proof
[(((((((((((triple3) -> rule5)) -> rule4)) -> rule1)) -> rule3)) -> rule1) OR ((((((((((triple8) -> rule5)) -> rule4)) -> rule1)) -> rule3)) -> rule1))]
("squirrel" "sees" "squirrel" "-")
((((((((((triple3) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int3
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int4
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int5
((((((((((triple8) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int3
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int4
The bear sees the bear.
("bear" "sees" "bear" "+")
int5
The bear does not eat the tiger.
Unknown
inv-rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "tiger" "-")
The tiger sees the squirrel.
Unknown
rconc
[@1: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "squirrel" "+")
The tiger does not see the bear.
Unknown
inv-rconc
[@1: The tiger sees the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "sees" "bear" "-")
The bald eagle sees the squirrel.
Unknown
rconc
[@1: The bald eagle sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "sees" "squirrel" "+")
The bald eagle does not eat the bear.
Unknown
inv-random
[@0: The bald eagle eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bear" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The tiger does not like the bear.
Unknown
inv-random
[@0: The tiger likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "bear" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
The squirrel does not see the tiger.
Unknown
inv-random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The tiger does not eat the squirrel.
Unknown
inv-random
[@0: The tiger eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "squirrel" "-")
The tiger likes the squirrel.
Unknown
random
[@0: The tiger likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "squirrel" "+")
@0: The bald eagle does not eat the squirrel.[(triple1)] The bald eagle is green.[(triple2)] The bald eagle is young.[(triple3)] The bald eagle likes the squirrel.[(triple4)] The bald eagle likes the tiger.[(triple5)] The bear does not eat the bald eagle.[(triple6)] The bear is big.[(triple7)] The bear is young.[(triple8)] The bear likes the squirrel.[(triple9)] The squirrel does not like the bald eagle.[(triple11)] The squirrel does not see the bear.[(triple12)] The squirrel eats the bear.[(triple10)] The tiger is not rough.[(triple13)] The tiger likes the bald eagle.[(triple14)] @1: The bald eagle sees the bear.[(((triple3) -> rule5))] The bear sees the bear.[(((triple8) -> rule5))] @2: The bear sees the bald eagle.[(((((triple3) -> rule5)) -> rule4) OR ((((triple8) -> rule5)) -> rule4))] @3: The bear sees the squirrel.[(((((((triple3) -> rule5)) -> rule4)) -> rule1) OR ((((((triple8) -> rule5)) -> rule4)) -> rule1))] @4: The squirrel sees the bald eagle.[(((((((((triple3) -> rule5)) -> rule4)) -> rule1)) -> rule3) OR ((((((((triple8) -> rule5)) -> rule4)) -> rule1)) -> rule3))] @5: The squirrel sees the squirrel.[(((((((((((triple3) -> rule5)) -> rule4)) -> rule1)) -> rule3)) -> rule1) OR ((((((((((triple8) -> rule5)) -> rule4)) -> rule1)) -> rule3)) -> rule1))]
The bald eagle does not eat the squirrel.
("bald eagle" "eats" "squirrel" "-")
triple1
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple2
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple3
The bald eagle likes the squirrel.
("bald eagle" "likes" "squirrel" "+")
triple4
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
triple5
The bear does not eat the bald eagle.
("bear" "eats" "bald eagle" "-")
triple6
The bear is big.
("bear" "is" "big" "+")
triple7
The bear is young.
("bear" "is" "young" "+")
triple8
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple9
The squirrel does not like the bald eagle.
("squirrel" "likes" "bald eagle" "-")
triple11
The squirrel does not see the bear.
("squirrel" "sees" "bear" "-")
triple12
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple10
The tiger is not rough.
("tiger" "is" "rough" "-")
triple13
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
triple14
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
((triple3) -> (rule5 % int1))
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple8) -> (rule5 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule4 % int1))
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int2
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int3
((((((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
int3
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
((((((((triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int3
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int4
((((((((triple8) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((((((((triple3) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int3
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int4
The bald eagle sees the bear.
("bald eagle" "sees" "bear" "+")
int5
((((((((((triple8) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int3
The bear sees the bald eagle.
("bear" "sees" "bald eagle" "+")
int4
The bear sees the bear.
("bear" "sees" "bear" "+")
int5