YES(?,O(n^1)) 16.27/4.35 YES(?,O(n^1)) 16.27/4.37 16.27/4.37 Problem: 16.27/4.37 active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z))) 16.27/4.37 active(__(X,nil())) -> mark(X) 16.27/4.37 active(__(nil(),X)) -> mark(X) 16.27/4.37 active(and(tt(),X)) -> mark(X) 16.27/4.37 active(isList(V)) -> mark(isNeList(V)) 16.27/4.37 active(isList(nil())) -> mark(tt()) 16.27/4.37 active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2))) 16.27/4.37 active(isNeList(V)) -> mark(isQid(V)) 16.27/4.37 active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2))) 16.27/4.37 active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2))) 16.27/4.37 active(isNePal(V)) -> mark(isQid(V)) 16.27/4.37 active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P))) 16.27/4.37 active(isPal(V)) -> mark(isNePal(V)) 16.27/4.37 active(isPal(nil())) -> mark(tt()) 16.27/4.37 active(isQid(a())) -> mark(tt()) 16.27/4.37 active(isQid(e())) -> mark(tt()) 16.27/4.37 active(isQid(i())) -> mark(tt()) 16.27/4.37 active(isQid(o())) -> mark(tt()) 16.27/4.37 active(isQid(u())) -> mark(tt()) 16.27/4.37 active(__(X1,X2)) -> __(active(X1),X2) 16.27/4.37 active(__(X1,X2)) -> __(X1,active(X2)) 16.27/4.37 active(and(X1,X2)) -> and(active(X1),X2) 16.27/4.37 __(mark(X1),X2) -> mark(__(X1,X2)) 16.27/4.37 __(X1,mark(X2)) -> mark(__(X1,X2)) 16.27/4.37 and(mark(X1),X2) -> mark(and(X1,X2)) 16.27/4.37 proper(__(X1,X2)) -> __(proper(X1),proper(X2)) 16.27/4.37 proper(nil()) -> ok(nil()) 16.27/4.37 proper(and(X1,X2)) -> and(proper(X1),proper(X2)) 16.27/4.37 proper(tt()) -> ok(tt()) 16.27/4.37 proper(isList(X)) -> isList(proper(X)) 16.27/4.37 proper(isNeList(X)) -> isNeList(proper(X)) 16.27/4.37 proper(isQid(X)) -> isQid(proper(X)) 16.27/4.37 proper(isNePal(X)) -> isNePal(proper(X)) 16.27/4.37 proper(isPal(X)) -> isPal(proper(X)) 16.27/4.37 proper(a()) -> ok(a()) 16.27/4.37 proper(e()) -> ok(e()) 16.27/4.37 proper(i()) -> ok(i()) 16.27/4.37 proper(o()) -> ok(o()) 16.27/4.37 proper(u()) -> ok(u()) 16.27/4.37 __(ok(X1),ok(X2)) -> ok(__(X1,X2)) 16.27/4.37 and(ok(X1),ok(X2)) -> ok(and(X1,X2)) 16.27/4.37 isList(ok(X)) -> ok(isList(X)) 16.27/4.37 isNeList(ok(X)) -> ok(isNeList(X)) 16.27/4.37 isQid(ok(X)) -> ok(isQid(X)) 16.27/4.37 isNePal(ok(X)) -> ok(isNePal(X)) 16.27/4.37 isPal(ok(X)) -> ok(isPal(X)) 16.27/4.37 top(mark(X)) -> top(proper(X)) 16.27/4.37 top(ok(X)) -> top(active(X)) 16.27/4.37 16.27/4.37 Proof: 16.27/4.37 Bounds Processor: 16.27/4.37 bound: 2 16.27/4.37 enrichment: match 16.27/4.37 automaton: 16.27/4.37 final states: {30,29,19,18,17,16,15,14,13,12,11,10} 16.27/4.37 transitions: 16.27/4.37 active0(35) -> 10* 16.27/4.37 active0(30) -> 10* 16.27/4.37 active0(5) -> 10* 16.27/4.37 active0(32) -> 10* 16.27/4.37 active0(7) -> 10* 16.27/4.37 active0(2) -> 10* 16.27/4.37 active0(34) -> 10* 16.27/4.37 active0(9) -> 10* 16.27/4.37 active0(4) -> 10* 16.27/4.37 active0(36) -> 10* 16.27/4.37 active0(31) -> 10* 16.27/4.37 active0(6) -> 10* 16.27/4.37 active0(1) -> 10* 16.27/4.37 active0(33) -> 10* 16.27/4.37 active0(8) -> 10* 16.27/4.37 active0(3) -> 10* 16.27/4.37 __0(31,35) -> 11* 16.27/4.37 __0(6,31) -> 11* 16.27/4.37 __0(1,31) -> 11* 16.27/4.37 __0(6,33) -> 11* 16.27/4.37 __0(1,33) -> 11* 16.27/4.37 __0(6,35) -> 11* 16.27/4.37 __0(33,1) -> 11* 16.27/4.37 __0(1,35) -> 11* 16.27/4.37 __0(33,3) -> 11* 16.27/4.37 __0(33,5) -> 11* 16.27/4.37 __0(8,1) -> 11* 16.27/4.37 __0(3,1) -> 11* 16.27/4.37 __0(33,7) -> 11* 16.27/4.37 __0(8,3) -> 11* 16.27/4.37 __0(3,3) -> 11* 16.27/4.37 __0(33,9) -> 11* 16.27/4.37 __0(8,5) -> 11* 16.27/4.37 __0(32,30) -> 11* 16.27/4.37 __0(3,5) -> 11* 16.27/4.37 __0(8,7) -> 11* 16.27/4.37 __0(32,32) -> 11* 16.27/4.37 __0(3,7) -> 11* 16.27/4.37 __0(8,9) -> 11* 16.27/4.37 __0(32,34) -> 11* 16.27/4.37 __0(3,9) -> 11* 16.27/4.37 __0(7,30) -> 11* 16.27/4.37 __0(32,36) -> 11* 16.27/4.37 __0(2,30) -> 11* 16.27/4.37 __0(7,32) -> 11* 16.27/4.37 __0(2,32) -> 11* 16.27/4.37 __0(7,34) -> 11* 16.27/4.37 __0(2,34) -> 11* 16.27/4.37 __0(7,36) -> 11* 16.27/4.37 __0(34,2) -> 11* 16.27/4.37 __0(2,36) -> 11* 16.27/4.37 __0(34,4) -> 11* 16.27/4.37 __0(34,6) -> 11* 16.27/4.37 __0(9,2) -> 11* 16.27/4.37 __0(4,2) -> 11* 16.27/4.37 __0(34,8) -> 11* 16.27/4.37 __0(9,4) -> 11* 16.27/4.37 __0(4,4) -> 11* 16.27/4.37 __0(9,6) -> 11* 16.27/4.37 __0(33,31) -> 11* 16.27/4.37 __0(4,6) -> 11* 16.27/4.37 __0(9,8) -> 11* 16.27/4.37 __0(33,33) -> 11* 16.27/4.37 __0(4,8) -> 11* 16.27/4.37 __0(33,35) -> 11* 16.27/4.37 __0(8,31) -> 11* 16.27/4.37 __0(3,31) -> 11* 16.27/4.37 __0(8,33) -> 11* 16.27/4.37 __0(3,33) -> 11* 16.27/4.37 __0(8,35) -> 11* 16.27/4.37 __0(35,1) -> 11* 16.27/4.37 __0(3,35) -> 11* 16.27/4.37 __0(30,1) -> 11* 16.27/4.37 __0(35,3) -> 11* 16.27/4.37 __0(30,3) -> 11* 16.27/4.37 __0(35,5) -> 11* 16.27/4.37 __0(30,5) -> 11* 16.27/4.37 __0(5,1) -> 11* 16.27/4.37 __0(35,7) -> 11* 16.27/4.37 __0(30,7) -> 11* 16.27/4.37 __0(5,3) -> 11* 16.27/4.37 __0(35,9) -> 11* 16.27/4.37 __0(30,9) -> 11* 16.27/4.37 __0(34,30) -> 11* 16.27/4.37 __0(5,5) -> 11* 16.27/4.37 __0(34,32) -> 11* 16.27/4.37 __0(5,7) -> 11* 16.27/4.37 __0(34,34) -> 11* 16.27/4.37 __0(5,9) -> 11* 16.27/4.37 __0(9,30) -> 11* 16.27/4.37 __0(34,36) -> 11* 16.27/4.37 __0(4,30) -> 11* 16.27/4.37 __0(9,32) -> 11* 16.27/4.37 __0(4,32) -> 11* 16.27/4.37 __0(9,34) -> 11* 16.27/4.37 __0(4,34) -> 11* 16.27/4.37 __0(9,36) -> 11* 16.27/4.37 __0(36,2) -> 11* 16.27/4.37 __0(4,36) -> 11* 16.27/4.37 __0(31,2) -> 11* 16.27/4.37 __0(36,4) -> 11* 16.27/4.37 __0(31,4) -> 11* 16.27/4.38 __0(36,6) -> 11* 16.27/4.38 __0(31,6) -> 11* 16.27/4.38 __0(6,2) -> 11* 16.27/4.38 __0(36,8) -> 11* 16.27/4.38 __0(1,2) -> 11* 16.27/4.38 __0(31,8) -> 11* 16.27/4.38 __0(6,4) -> 11* 16.27/4.38 __0(1,4) -> 11* 16.27/4.38 __0(35,31) -> 11* 16.27/4.38 __0(6,6) -> 11* 16.27/4.38 __0(30,31) -> 11* 16.27/4.38 __0(1,6) -> 11* 16.27/4.38 __0(35,33) -> 11* 16.27/4.38 __0(6,8) -> 11* 16.27/4.38 __0(30,33) -> 11* 16.27/4.38 __0(1,8) -> 11* 16.27/4.38 __0(35,35) -> 11* 16.27/4.38 __0(30,35) -> 11* 16.27/4.38 __0(5,31) -> 11* 16.27/4.38 __0(5,33) -> 11* 16.27/4.38 __0(5,35) -> 11* 16.27/4.38 __0(32,1) -> 11* 16.27/4.38 __0(32,3) -> 11* 16.27/4.38 __0(32,5) -> 11* 16.27/4.38 __0(7,1) -> 11* 16.27/4.38 __0(2,1) -> 11* 16.27/4.38 __0(32,7) -> 11* 16.27/4.38 __0(7,3) -> 11* 16.27/4.38 __0(2,3) -> 11* 16.27/4.38 __0(32,9) -> 11* 16.27/4.38 __0(36,30) -> 11* 16.27/4.38 __0(7,5) -> 11* 16.27/4.38 __0(31,30) -> 11* 16.27/4.38 __0(2,5) -> 11* 16.27/4.38 __0(36,32) -> 11* 16.27/4.38 __0(7,7) -> 11* 16.27/4.38 __0(31,32) -> 11* 16.27/4.38 __0(2,7) -> 11* 16.27/4.38 __0(36,34) -> 11* 16.27/4.38 __0(7,9) -> 11* 16.27/4.38 __0(31,34) -> 11* 16.27/4.38 __0(2,9) -> 11* 16.27/4.38 __0(36,36) -> 11* 16.27/4.38 __0(6,30) -> 11* 16.27/4.38 __0(31,36) -> 11* 16.27/4.38 __0(1,30) -> 11* 16.27/4.38 __0(6,32) -> 11* 16.27/4.38 __0(1,32) -> 11* 16.27/4.38 __0(6,34) -> 11* 16.27/4.38 __0(1,34) -> 11* 16.27/4.38 __0(6,36) -> 11* 16.27/4.38 __0(33,2) -> 11* 16.27/4.38 __0(1,36) -> 11* 16.27/4.38 __0(33,4) -> 11* 16.27/4.38 __0(33,6) -> 11* 16.27/4.38 __0(8,2) -> 11* 16.27/4.38 __0(3,2) -> 11* 16.27/4.38 __0(33,8) -> 11* 16.27/4.38 __0(8,4) -> 11* 16.27/4.38 __0(3,4) -> 11* 16.27/4.38 __0(8,6) -> 11* 16.27/4.38 __0(32,31) -> 11* 16.27/4.38 __0(3,6) -> 11* 16.27/4.38 __0(8,8) -> 11* 16.27/4.38 __0(32,33) -> 11* 16.27/4.38 __0(3,8) -> 11* 16.27/4.38 __0(32,35) -> 11* 16.27/4.38 __0(7,31) -> 11* 16.27/4.38 __0(2,31) -> 11* 16.27/4.38 __0(7,33) -> 11* 16.27/4.38 __0(2,33) -> 11* 16.27/4.38 __0(7,35) -> 11* 16.27/4.38 __0(34,1) -> 11* 16.27/4.38 __0(2,35) -> 11* 16.27/4.38 __0(34,3) -> 11* 16.27/4.38 __0(34,5) -> 11* 16.27/4.38 __0(9,1) -> 11* 16.27/4.38 __0(4,1) -> 11* 16.27/4.38 __0(34,7) -> 11* 16.27/4.38 __0(9,3) -> 11* 16.27/4.38 __0(4,3) -> 11* 16.27/4.38 __0(34,9) -> 11* 16.27/4.38 __0(9,5) -> 11* 16.27/4.38 __0(33,30) -> 11* 16.27/4.38 __0(4,5) -> 11* 16.27/4.38 __0(9,7) -> 11* 16.27/4.38 __0(33,32) -> 11* 16.27/4.38 __0(4,7) -> 11* 16.27/4.38 __0(9,9) -> 11* 16.27/4.38 __0(33,34) -> 11* 16.27/4.38 __0(4,9) -> 11* 16.27/4.38 __0(8,30) -> 11* 16.27/4.38 __0(33,36) -> 11* 16.27/4.38 __0(3,30) -> 11* 16.27/4.38 __0(8,32) -> 11* 16.27/4.38 __0(3,32) -> 11* 16.27/4.38 __0(8,34) -> 11* 16.27/4.38 __0(3,34) -> 11* 16.27/4.38 __0(8,36) -> 11* 16.27/4.38 __0(35,2) -> 11* 16.27/4.38 __0(3,36) -> 11* 16.27/4.38 __0(30,2) -> 11* 16.27/4.38 __0(35,4) -> 11* 16.27/4.38 __0(30,4) -> 11* 16.27/4.38 __0(35,6) -> 11* 16.27/4.38 __0(30,6) -> 11* 16.27/4.38 __0(5,2) -> 11* 16.27/4.38 __0(35,8) -> 11* 16.27/4.38 __0(30,8) -> 11* 16.27/4.38 __0(5,4) -> 11* 16.27/4.38 __0(34,31) -> 11* 16.27/4.38 __0(5,6) -> 11* 16.27/4.38 __0(34,33) -> 11* 16.27/4.38 __0(5,8) -> 11* 16.27/4.38 __0(34,35) -> 11* 16.27/4.38 __0(9,31) -> 11* 16.27/4.38 __0(4,31) -> 11* 16.27/4.38 __0(9,33) -> 11* 16.27/4.38 __0(4,33) -> 11* 16.27/4.38 __0(9,35) -> 11* 16.27/4.38 __0(36,1) -> 11* 16.27/4.38 __0(4,35) -> 11* 16.27/4.38 __0(31,1) -> 11* 16.27/4.38 __0(36,3) -> 11* 16.27/4.38 __0(31,3) -> 11* 16.27/4.38 __0(36,5) -> 11* 16.27/4.38 __0(31,5) -> 11* 16.27/4.38 __0(6,1) -> 11* 16.27/4.38 __0(36,7) -> 11* 16.27/4.38 __0(1,1) -> 11* 16.27/4.38 __0(31,7) -> 11* 16.27/4.38 __0(6,3) -> 11* 16.27/4.38 __0(36,9) -> 11* 16.27/4.38 __0(1,3) -> 11* 16.27/4.38 __0(31,9) -> 11* 16.27/4.38 __0(35,30) -> 11* 16.27/4.38 __0(6,5) -> 11* 16.27/4.38 __0(30,30) -> 11* 16.27/4.38 __0(1,5) -> 11* 16.27/4.38 __0(35,32) -> 11* 16.27/4.38 __0(6,7) -> 11* 16.27/4.38 __0(30,32) -> 11* 16.27/4.38 __0(1,7) -> 11* 16.27/4.38 __0(35,34) -> 11* 16.27/4.38 __0(6,9) -> 11* 16.27/4.38 __0(30,34) -> 11* 16.27/4.38 __0(1,9) -> 11* 16.27/4.38 __0(35,36) -> 11* 16.27/4.38 __0(5,30) -> 11* 16.27/4.38 __0(30,36) -> 11* 16.27/4.38 __0(5,32) -> 11* 16.27/4.38 __0(5,34) -> 11* 16.27/4.38 __0(5,36) -> 11* 16.27/4.38 __0(32,2) -> 11* 16.27/4.38 __0(32,4) -> 11* 16.27/4.38 __0(32,6) -> 11* 16.27/4.38 __0(7,2) -> 11* 16.27/4.38 __0(2,2) -> 11* 16.27/4.38 __0(32,8) -> 11* 16.27/4.38 __0(7,4) -> 11* 16.27/4.38 __0(2,4) -> 11* 16.27/4.38 __0(36,31) -> 11* 16.27/4.38 __0(7,6) -> 11* 16.27/4.38 __0(31,31) -> 11* 16.27/4.38 __0(2,6) -> 11* 16.27/4.38 __0(36,33) -> 11* 16.27/4.38 __0(7,8) -> 11* 16.27/4.38 __0(31,33) -> 11* 16.27/4.38 __0(2,8) -> 11* 16.27/4.38 __0(36,35) -> 11* 16.27/4.38 mark0(35) -> 1* 16.27/4.38 mark0(30) -> 1* 16.27/4.38 mark0(5) -> 1* 16.27/4.38 mark0(32) -> 1* 16.27/4.38 mark0(7) -> 1* 16.27/4.38 mark0(2) -> 1* 16.27/4.38 mark0(34) -> 1* 16.27/4.38 mark0(9) -> 1* 16.27/4.38 mark0(4) -> 1* 16.27/4.38 mark0(36) -> 1* 16.27/4.38 mark0(31) -> 1* 16.27/4.38 mark0(6) -> 1* 16.27/4.38 mark0(1) -> 1* 16.27/4.38 mark0(33) -> 1* 16.27/4.38 mark0(8) -> 1* 16.27/4.38 mark0(3) -> 1* 16.27/4.38 nil0() -> 2* 16.27/4.38 and0(31,35) -> 12* 16.27/4.38 and0(6,31) -> 12* 16.27/4.38 and0(1,31) -> 12* 16.27/4.38 and0(6,33) -> 12* 16.27/4.38 and0(1,33) -> 12* 16.27/4.38 and0(6,35) -> 12* 16.27/4.38 and0(33,1) -> 12* 16.27/4.38 and0(1,35) -> 12* 16.27/4.38 and0(33,3) -> 12* 16.27/4.38 and0(33,5) -> 12* 16.27/4.38 and0(8,1) -> 12* 16.27/4.38 and0(3,1) -> 12* 16.27/4.38 and0(33,7) -> 12* 16.27/4.38 and0(8,3) -> 12* 16.27/4.38 and0(3,3) -> 12* 16.27/4.38 and0(33,9) -> 12* 16.27/4.38 and0(8,5) -> 12* 16.27/4.38 and0(32,30) -> 12* 16.27/4.38 and0(3,5) -> 12* 16.27/4.38 and0(8,7) -> 12* 16.27/4.38 and0(32,32) -> 12* 16.27/4.38 and0(3,7) -> 12* 16.27/4.38 and0(8,9) -> 12* 16.27/4.38 and0(32,34) -> 12* 16.27/4.38 and0(3,9) -> 12* 16.27/4.38 and0(7,30) -> 12* 16.27/4.38 and0(32,36) -> 12* 16.27/4.38 and0(2,30) -> 12* 16.27/4.38 and0(7,32) -> 12* 16.27/4.38 and0(2,32) -> 12* 16.27/4.38 and0(7,34) -> 12* 16.27/4.38 and0(2,34) -> 12* 16.27/4.38 and0(7,36) -> 12* 16.27/4.38 and0(34,2) -> 12* 16.27/4.38 and0(2,36) -> 12* 16.27/4.38 and0(34,4) -> 12* 16.27/4.38 and0(34,6) -> 12* 16.27/4.38 and0(9,2) -> 12* 16.27/4.38 and0(4,2) -> 12* 16.27/4.38 and0(34,8) -> 12* 16.27/4.38 and0(9,4) -> 12* 16.27/4.38 and0(4,4) -> 12* 16.27/4.38 and0(9,6) -> 12* 16.27/4.38 and0(33,31) -> 12* 16.27/4.38 and0(4,6) -> 12* 16.27/4.38 and0(9,8) -> 12* 16.27/4.38 and0(33,33) -> 12* 16.27/4.38 and0(4,8) -> 12* 16.27/4.38 and0(33,35) -> 12* 16.27/4.38 and0(8,31) -> 12* 16.27/4.38 and0(3,31) -> 12* 16.27/4.38 and0(8,33) -> 12* 16.27/4.38 and0(3,33) -> 12* 16.27/4.38 and0(8,35) -> 12* 16.27/4.38 and0(35,1) -> 12* 16.27/4.38 and0(3,35) -> 12* 16.27/4.38 and0(30,1) -> 12* 16.27/4.38 and0(35,3) -> 12* 16.27/4.38 and0(30,3) -> 12* 16.27/4.38 and0(35,5) -> 12* 16.27/4.38 and0(30,5) -> 12* 16.27/4.38 and0(5,1) -> 12* 16.27/4.38 and0(35,7) -> 12* 16.27/4.38 and0(30,7) -> 12* 16.27/4.38 and0(5,3) -> 12* 16.27/4.38 and0(35,9) -> 12* 16.27/4.38 and0(30,9) -> 12* 16.27/4.38 and0(34,30) -> 12* 16.27/4.38 and0(5,5) -> 12* 16.27/4.38 and0(34,32) -> 12* 16.27/4.38 and0(5,7) -> 12* 16.27/4.38 and0(34,34) -> 12* 16.27/4.38 and0(5,9) -> 12* 16.27/4.38 and0(9,30) -> 12* 16.27/4.38 and0(34,36) -> 12* 16.27/4.38 and0(4,30) -> 12* 16.27/4.38 and0(9,32) -> 12* 16.27/4.38 and0(4,32) -> 12* 16.27/4.38 and0(9,34) -> 12* 16.27/4.38 and0(4,34) -> 12* 16.27/4.38 and0(9,36) -> 12* 16.27/4.38 and0(36,2) -> 12* 16.27/4.38 and0(4,36) -> 12* 16.27/4.38 and0(31,2) -> 12* 16.27/4.38 and0(36,4) -> 12* 16.27/4.38 and0(31,4) -> 12* 16.27/4.38 and0(36,6) -> 12* 16.27/4.38 and0(31,6) -> 12* 16.27/4.38 and0(6,2) -> 12* 16.27/4.38 and0(36,8) -> 12* 16.27/4.38 and0(1,2) -> 12* 16.27/4.38 and0(31,8) -> 12* 16.27/4.38 and0(6,4) -> 12* 16.27/4.38 and0(1,4) -> 12* 16.27/4.38 and0(35,31) -> 12* 16.27/4.38 and0(6,6) -> 12* 16.27/4.38 and0(30,31) -> 12* 16.27/4.38 and0(1,6) -> 12* 16.27/4.38 and0(35,33) -> 12* 16.27/4.38 and0(6,8) -> 12* 16.27/4.38 and0(30,33) -> 12* 16.27/4.38 and0(1,8) -> 12* 16.27/4.38 and0(35,35) -> 12* 16.27/4.38 and0(30,35) -> 12* 16.27/4.38 and0(5,31) -> 12* 16.27/4.38 and0(5,33) -> 12* 16.27/4.38 and0(5,35) -> 12* 16.27/4.38 and0(32,1) -> 12* 16.27/4.38 and0(32,3) -> 12* 16.27/4.38 and0(32,5) -> 12* 16.27/4.38 and0(7,1) -> 12* 16.27/4.38 and0(2,1) -> 12* 16.27/4.38 and0(32,7) -> 12* 16.27/4.38 and0(7,3) -> 12* 16.27/4.38 and0(2,3) -> 12* 16.27/4.38 and0(32,9) -> 12* 16.27/4.38 and0(36,30) -> 12* 16.27/4.38 and0(7,5) -> 12* 16.27/4.38 and0(31,30) -> 12* 16.27/4.38 and0(2,5) -> 12* 16.27/4.38 and0(36,32) -> 12* 16.27/4.38 and0(7,7) -> 12* 16.27/4.38 and0(31,32) -> 12* 16.27/4.38 and0(2,7) -> 12* 16.27/4.38 and0(36,34) -> 12* 16.27/4.38 and0(7,9) -> 12* 16.27/4.38 and0(31,34) -> 12* 16.27/4.38 and0(2,9) -> 12* 16.27/4.38 and0(36,36) -> 12* 16.27/4.38 and0(6,30) -> 12* 16.27/4.38 and0(31,36) -> 12* 16.27/4.38 and0(1,30) -> 12* 16.27/4.38 and0(6,32) -> 12* 16.27/4.38 and0(1,32) -> 12* 16.27/4.38 and0(6,34) -> 12* 16.27/4.38 and0(1,34) -> 12* 16.27/4.38 and0(6,36) -> 12* 16.27/4.38 and0(33,2) -> 12* 16.27/4.38 and0(1,36) -> 12* 16.27/4.38 and0(33,4) -> 12* 16.27/4.38 and0(33,6) -> 12* 16.27/4.38 and0(8,2) -> 12* 16.27/4.38 and0(3,2) -> 12* 16.27/4.38 and0(33,8) -> 12* 16.27/4.38 and0(8,4) -> 12* 16.27/4.38 and0(3,4) -> 12* 16.27/4.38 and0(8,6) -> 12* 16.27/4.38 and0(32,31) -> 12* 16.27/4.38 and0(3,6) -> 12* 16.27/4.38 and0(8,8) -> 12* 16.27/4.38 and0(32,33) -> 12* 16.27/4.38 and0(3,8) -> 12* 16.27/4.38 and0(32,35) -> 12* 16.27/4.38 and0(7,31) -> 12* 16.27/4.38 and0(2,31) -> 12* 16.27/4.38 and0(7,33) -> 12* 16.27/4.38 and0(2,33) -> 12* 16.27/4.38 and0(7,35) -> 12* 16.27/4.38 and0(34,1) -> 12* 16.27/4.38 and0(2,35) -> 12* 16.27/4.38 and0(34,3) -> 12* 16.27/4.38 and0(34,5) -> 12* 16.27/4.38 and0(9,1) -> 12* 16.27/4.38 and0(4,1) -> 12* 16.27/4.38 and0(34,7) -> 12* 16.27/4.38 and0(9,3) -> 12* 16.27/4.38 and0(4,3) -> 12* 16.27/4.38 and0(34,9) -> 12* 16.27/4.38 and0(9,5) -> 12* 16.27/4.38 and0(33,30) -> 12* 16.27/4.38 and0(4,5) -> 12* 16.27/4.38 and0(9,7) -> 12* 16.27/4.38 and0(33,32) -> 12* 16.27/4.38 and0(4,7) -> 12* 16.27/4.38 and0(9,9) -> 12* 16.27/4.38 and0(33,34) -> 12* 16.27/4.38 and0(4,9) -> 12* 16.27/4.38 and0(8,30) -> 12* 16.27/4.38 and0(33,36) -> 12* 16.27/4.38 and0(3,30) -> 12* 16.27/4.38 and0(8,32) -> 12* 16.27/4.38 and0(3,32) -> 12* 16.27/4.38 and0(8,34) -> 12* 16.27/4.38 and0(3,34) -> 12* 16.27/4.38 and0(8,36) -> 12* 16.27/4.38 and0(35,2) -> 12* 16.27/4.38 and0(3,36) -> 12* 16.27/4.38 and0(30,2) -> 12* 16.27/4.38 and0(35,4) -> 12* 16.27/4.38 and0(30,4) -> 12* 16.27/4.38 and0(35,6) -> 12* 16.27/4.38 and0(30,6) -> 12* 16.27/4.38 and0(5,2) -> 12* 16.27/4.38 and0(35,8) -> 12* 16.27/4.38 and0(30,8) -> 12* 16.27/4.38 and0(5,4) -> 12* 16.27/4.38 and0(34,31) -> 12* 16.27/4.38 and0(5,6) -> 12* 16.27/4.38 and0(34,33) -> 12* 16.27/4.38 and0(5,8) -> 12* 16.27/4.38 and0(34,35) -> 12* 16.27/4.38 and0(9,31) -> 12* 16.27/4.38 and0(4,31) -> 12* 16.27/4.38 and0(9,33) -> 12* 16.27/4.38 and0(4,33) -> 12* 16.27/4.38 and0(9,35) -> 12* 16.27/4.38 and0(36,1) -> 12* 16.27/4.38 and0(4,35) -> 12* 16.27/4.38 and0(31,1) -> 12* 16.27/4.38 and0(36,3) -> 12* 16.27/4.38 and0(31,3) -> 12* 16.27/4.38 and0(36,5) -> 12* 16.27/4.38 and0(31,5) -> 12* 16.27/4.38 and0(6,1) -> 12* 16.27/4.38 and0(36,7) -> 12* 16.27/4.38 and0(1,1) -> 12* 16.27/4.38 and0(31,7) -> 12* 16.27/4.38 and0(6,3) -> 12* 16.27/4.38 and0(36,9) -> 12* 16.27/4.38 and0(1,3) -> 12* 16.27/4.38 and0(31,9) -> 12* 16.27/4.38 and0(35,30) -> 12* 16.27/4.38 and0(6,5) -> 12* 16.27/4.38 and0(30,30) -> 12* 16.27/4.38 and0(1,5) -> 12* 16.27/4.38 and0(35,32) -> 12* 16.27/4.38 and0(6,7) -> 12* 16.27/4.38 and0(30,32) -> 12* 16.27/4.38 and0(1,7) -> 12* 16.27/4.38 and0(35,34) -> 12* 16.27/4.38 and0(6,9) -> 12* 16.27/4.38 and0(30,34) -> 12* 16.27/4.38 and0(1,9) -> 12* 16.27/4.38 and0(35,36) -> 12* 16.27/4.38 and0(5,30) -> 12* 16.27/4.38 and0(30,36) -> 12* 16.27/4.38 and0(5,32) -> 12* 16.27/4.38 and0(5,34) -> 12* 16.27/4.38 and0(5,36) -> 12* 16.27/4.38 and0(32,2) -> 12* 16.27/4.38 and0(32,4) -> 12* 16.27/4.38 and0(32,6) -> 12* 16.27/4.38 and0(7,2) -> 12* 16.27/4.38 and0(2,2) -> 12* 16.27/4.38 and0(32,8) -> 12* 16.27/4.38 and0(7,4) -> 12* 16.27/4.38 and0(2,4) -> 12* 16.27/4.38 and0(36,31) -> 12* 16.27/4.38 and0(7,6) -> 12* 16.27/4.38 and0(31,31) -> 12* 16.27/4.38 and0(2,6) -> 12* 16.27/4.38 and0(36,33) -> 12* 16.27/4.38 and0(7,8) -> 12* 16.27/4.38 and0(31,33) -> 12* 16.27/4.38 and0(2,8) -> 12* 16.27/4.38 and0(36,35) -> 12* 16.27/4.38 tt0() -> 3* 16.27/4.38 isList0(35) -> 14* 16.27/4.38 isList0(30) -> 14* 16.27/4.38 isList0(5) -> 14* 16.27/4.38 isList0(32) -> 14* 16.27/4.38 isList0(7) -> 14* 16.27/4.38 isList0(2) -> 14* 16.27/4.38 isList0(34) -> 14* 16.27/4.38 isList0(9) -> 14* 16.27/4.38 isList0(4) -> 14* 16.27/4.38 isList0(36) -> 14* 16.27/4.38 isList0(31) -> 14* 16.27/4.38 isList0(6) -> 14* 16.27/4.38 isList0(1) -> 14* 16.27/4.38 isList0(33) -> 14* 16.27/4.38 isList0(8) -> 14* 16.27/4.38 isList0(3) -> 14* 16.27/4.38 isNeList0(35) -> 15* 16.27/4.38 isNeList0(30) -> 15* 16.27/4.38 isNeList0(5) -> 15* 16.27/4.38 isNeList0(32) -> 15* 16.27/4.38 isNeList0(7) -> 15* 16.27/4.38 isNeList0(2) -> 15* 16.27/4.38 isNeList0(34) -> 15* 16.27/4.38 isNeList0(9) -> 15* 16.27/4.38 isNeList0(4) -> 15* 16.27/4.38 isNeList0(36) -> 15* 16.27/4.38 isNeList0(31) -> 15* 16.27/4.38 isNeList0(6) -> 15* 16.27/4.38 isNeList0(1) -> 15* 16.27/4.38 isNeList0(33) -> 15* 16.27/4.38 isNeList0(8) -> 15* 16.27/4.38 isNeList0(3) -> 15* 16.27/4.39 isQid0(35) -> 16* 16.27/4.39 isQid0(30) -> 16* 16.27/4.39 isQid0(5) -> 16* 16.27/4.39 isQid0(32) -> 16* 16.27/4.39 isQid0(7) -> 16* 16.27/4.39 isQid0(2) -> 16* 16.27/4.39 isQid0(34) -> 16* 16.27/4.39 isQid0(9) -> 16* 16.27/4.39 isQid0(4) -> 16* 16.27/4.39 isQid0(36) -> 16* 16.27/4.39 isQid0(31) -> 16* 16.27/4.39 isQid0(6) -> 16* 16.27/4.39 isQid0(1) -> 16* 16.27/4.39 isQid0(33) -> 16* 16.27/4.39 isQid0(8) -> 16* 16.27/4.39 isQid0(3) -> 16* 16.27/4.39 isNePal0(35) -> 17* 16.27/4.39 isNePal0(30) -> 17* 16.27/4.39 isNePal0(5) -> 17* 16.27/4.39 isNePal0(32) -> 17* 16.27/4.39 isNePal0(7) -> 17* 16.27/4.39 isNePal0(2) -> 17* 16.27/4.39 isNePal0(34) -> 17* 16.27/4.39 isNePal0(9) -> 17* 16.27/4.39 isNePal0(4) -> 17* 16.27/4.39 isNePal0(36) -> 17* 16.27/4.39 isNePal0(31) -> 17* 16.27/4.39 isNePal0(6) -> 17* 16.27/4.39 isNePal0(1) -> 17* 16.27/4.39 isNePal0(33) -> 17* 16.27/4.39 isNePal0(8) -> 17* 16.27/4.39 isNePal0(3) -> 17* 16.27/4.39 isPal0(35) -> 18* 16.27/4.39 isPal0(30) -> 18* 16.27/4.39 isPal0(5) -> 18* 16.27/4.39 isPal0(32) -> 18* 16.27/4.39 isPal0(7) -> 18* 16.27/4.39 isPal0(2) -> 18* 16.27/4.39 isPal0(34) -> 18* 16.27/4.39 isPal0(9) -> 18* 16.27/4.39 isPal0(4) -> 18* 16.27/4.39 isPal0(36) -> 18* 16.27/4.39 isPal0(31) -> 18* 16.27/4.39 isPal0(6) -> 18* 16.27/4.39 isPal0(1) -> 18* 16.27/4.39 isPal0(33) -> 18* 16.27/4.39 isPal0(8) -> 18* 16.27/4.39 isPal0(3) -> 18* 16.27/4.39 a0() -> 4* 16.27/4.39 e0() -> 5* 16.27/4.39 i0() -> 6* 16.27/4.39 o0() -> 7* 16.27/4.39 u0() -> 8* 16.27/4.39 proper0(35) -> 13* 16.27/4.39 proper0(30) -> 13* 16.27/4.39 proper0(5) -> 13* 16.27/4.39 proper0(32) -> 13* 16.27/4.39 proper0(7) -> 13* 16.27/4.39 proper0(2) -> 13* 16.27/4.39 proper0(34) -> 13* 16.27/4.39 proper0(9) -> 13* 16.27/4.39 proper0(4) -> 13* 16.27/4.39 proper0(36) -> 13* 16.27/4.39 proper0(31) -> 13* 16.27/4.39 proper0(6) -> 13* 16.27/4.39 proper0(1) -> 13* 16.27/4.39 proper0(33) -> 13* 16.27/4.39 proper0(8) -> 13* 16.27/4.39 proper0(3) -> 13* 16.27/4.39 ok0(35) -> 9* 16.27/4.39 ok0(30) -> 9* 16.27/4.39 ok0(5) -> 9* 16.27/4.39 ok0(32) -> 9* 16.27/4.39 ok0(7) -> 9* 16.27/4.39 ok0(2) -> 9* 16.27/4.39 ok0(34) -> 9* 16.27/4.39 ok0(9) -> 9* 16.27/4.39 ok0(4) -> 9* 16.27/4.39 ok0(36) -> 9* 16.27/4.39 ok0(31) -> 9* 16.27/4.39 ok0(6) -> 9* 16.27/4.39 ok0(1) -> 9* 16.27/4.39 ok0(33) -> 9* 16.27/4.39 ok0(8) -> 9* 16.27/4.39 ok0(3) -> 9* 16.27/4.39 top0(35) -> 19* 16.27/4.39 top0(30) -> 19* 16.27/4.39 top0(5) -> 19* 16.27/4.39 top0(32) -> 19* 16.27/4.39 top0(7) -> 19* 16.27/4.39 top0(2) -> 19* 16.27/4.39 top0(34) -> 19* 16.27/4.39 top0(9) -> 19* 16.27/4.39 top0(4) -> 19* 16.27/4.39 top0(36) -> 19* 16.27/4.39 top0(31) -> 19* 16.27/4.39 top0(6) -> 19* 16.27/4.39 top0(1) -> 19* 16.27/4.39 top0(33) -> 19* 16.27/4.39 top0(8) -> 19* 16.27/4.39 top0(3) -> 19* 16.27/4.39 top1(30) -> 19* 16.27/4.39 top1(29) -> 19* 16.27/4.39 top1(13) -> 19* 16.27/4.39 active1(35) -> 10,29* 16.27/4.39 active1(30) -> 10,29* 16.27/4.39 active1(5) -> 29*,10,13 16.27/4.39 active1(32) -> 10,29* 16.27/4.39 active1(7) -> 29*,10,13 16.27/4.39 active1(2) -> 29*,10,13 16.27/4.39 active1(34) -> 10,29* 16.27/4.39 active1(9) -> 29*,10,13 16.27/4.39 active1(4) -> 29*,10,13 16.27/4.39 active1(36) -> 10,29* 16.27/4.39 active1(31) -> 10,29* 16.27/4.39 active1(6) -> 29*,10,13 16.27/4.39 active1(1) -> 29*,10,13 16.27/4.39 active1(33) -> 10,29* 16.27/4.39 active1(8) -> 29*,10,13 16.27/4.39 active1(3) -> 29*,10,13 16.27/4.39 proper1(35) -> 13* 16.27/4.39 proper1(30) -> 13* 16.27/4.39 proper1(5) -> 13* 16.27/4.39 proper1(32) -> 13* 16.27/4.39 proper1(7) -> 13* 16.27/4.39 proper1(2) -> 13* 16.27/4.39 proper1(34) -> 13* 16.27/4.39 proper1(9) -> 13* 16.27/4.39 proper1(4) -> 13* 16.27/4.39 proper1(36) -> 13* 16.27/4.39 proper1(31) -> 13* 16.27/4.39 proper1(6) -> 13* 16.27/4.39 proper1(1) -> 13* 16.27/4.39 proper1(33) -> 13* 16.27/4.39 proper1(8) -> 13* 16.27/4.39 proper1(3) -> 13* 16.27/4.39 ok1(35) -> 9,30* 16.27/4.39 ok1(15) -> 15* 16.27/4.39 ok1(32) -> 9,30* 16.27/4.39 ok1(17) -> 17* 16.27/4.39 ok1(12) -> 12* 16.27/4.39 ok1(2) -> 30*,9,13 16.27/4.39 ok1(34) -> 9,30* 16.27/4.39 ok1(14) -> 14* 16.27/4.39 ok1(36) -> 9,30* 16.27/4.39 ok1(31) -> 9,30* 16.27/4.39 ok1(16) -> 16* 16.27/4.39 ok1(11) -> 11* 16.27/4.39 ok1(33) -> 9,30* 16.27/4.39 ok1(18) -> 18* 16.27/4.39 isPal1(35) -> 18* 16.27/4.39 isPal1(30) -> 18* 16.27/4.39 isPal1(5) -> 18* 16.27/4.39 isPal1(32) -> 18* 16.27/4.39 isPal1(7) -> 18* 16.27/4.39 isPal1(2) -> 18* 16.27/4.39 isPal1(34) -> 18* 16.27/4.39 isPal1(9) -> 18* 16.27/4.39 isPal1(4) -> 18* 16.27/4.39 isPal1(36) -> 18* 16.27/4.39 isPal1(31) -> 18* 16.27/4.39 isPal1(6) -> 18* 16.27/4.39 isPal1(1) -> 18* 16.27/4.39 isPal1(33) -> 18* 16.27/4.39 isPal1(8) -> 18* 16.27/4.39 isPal1(3) -> 18* 16.27/4.39 isNePal1(35) -> 17* 16.27/4.39 isNePal1(30) -> 17* 16.27/4.39 isNePal1(5) -> 17* 16.27/4.39 isNePal1(32) -> 17* 16.27/4.39 isNePal1(7) -> 17* 16.27/4.39 isNePal1(2) -> 17* 16.27/4.39 isNePal1(34) -> 17* 16.27/4.39 isNePal1(9) -> 17* 16.27/4.39 isNePal1(4) -> 17* 16.27/4.39 isNePal1(36) -> 17* 16.27/4.39 isNePal1(31) -> 17* 16.27/4.39 isNePal1(6) -> 17* 16.27/4.39 isNePal1(1) -> 17* 16.27/4.39 isNePal1(33) -> 17* 16.27/4.39 isNePal1(8) -> 17* 16.27/4.39 isNePal1(3) -> 17* 16.27/4.39 isQid1(35) -> 16* 16.27/4.39 isQid1(30) -> 16* 16.27/4.39 isQid1(5) -> 16* 16.27/4.39 isQid1(32) -> 16* 16.27/4.39 isQid1(7) -> 16* 16.27/4.39 isQid1(2) -> 16* 16.27/4.39 isQid1(34) -> 16* 16.27/4.39 isQid1(9) -> 16* 16.27/4.39 isQid1(4) -> 16* 16.27/4.39 isQid1(36) -> 16* 16.27/4.39 isQid1(31) -> 16* 16.27/4.39 isQid1(6) -> 16* 16.27/4.39 isQid1(1) -> 16* 16.27/4.39 isQid1(33) -> 16* 16.27/4.39 isQid1(8) -> 16* 16.27/4.39 isQid1(3) -> 16* 16.27/4.39 isNeList1(35) -> 15* 16.27/4.39 isNeList1(30) -> 15* 16.27/4.39 isNeList1(5) -> 15* 16.27/4.39 isNeList1(32) -> 15* 16.27/4.39 isNeList1(7) -> 15* 16.27/4.39 isNeList1(2) -> 15* 16.27/4.39 isNeList1(34) -> 15* 16.27/4.39 isNeList1(9) -> 15* 16.27/4.39 isNeList1(4) -> 15* 16.27/4.39 isNeList1(36) -> 15* 16.27/4.39 isNeList1(31) -> 15* 16.27/4.39 isNeList1(6) -> 15* 16.27/4.39 isNeList1(1) -> 15* 16.27/4.39 isNeList1(33) -> 15* 16.27/4.39 isNeList1(8) -> 15* 16.27/4.39 isNeList1(3) -> 15* 16.27/4.39 isList1(35) -> 14* 16.27/4.39 isList1(30) -> 14* 16.27/4.39 isList1(5) -> 14* 16.27/4.39 isList1(32) -> 14* 16.27/4.39 isList1(7) -> 14* 16.27/4.39 isList1(2) -> 14* 16.27/4.39 isList1(34) -> 14* 16.27/4.39 isList1(9) -> 14* 16.27/4.39 isList1(4) -> 14* 16.27/4.39 isList1(36) -> 14* 16.27/4.39 isList1(31) -> 14* 16.27/4.39 isList1(6) -> 14* 16.27/4.39 isList1(1) -> 14* 16.27/4.39 isList1(33) -> 14* 16.27/4.39 isList1(8) -> 14* 16.27/4.39 isList1(3) -> 14* 16.27/4.39 and1(2,4) -> 12* 16.27/4.39 and1(36,31) -> 12* 16.27/4.39 and1(7,6) -> 12* 16.27/4.39 and1(31,31) -> 12* 16.27/4.39 and1(2,6) -> 12* 16.27/4.39 and1(36,33) -> 12* 16.27/4.39 and1(7,8) -> 12* 16.27/4.39 and1(31,33) -> 12* 16.27/4.39 and1(2,8) -> 12* 16.27/4.39 and1(36,35) -> 12* 16.27/4.39 and1(31,35) -> 12* 16.27/4.39 and1(6,31) -> 12* 16.27/4.39 and1(1,31) -> 12* 16.27/4.39 and1(6,33) -> 12* 16.27/4.39 and1(1,33) -> 12* 16.27/4.39 and1(6,35) -> 12* 16.27/4.39 and1(33,1) -> 12* 16.27/4.39 and1(1,35) -> 12* 16.27/4.39 and1(33,3) -> 12* 16.27/4.39 and1(33,5) -> 12* 16.27/4.39 and1(8,1) -> 12* 16.27/4.39 and1(3,1) -> 12* 16.27/4.39 and1(33,7) -> 12* 16.27/4.39 and1(8,3) -> 12* 16.27/4.39 and1(3,3) -> 12* 16.27/4.39 and1(33,9) -> 12* 16.27/4.39 and1(8,5) -> 12* 16.27/4.39 and1(32,30) -> 12* 16.27/4.39 and1(3,5) -> 12* 16.27/4.39 and1(8,7) -> 12* 16.27/4.39 and1(32,32) -> 12* 16.27/4.39 and1(3,7) -> 12* 16.27/4.39 and1(8,9) -> 12* 16.27/4.39 and1(32,34) -> 12* 16.27/4.39 and1(3,9) -> 12* 16.27/4.39 and1(7,30) -> 12* 16.27/4.39 and1(32,36) -> 12* 16.27/4.39 and1(2,30) -> 12* 16.27/4.39 and1(7,32) -> 12* 16.27/4.39 and1(2,32) -> 12* 16.27/4.39 and1(7,34) -> 12* 16.27/4.39 and1(2,34) -> 12* 16.27/4.39 and1(7,36) -> 12* 16.27/4.39 and1(34,2) -> 12* 16.27/4.39 and1(2,36) -> 12* 16.27/4.39 and1(34,4) -> 12* 16.27/4.39 and1(34,6) -> 12* 16.27/4.39 and1(9,2) -> 12* 16.27/4.39 and1(4,2) -> 12* 16.27/4.39 and1(34,8) -> 12* 16.27/4.39 and1(9,4) -> 12* 16.27/4.39 and1(4,4) -> 12* 16.27/4.39 and1(9,6) -> 12* 16.27/4.39 and1(33,31) -> 12* 16.27/4.39 and1(4,6) -> 12* 16.27/4.39 and1(9,8) -> 12* 16.27/4.39 and1(33,33) -> 12* 16.27/4.39 and1(4,8) -> 12* 16.27/4.39 and1(33,35) -> 12* 16.27/4.39 and1(8,31) -> 12* 16.27/4.39 and1(3,31) -> 12* 16.27/4.39 and1(8,33) -> 12* 16.27/4.39 and1(3,33) -> 12* 16.27/4.39 and1(8,35) -> 12* 16.27/4.39 and1(35,1) -> 12* 16.27/4.39 and1(3,35) -> 12* 16.27/4.39 and1(30,1) -> 12* 16.27/4.39 and1(35,3) -> 12* 16.27/4.39 and1(30,3) -> 12* 16.27/4.39 and1(35,5) -> 12* 16.27/4.39 and1(30,5) -> 12* 16.27/4.39 and1(5,1) -> 12* 16.27/4.39 and1(35,7) -> 12* 16.27/4.39 and1(30,7) -> 12* 16.27/4.39 and1(5,3) -> 12* 16.27/4.39 and1(35,9) -> 12* 16.27/4.39 and1(30,9) -> 12* 16.27/4.39 and1(34,30) -> 12* 16.27/4.39 and1(5,5) -> 12* 16.27/4.39 and1(34,32) -> 12* 16.27/4.39 and1(5,7) -> 12* 16.27/4.39 and1(34,34) -> 12* 16.27/4.39 and1(5,9) -> 12* 16.27/4.39 and1(9,30) -> 12* 16.27/4.39 and1(34,36) -> 12* 16.27/4.39 and1(4,30) -> 12* 16.27/4.39 and1(9,32) -> 12* 16.27/4.39 and1(4,32) -> 12* 16.27/4.39 and1(9,34) -> 12* 16.27/4.39 and1(4,34) -> 12* 16.27/4.39 and1(9,36) -> 12* 16.27/4.39 and1(36,2) -> 12* 16.27/4.39 and1(4,36) -> 12* 16.27/4.39 and1(31,2) -> 12* 16.27/4.39 and1(36,4) -> 12* 16.27/4.39 and1(31,4) -> 12* 16.27/4.39 and1(36,6) -> 12* 16.27/4.39 and1(31,6) -> 12* 16.27/4.39 and1(6,2) -> 12* 16.27/4.39 and1(36,8) -> 12* 16.27/4.39 and1(1,2) -> 12* 16.27/4.39 and1(31,8) -> 12* 16.27/4.39 and1(6,4) -> 12* 16.27/4.39 and1(1,4) -> 12* 16.27/4.39 and1(35,31) -> 12* 16.27/4.39 and1(6,6) -> 12* 16.27/4.39 and1(30,31) -> 12* 16.27/4.39 and1(1,6) -> 12* 16.27/4.39 and1(35,33) -> 12* 16.27/4.39 and1(6,8) -> 12* 16.27/4.39 and1(30,33) -> 12* 16.27/4.39 and1(1,8) -> 12* 16.27/4.39 and1(35,35) -> 12* 16.27/4.39 and1(30,35) -> 12* 16.27/4.39 and1(5,31) -> 12* 16.27/4.39 and1(5,33) -> 12* 16.27/4.39 and1(5,35) -> 12* 16.27/4.39 and1(32,1) -> 12* 16.27/4.39 and1(32,3) -> 12* 16.27/4.39 and1(32,5) -> 12* 16.27/4.39 and1(7,1) -> 12* 16.27/4.39 and1(2,1) -> 12* 16.27/4.39 and1(32,7) -> 12* 16.27/4.39 and1(7,3) -> 12* 16.27/4.39 and1(2,3) -> 12* 16.27/4.39 and1(32,9) -> 12* 16.27/4.39 and1(36,30) -> 12* 16.27/4.39 and1(7,5) -> 12* 16.27/4.39 and1(31,30) -> 12* 16.27/4.39 and1(2,5) -> 12* 16.27/4.39 and1(36,32) -> 12* 16.27/4.39 and1(7,7) -> 12* 16.27/4.39 and1(31,32) -> 12* 16.27/4.39 and1(2,7) -> 12* 16.27/4.39 and1(36,34) -> 12* 16.27/4.39 and1(7,9) -> 12* 16.27/4.39 and1(31,34) -> 12* 16.27/4.39 and1(2,9) -> 12* 16.27/4.39 and1(36,36) -> 12* 16.27/4.39 and1(6,30) -> 12* 16.27/4.39 and1(31,36) -> 12* 16.27/4.39 and1(1,30) -> 12* 16.27/4.39 and1(6,32) -> 12* 16.27/4.39 and1(1,32) -> 12* 16.27/4.39 and1(6,34) -> 12* 16.27/4.39 and1(1,34) -> 12* 16.27/4.39 and1(6,36) -> 12* 16.27/4.39 and1(33,2) -> 12* 16.27/4.39 and1(1,36) -> 12* 16.27/4.39 and1(33,4) -> 12* 16.27/4.39 and1(33,6) -> 12* 16.27/4.39 and1(8,2) -> 12* 16.27/4.39 and1(3,2) -> 12* 16.27/4.39 and1(33,8) -> 12* 16.27/4.39 and1(8,4) -> 12* 16.27/4.39 and1(3,4) -> 12* 16.27/4.39 and1(8,6) -> 12* 16.27/4.39 and1(32,31) -> 12* 16.27/4.39 and1(3,6) -> 12* 16.27/4.39 and1(8,8) -> 12* 16.27/4.39 and1(32,33) -> 12* 16.27/4.39 and1(3,8) -> 12* 16.27/4.39 and1(32,35) -> 12* 16.27/4.39 and1(7,31) -> 12* 16.27/4.39 and1(2,31) -> 12* 16.27/4.39 and1(7,33) -> 12* 16.27/4.39 and1(2,33) -> 12* 16.27/4.39 and1(7,35) -> 12* 16.27/4.39 and1(34,1) -> 12* 16.27/4.39 and1(2,35) -> 12* 16.27/4.39 and1(34,3) -> 12* 16.27/4.39 and1(34,5) -> 12* 16.27/4.39 and1(9,1) -> 12* 16.27/4.39 and1(4,1) -> 12* 16.27/4.39 and1(34,7) -> 12* 16.27/4.39 and1(9,3) -> 12* 16.27/4.39 and1(4,3) -> 12* 16.27/4.39 and1(34,9) -> 12* 16.27/4.39 and1(9,5) -> 12* 16.27/4.39 and1(33,30) -> 12* 16.27/4.39 and1(4,5) -> 12* 16.27/4.39 and1(9,7) -> 12* 16.27/4.39 and1(33,32) -> 12* 16.27/4.39 and1(4,7) -> 12* 16.27/4.39 and1(9,9) -> 12* 16.27/4.39 and1(33,34) -> 12* 16.27/4.39 and1(4,9) -> 12* 16.27/4.39 and1(8,30) -> 12* 16.27/4.39 and1(33,36) -> 12* 16.27/4.39 and1(3,30) -> 12* 16.27/4.39 and1(8,32) -> 12* 16.27/4.39 and1(3,32) -> 12* 16.27/4.39 and1(8,34) -> 12* 16.27/4.39 and1(3,34) -> 12* 16.27/4.39 and1(8,36) -> 12* 16.27/4.39 and1(35,2) -> 12* 16.27/4.39 and1(3,36) -> 12* 16.27/4.39 and1(30,2) -> 12* 16.27/4.39 and1(35,4) -> 12* 16.27/4.39 and1(30,4) -> 12* 16.27/4.39 and1(35,6) -> 12* 16.27/4.39 and1(30,6) -> 12* 16.27/4.39 and1(5,2) -> 12* 16.27/4.39 and1(35,8) -> 12* 16.27/4.39 and1(30,8) -> 12* 16.27/4.39 and1(5,4) -> 12* 16.27/4.39 and1(34,31) -> 12* 16.27/4.39 and1(5,6) -> 12* 16.27/4.39 and1(34,33) -> 12* 16.27/4.39 and1(5,8) -> 12* 16.27/4.39 and1(34,35) -> 12* 16.27/4.39 and1(9,31) -> 12* 16.27/4.39 and1(4,31) -> 12* 16.27/4.39 and1(9,33) -> 12* 16.27/4.39 and1(4,33) -> 12* 16.27/4.39 and1(9,35) -> 12* 16.27/4.39 and1(36,1) -> 12* 16.27/4.39 and1(4,35) -> 12* 16.27/4.39 and1(31,1) -> 12* 16.27/4.39 and1(36,3) -> 12* 16.27/4.39 and1(31,3) -> 12* 16.27/4.39 and1(36,5) -> 12* 16.27/4.39 and1(31,5) -> 12* 16.27/4.39 and1(6,1) -> 12* 16.27/4.39 and1(36,7) -> 12* 16.27/4.39 and1(1,1) -> 12* 16.27/4.39 and1(31,7) -> 12* 16.27/4.39 and1(6,3) -> 12* 16.27/4.39 and1(36,9) -> 12* 16.27/4.39 and1(1,3) -> 12* 16.27/4.39 and1(31,9) -> 12* 16.27/4.39 and1(35,30) -> 12* 16.27/4.39 and1(6,5) -> 12* 16.27/4.39 and1(30,30) -> 12* 16.27/4.39 and1(1,5) -> 12* 16.27/4.39 and1(35,32) -> 12* 16.27/4.39 and1(6,7) -> 12* 16.27/4.39 and1(30,32) -> 12* 16.27/4.40 and1(1,7) -> 12* 16.27/4.40 and1(35,34) -> 12* 16.27/4.40 and1(6,9) -> 12* 16.27/4.40 and1(30,34) -> 12* 16.27/4.40 and1(1,9) -> 12* 16.27/4.40 and1(35,36) -> 12* 16.27/4.40 and1(5,30) -> 12* 16.27/4.40 and1(30,36) -> 12* 16.27/4.40 and1(5,32) -> 12* 16.27/4.40 and1(5,34) -> 12* 16.27/4.40 and1(5,36) -> 12* 16.27/4.40 and1(32,2) -> 12* 16.27/4.40 and1(32,4) -> 12* 16.27/4.40 and1(32,6) -> 12* 16.27/4.40 and1(7,2) -> 12* 16.27/4.40 and1(2,2) -> 12* 16.27/4.40 and1(32,8) -> 12* 16.27/4.40 and1(7,4) -> 12* 16.27/4.40 __1(2,4) -> 11* 16.27/4.40 __1(36,31) -> 11* 16.27/4.40 __1(7,6) -> 11* 16.27/4.40 __1(31,31) -> 11* 16.27/4.40 __1(2,6) -> 11* 16.27/4.40 __1(36,33) -> 11* 16.27/4.40 __1(7,8) -> 11* 16.27/4.40 __1(31,33) -> 11* 16.27/4.40 __1(2,8) -> 11* 16.27/4.40 __1(36,35) -> 11* 16.27/4.40 __1(31,35) -> 11* 16.27/4.40 __1(6,31) -> 11* 16.27/4.40 __1(1,31) -> 11* 16.27/4.40 __1(6,33) -> 11* 16.27/4.40 __1(1,33) -> 11* 16.27/4.40 __1(6,35) -> 11* 16.27/4.40 __1(33,1) -> 11* 16.27/4.40 __1(1,35) -> 11* 16.27/4.40 __1(33,3) -> 11* 16.27/4.40 __1(33,5) -> 11* 16.27/4.40 __1(8,1) -> 11* 16.27/4.40 __1(3,1) -> 11* 16.27/4.40 __1(33,7) -> 11* 16.27/4.40 __1(8,3) -> 11* 16.27/4.40 __1(3,3) -> 11* 16.27/4.40 __1(33,9) -> 11* 16.27/4.40 __1(8,5) -> 11* 16.27/4.40 __1(32,30) -> 11* 16.27/4.40 __1(3,5) -> 11* 16.27/4.40 __1(8,7) -> 11* 16.27/4.40 __1(32,32) -> 11* 16.27/4.40 __1(3,7) -> 11* 16.27/4.40 __1(8,9) -> 11* 16.27/4.40 __1(32,34) -> 11* 16.27/4.40 __1(3,9) -> 11* 16.27/4.40 __1(7,30) -> 11* 16.27/4.40 __1(32,36) -> 11* 16.27/4.40 __1(2,30) -> 11* 16.27/4.40 __1(7,32) -> 11* 16.27/4.40 __1(2,32) -> 11* 16.27/4.40 __1(7,34) -> 11* 16.27/4.40 __1(2,34) -> 11* 16.27/4.40 __1(7,36) -> 11* 16.27/4.40 __1(34,2) -> 11* 16.27/4.40 __1(2,36) -> 11* 16.27/4.40 __1(34,4) -> 11* 16.27/4.40 __1(34,6) -> 11* 16.27/4.40 __1(9,2) -> 11* 16.27/4.40 __1(4,2) -> 11* 16.27/4.40 __1(34,8) -> 11* 16.27/4.40 __1(9,4) -> 11* 16.27/4.40 __1(4,4) -> 11* 16.27/4.40 __1(9,6) -> 11* 16.27/4.40 __1(33,31) -> 11* 16.27/4.40 __1(4,6) -> 11* 16.27/4.40 __1(9,8) -> 11* 16.27/4.40 __1(33,33) -> 11* 16.27/4.40 __1(4,8) -> 11* 16.27/4.40 __1(33,35) -> 11* 16.27/4.40 __1(8,31) -> 11* 16.27/4.40 __1(3,31) -> 11* 16.27/4.40 __1(8,33) -> 11* 16.27/4.40 __1(3,33) -> 11* 16.27/4.40 __1(8,35) -> 11* 16.27/4.40 __1(35,1) -> 11* 16.27/4.40 __1(3,35) -> 11* 16.27/4.40 __1(30,1) -> 11* 16.27/4.40 __1(35,3) -> 11* 16.27/4.40 __1(30,3) -> 11* 16.27/4.40 __1(35,5) -> 11* 16.27/4.40 __1(30,5) -> 11* 16.27/4.40 __1(5,1) -> 11* 16.27/4.40 __1(35,7) -> 11* 16.27/4.40 __1(30,7) -> 11* 16.27/4.40 __1(5,3) -> 11* 16.27/4.40 __1(35,9) -> 11* 16.27/4.40 __1(30,9) -> 11* 16.27/4.40 __1(34,30) -> 11* 16.27/4.40 __1(5,5) -> 11* 16.27/4.40 __1(34,32) -> 11* 16.27/4.40 __1(5,7) -> 11* 16.27/4.40 __1(34,34) -> 11* 16.27/4.40 __1(5,9) -> 11* 16.27/4.40 __1(9,30) -> 11* 16.27/4.40 __1(34,36) -> 11* 16.27/4.40 __1(4,30) -> 11* 16.27/4.40 __1(9,32) -> 11* 16.27/4.40 __1(4,32) -> 11* 16.27/4.40 __1(9,34) -> 11* 16.27/4.40 __1(4,34) -> 11* 16.27/4.40 __1(9,36) -> 11* 16.27/4.40 __1(36,2) -> 11* 16.27/4.40 __1(4,36) -> 11* 16.27/4.40 __1(31,2) -> 11* 16.27/4.40 __1(36,4) -> 11* 16.27/4.40 __1(31,4) -> 11* 16.27/4.40 __1(36,6) -> 11* 16.27/4.40 __1(31,6) -> 11* 16.27/4.40 __1(6,2) -> 11* 16.27/4.40 __1(36,8) -> 11* 16.27/4.40 __1(1,2) -> 11* 16.27/4.40 __1(31,8) -> 11* 16.27/4.40 __1(6,4) -> 11* 16.27/4.40 __1(1,4) -> 11* 16.27/4.40 __1(35,31) -> 11* 16.27/4.40 __1(6,6) -> 11* 16.27/4.40 __1(30,31) -> 11* 16.27/4.40 __1(1,6) -> 11* 16.27/4.40 __1(35,33) -> 11* 16.27/4.40 __1(6,8) -> 11* 16.27/4.40 __1(30,33) -> 11* 16.27/4.40 __1(1,8) -> 11* 16.27/4.40 __1(35,35) -> 11* 16.27/4.40 __1(30,35) -> 11* 16.27/4.40 __1(5,31) -> 11* 16.27/4.40 __1(5,33) -> 11* 16.27/4.40 __1(5,35) -> 11* 16.27/4.40 __1(32,1) -> 11* 16.27/4.40 __1(32,3) -> 11* 16.27/4.40 __1(32,5) -> 11* 16.27/4.40 __1(7,1) -> 11* 16.27/4.40 __1(2,1) -> 11* 16.27/4.40 __1(32,7) -> 11* 16.27/4.40 __1(7,3) -> 11* 16.27/4.40 __1(2,3) -> 11* 16.27/4.40 __1(32,9) -> 11* 16.27/4.40 __1(36,30) -> 11* 16.27/4.40 __1(7,5) -> 11* 16.27/4.40 __1(31,30) -> 11* 16.27/4.40 __1(2,5) -> 11* 16.27/4.40 __1(36,32) -> 11* 16.27/4.40 __1(7,7) -> 11* 16.27/4.40 __1(31,32) -> 11* 16.27/4.40 __1(2,7) -> 11* 16.27/4.40 __1(36,34) -> 11* 16.27/4.40 __1(7,9) -> 11* 16.27/4.40 __1(31,34) -> 11* 16.27/4.40 __1(2,9) -> 11* 16.27/4.40 __1(36,36) -> 11* 16.27/4.40 __1(6,30) -> 11* 16.27/4.40 __1(31,36) -> 11* 16.27/4.40 __1(1,30) -> 11* 16.27/4.40 __1(6,32) -> 11* 16.27/4.40 __1(1,32) -> 11* 16.27/4.40 __1(6,34) -> 11* 16.27/4.40 __1(1,34) -> 11* 16.27/4.40 __1(6,36) -> 11* 16.27/4.40 __1(33,2) -> 11* 16.27/4.40 __1(1,36) -> 11* 16.27/4.40 __1(33,4) -> 11* 16.27/4.40 __1(33,6) -> 11* 16.27/4.40 __1(8,2) -> 11* 16.27/4.40 __1(3,2) -> 11* 16.27/4.40 __1(33,8) -> 11* 16.27/4.40 __1(8,4) -> 11* 16.27/4.40 __1(3,4) -> 11* 16.27/4.40 __1(8,6) -> 11* 16.27/4.40 __1(32,31) -> 11* 16.27/4.40 __1(3,6) -> 11* 16.27/4.40 __1(8,8) -> 11* 16.27/4.40 __1(32,33) -> 11* 16.27/4.40 __1(3,8) -> 11* 16.27/4.40 __1(32,35) -> 11* 16.27/4.40 __1(7,31) -> 11* 16.27/4.40 __1(2,31) -> 11* 16.27/4.40 __1(7,33) -> 11* 16.27/4.40 __1(2,33) -> 11* 16.27/4.40 __1(7,35) -> 11* 16.27/4.40 __1(34,1) -> 11* 16.27/4.40 __1(2,35) -> 11* 16.27/4.40 __1(34,3) -> 11* 16.27/4.40 __1(34,5) -> 11* 16.27/4.40 __1(9,1) -> 11* 16.27/4.40 __1(4,1) -> 11* 16.27/4.40 __1(34,7) -> 11* 16.27/4.40 __1(9,3) -> 11* 16.27/4.40 __1(4,3) -> 11* 16.27/4.40 __1(34,9) -> 11* 16.27/4.40 __1(9,5) -> 11* 16.27/4.40 __1(33,30) -> 11* 16.27/4.40 __1(4,5) -> 11* 16.27/4.40 __1(9,7) -> 11* 16.27/4.40 __1(33,32) -> 11* 16.27/4.40 __1(4,7) -> 11* 16.27/4.40 __1(9,9) -> 11* 16.27/4.40 __1(33,34) -> 11* 16.27/4.40 __1(4,9) -> 11* 16.27/4.40 __1(8,30) -> 11* 16.27/4.40 __1(33,36) -> 11* 16.27/4.40 __1(3,30) -> 11* 16.27/4.40 __1(8,32) -> 11* 16.27/4.40 __1(3,32) -> 11* 16.27/4.40 __1(8,34) -> 11* 16.27/4.40 __1(3,34) -> 11* 16.27/4.40 __1(8,36) -> 11* 16.27/4.40 __1(35,2) -> 11* 16.27/4.40 __1(3,36) -> 11* 16.27/4.40 __1(30,2) -> 11* 16.27/4.40 __1(35,4) -> 11* 16.27/4.40 __1(30,4) -> 11* 16.27/4.40 __1(35,6) -> 11* 16.27/4.40 __1(30,6) -> 11* 16.27/4.40 __1(5,2) -> 11* 16.27/4.40 __1(35,8) -> 11* 16.27/4.40 __1(30,8) -> 11* 16.27/4.40 __1(5,4) -> 11* 16.27/4.40 __1(34,31) -> 11* 16.27/4.40 __1(5,6) -> 11* 16.27/4.40 __1(34,33) -> 11* 16.27/4.40 __1(5,8) -> 11* 16.27/4.40 __1(34,35) -> 11* 16.27/4.40 __1(9,31) -> 11* 16.27/4.40 __1(4,31) -> 11* 16.27/4.40 __1(9,33) -> 11* 16.27/4.40 __1(4,33) -> 11* 16.27/4.40 __1(9,35) -> 11* 16.27/4.40 __1(36,1) -> 11* 16.27/4.40 __1(4,35) -> 11* 16.27/4.40 __1(31,1) -> 11* 16.27/4.40 __1(36,3) -> 11* 16.27/4.40 __1(31,3) -> 11* 16.27/4.40 __1(36,5) -> 11* 16.27/4.40 __1(31,5) -> 11* 16.27/4.40 __1(6,1) -> 11* 16.27/4.40 __1(36,7) -> 11* 16.27/4.40 __1(1,1) -> 11* 16.27/4.40 __1(31,7) -> 11* 16.27/4.40 __1(6,3) -> 11* 16.27/4.40 __1(36,9) -> 11* 16.27/4.40 __1(1,3) -> 11* 16.27/4.40 __1(31,9) -> 11* 16.27/4.40 __1(35,30) -> 11* 16.27/4.40 __1(6,5) -> 11* 16.27/4.40 __1(30,30) -> 11* 16.27/4.40 __1(1,5) -> 11* 16.27/4.40 __1(35,32) -> 11* 16.27/4.40 __1(6,7) -> 11* 16.27/4.40 __1(30,32) -> 11* 16.27/4.40 __1(1,7) -> 11* 16.27/4.40 __1(35,34) -> 11* 16.27/4.40 __1(6,9) -> 11* 16.27/4.40 __1(30,34) -> 11* 16.27/4.40 __1(1,9) -> 11* 16.27/4.40 __1(35,36) -> 11* 16.27/4.40 __1(5,30) -> 11* 16.27/4.40 __1(30,36) -> 11* 16.27/4.40 __1(5,32) -> 11* 16.27/4.40 __1(5,34) -> 11* 16.27/4.40 __1(5,36) -> 11* 16.27/4.40 __1(32,2) -> 11* 16.27/4.40 __1(32,4) -> 11* 16.27/4.40 __1(32,6) -> 11* 16.27/4.40 __1(7,2) -> 11* 16.27/4.40 __1(2,2) -> 11* 16.27/4.40 __1(32,8) -> 11* 16.27/4.40 __1(7,4) -> 11* 16.27/4.40 u1() -> 31*,8,2 16.27/4.40 o1() -> 32*,7,2 16.27/4.40 i1() -> 33*,6,2 16.27/4.40 e1() -> 34*,5,2 16.27/4.40 a1() -> 35*,4,2 16.27/4.40 tt1() -> 36*,3,2 16.27/4.40 nil1() -> 2* 16.27/4.40 mark1(12) -> 12* 16.27/4.40 mark1(11) -> 11* 16.27/4.40 top2(10) -> 19* 16.27/4.40 top2(29) -> 19* 16.27/4.40 active2(35) -> 29*,10 16.27/4.40 active2(32) -> 29*,10 16.27/4.40 active2(2) -> 13,29*,10 16.27/4.40 active2(34) -> 29*,10 16.27/4.40 active2(36) -> 29*,10 16.27/4.40 active2(31) -> 29*,10 16.27/4.40 active2(33) -> 29*,10 16.27/4.40 ok2(35) -> 9,30* 16.27/4.40 ok2(15) -> 15* 16.27/4.40 ok2(32) -> 9,30* 16.27/4.40 ok2(17) -> 17* 16.27/4.40 ok2(12) -> 12* 16.27/4.40 ok2(2) -> 9,30*,13 16.27/4.40 ok2(34) -> 9,30* 16.27/4.40 ok2(14) -> 14* 16.27/4.40 ok2(36) -> 9,30* 16.27/4.40 ok2(31) -> 9,30* 16.27/4.40 ok2(16) -> 16* 16.27/4.40 ok2(11) -> 11* 16.27/4.40 ok2(33) -> 9,30* 16.27/4.40 ok2(18) -> 18* 16.27/4.40 isPal2(35) -> 18* 16.27/4.40 isPal2(32) -> 18* 16.27/4.40 isPal2(2) -> 18* 16.27/4.40 isPal2(34) -> 18* 16.27/4.40 isPal2(36) -> 18* 16.27/4.40 isPal2(31) -> 18* 16.27/4.40 isPal2(33) -> 18* 16.27/4.40 isNePal2(35) -> 17* 16.27/4.40 isNePal2(32) -> 17* 16.27/4.40 isNePal2(2) -> 17* 16.27/4.40 isNePal2(34) -> 17* 16.27/4.40 isNePal2(36) -> 17* 16.27/4.40 isNePal2(31) -> 17* 16.27/4.40 isNePal2(33) -> 17* 16.27/4.40 isQid2(35) -> 16* 16.27/4.40 isQid2(32) -> 16* 16.27/4.40 isQid2(2) -> 16* 16.27/4.40 isQid2(34) -> 16* 16.27/4.40 isQid2(36) -> 16* 16.27/4.40 isQid2(31) -> 16* 16.27/4.40 isQid2(33) -> 16* 16.27/4.40 isNeList2(35) -> 15* 16.27/4.40 isNeList2(32) -> 15* 16.27/4.40 isNeList2(2) -> 15* 16.27/4.40 isNeList2(34) -> 15* 16.27/4.40 isNeList2(36) -> 15* 16.27/4.40 isNeList2(31) -> 15* 16.27/4.40 isNeList2(33) -> 15* 16.27/4.40 isList2(35) -> 14* 16.27/4.40 isList2(32) -> 14* 16.27/4.40 isList2(2) -> 14* 16.27/4.40 isList2(34) -> 14* 16.27/4.40 isList2(36) -> 14* 16.27/4.40 isList2(31) -> 14* 16.27/4.40 isList2(33) -> 14* 16.27/4.40 and2(2,2) -> 12* 16.27/4.40 and2(36,31) -> 12* 16.27/4.40 and2(31,31) -> 12* 16.27/4.40 and2(36,33) -> 12* 16.27/4.40 and2(31,33) -> 12* 16.27/4.40 and2(36,35) -> 12* 16.27/4.40 and2(31,35) -> 12* 16.27/4.40 and2(32,32) -> 12* 16.27/4.40 and2(32,34) -> 12* 16.27/4.40 and2(32,36) -> 12* 16.27/4.40 and2(2,32) -> 12* 16.27/4.40 and2(2,34) -> 12* 16.27/4.40 and2(34,2) -> 12* 16.27/4.40 and2(2,36) -> 12* 16.27/4.40 and2(33,31) -> 12* 16.27/4.40 and2(33,33) -> 12* 16.27/4.40 and2(33,35) -> 12* 16.27/4.40 and2(34,32) -> 12* 16.27/4.40 and2(34,34) -> 12* 16.27/4.40 and2(34,36) -> 12* 16.27/4.40 and2(36,2) -> 12* 16.27/4.40 and2(31,2) -> 12* 16.27/4.40 and2(35,31) -> 12* 16.27/4.40 and2(35,33) -> 12* 16.27/4.40 and2(35,35) -> 12* 16.27/4.40 and2(36,32) -> 12* 16.27/4.40 and2(31,32) -> 12* 16.27/4.40 and2(36,34) -> 12* 16.27/4.40 and2(31,34) -> 12* 16.27/4.40 and2(36,36) -> 12* 16.27/4.40 and2(31,36) -> 12* 16.27/4.40 and2(33,2) -> 12* 16.27/4.40 and2(32,31) -> 12* 16.27/4.40 and2(32,33) -> 12* 16.27/4.40 and2(32,35) -> 12* 16.27/4.40 and2(2,31) -> 12* 16.27/4.40 and2(2,33) -> 12* 16.27/4.40 and2(2,35) -> 12* 16.27/4.40 and2(33,32) -> 12* 16.27/4.40 and2(33,34) -> 12* 16.27/4.40 and2(33,36) -> 12* 16.27/4.40 and2(35,2) -> 12* 16.27/4.40 and2(34,31) -> 12* 16.27/4.40 and2(34,33) -> 12* 16.27/4.40 and2(34,35) -> 12* 16.27/4.40 and2(35,32) -> 12* 16.27/4.40 and2(35,34) -> 12* 16.27/4.40 and2(35,36) -> 12* 16.27/4.40 and2(32,2) -> 12* 16.27/4.40 __2(2,2) -> 11* 16.27/4.40 __2(36,31) -> 11* 16.27/4.40 __2(31,31) -> 11* 16.27/4.40 __2(36,33) -> 11* 16.27/4.40 __2(31,33) -> 11* 16.27/4.40 __2(36,35) -> 11* 16.27/4.40 __2(31,35) -> 11* 16.27/4.40 __2(32,32) -> 11* 16.27/4.40 __2(32,34) -> 11* 16.27/4.40 __2(32,36) -> 11* 16.27/4.40 __2(2,32) -> 11* 16.27/4.40 __2(2,34) -> 11* 16.27/4.40 __2(34,2) -> 11* 16.27/4.40 __2(2,36) -> 11* 16.27/4.40 __2(33,31) -> 11* 16.27/4.40 __2(33,33) -> 11* 16.27/4.40 __2(33,35) -> 11* 16.27/4.40 __2(34,32) -> 11* 16.27/4.40 __2(34,34) -> 11* 16.27/4.40 __2(34,36) -> 11* 16.27/4.40 __2(36,2) -> 11* 16.27/4.40 __2(31,2) -> 11* 16.27/4.40 __2(35,31) -> 11* 16.27/4.40 __2(35,33) -> 11* 16.27/4.40 __2(35,35) -> 11* 16.27/4.40 __2(36,32) -> 11* 16.27/4.40 __2(31,32) -> 11* 16.27/4.40 __2(36,34) -> 11* 16.27/4.40 __2(31,34) -> 11* 16.27/4.40 __2(36,36) -> 11* 16.27/4.40 __2(31,36) -> 11* 16.27/4.40 __2(33,2) -> 11* 16.27/4.40 __2(32,31) -> 11* 16.27/4.40 __2(32,33) -> 11* 16.27/4.40 __2(32,35) -> 11* 16.27/4.40 __2(2,31) -> 11* 16.27/4.40 __2(2,33) -> 11* 16.27/4.40 __2(2,35) -> 11* 16.27/4.40 __2(33,32) -> 11* 16.27/4.40 __2(33,34) -> 11* 16.27/4.40 __2(33,36) -> 11* 16.27/4.40 __2(35,2) -> 11* 16.27/4.40 __2(34,31) -> 11* 16.27/4.40 __2(34,33) -> 11* 16.27/4.40 __2(34,35) -> 11* 16.27/4.40 __2(35,32) -> 11* 16.27/4.40 __2(35,34) -> 11* 16.27/4.40 __2(35,36) -> 11* 16.27/4.40 __2(32,2) -> 11* 16.27/4.40 u2() -> 8,31*,2 16.27/4.40 o2() -> 7,32*,2 16.27/4.40 i2() -> 6,33*,2 16.27/4.40 e2() -> 5,34*,2 16.27/4.40 a2() -> 4,35*,2 16.27/4.40 tt2() -> 3,36*,2 16.27/4.40 nil2() -> 2* 16.27/4.40 problem: 16.27/4.40 16.27/4.40 Qed 16.47/4.41 EOF