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