Problem Transformed CSR 04 PALINDROME nokinds C

Tool CaT

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 PALINDROME nokinds C

stdout:

YES(?,O(n^1))

Problem:
 active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
 active(__(X,nil())) -> mark(X)
 active(__(nil(),X)) -> mark(X)
 active(and(tt(),X)) -> mark(X)
 active(isList(V)) -> mark(isNeList(V))
 active(isList(nil())) -> mark(tt())
 active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
 active(isNeList(V)) -> mark(isQid(V))
 active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
 active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
 active(isNePal(V)) -> mark(isQid(V))
 active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
 active(isPal(V)) -> mark(isNePal(V))
 active(isPal(nil())) -> mark(tt())
 active(isQid(a())) -> mark(tt())
 active(isQid(e())) -> mark(tt())
 active(isQid(i())) -> mark(tt())
 active(isQid(o())) -> mark(tt())
 active(isQid(u())) -> mark(tt())
 active(__(X1,X2)) -> __(active(X1),X2)
 active(__(X1,X2)) -> __(X1,active(X2))
 active(and(X1,X2)) -> and(active(X1),X2)
 __(mark(X1),X2) -> mark(__(X1,X2))
 __(X1,mark(X2)) -> mark(__(X1,X2))
 and(mark(X1),X2) -> mark(and(X1,X2))
 proper(__(X1,X2)) -> __(proper(X1),proper(X2))
 proper(nil()) -> ok(nil())
 proper(and(X1,X2)) -> and(proper(X1),proper(X2))
 proper(tt()) -> ok(tt())
 proper(isList(X)) -> isList(proper(X))
 proper(isNeList(X)) -> isNeList(proper(X))
 proper(isQid(X)) -> isQid(proper(X))
 proper(isNePal(X)) -> isNePal(proper(X))
 proper(isPal(X)) -> isPal(proper(X))
 proper(a()) -> ok(a())
 proper(e()) -> ok(e())
 proper(i()) -> ok(i())
 proper(o()) -> ok(o())
 proper(u()) -> ok(u())
 __(ok(X1),ok(X2)) -> ok(__(X1,X2))
 and(ok(X1),ok(X2)) -> ok(and(X1,X2))
 isList(ok(X)) -> ok(isList(X))
 isNeList(ok(X)) -> ok(isNeList(X))
 isQid(ok(X)) -> ok(isQid(X))
 isNePal(ok(X)) -> ok(isNePal(X))
 isPal(ok(X)) -> ok(isPal(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {30,29,19,18,17,16,15,14,13,12,11,10}
   transitions:
    active0(35) -> 10*
    active0(30) -> 10*
    active0(5) -> 10*
    active0(32) -> 10*
    active0(7) -> 10*
    active0(2) -> 10*
    active0(34) -> 10*
    active0(9) -> 10*
    active0(4) -> 10*
    active0(36) -> 10*
    active0(31) -> 10*
    active0(6) -> 10*
    active0(1) -> 10*
    active0(33) -> 10*
    active0(8) -> 10*
    active0(3) -> 10*
    __0(31,35) -> 11*
    __0(6,31) -> 11*
    __0(1,31) -> 11*
    __0(6,33) -> 11*
    __0(1,33) -> 11*
    __0(6,35) -> 11*
    __0(33,1) -> 11*
    __0(1,35) -> 11*
    __0(33,3) -> 11*
    __0(33,5) -> 11*
    __0(8,1) -> 11*
    __0(3,1) -> 11*
    __0(33,7) -> 11*
    __0(8,3) -> 11*
    __0(3,3) -> 11*
    __0(33,9) -> 11*
    __0(8,5) -> 11*
    __0(32,30) -> 11*
    __0(3,5) -> 11*
    __0(8,7) -> 11*
    __0(32,32) -> 11*
    __0(3,7) -> 11*
    __0(8,9) -> 11*
    __0(32,34) -> 11*
    __0(3,9) -> 11*
    __0(7,30) -> 11*
    __0(32,36) -> 11*
    __0(2,30) -> 11*
    __0(7,32) -> 11*
    __0(2,32) -> 11*
    __0(7,34) -> 11*
    __0(2,34) -> 11*
    __0(7,36) -> 11*
    __0(34,2) -> 11*
    __0(2,36) -> 11*
    __0(34,4) -> 11*
    __0(34,6) -> 11*
    __0(9,2) -> 11*
    __0(4,2) -> 11*
    __0(34,8) -> 11*
    __0(9,4) -> 11*
    __0(4,4) -> 11*
    __0(9,6) -> 11*
    __0(33,31) -> 11*
    __0(4,6) -> 11*
    __0(9,8) -> 11*
    __0(33,33) -> 11*
    __0(4,8) -> 11*
    __0(33,35) -> 11*
    __0(8,31) -> 11*
    __0(3,31) -> 11*
    __0(8,33) -> 11*
    __0(3,33) -> 11*
    __0(8,35) -> 11*
    __0(35,1) -> 11*
    __0(3,35) -> 11*
    __0(30,1) -> 11*
    __0(35,3) -> 11*
    __0(30,3) -> 11*
    __0(35,5) -> 11*
    __0(30,5) -> 11*
    __0(5,1) -> 11*
    __0(35,7) -> 11*
    __0(30,7) -> 11*
    __0(5,3) -> 11*
    __0(35,9) -> 11*
    __0(30,9) -> 11*
    __0(34,30) -> 11*
    __0(5,5) -> 11*
    __0(34,32) -> 11*
    __0(5,7) -> 11*
    __0(34,34) -> 11*
    __0(5,9) -> 11*
    __0(9,30) -> 11*
    __0(34,36) -> 11*
    __0(4,30) -> 11*
    __0(9,32) -> 11*
    __0(4,32) -> 11*
    __0(9,34) -> 11*
    __0(4,34) -> 11*
    __0(9,36) -> 11*
    __0(36,2) -> 11*
    __0(4,36) -> 11*
    __0(31,2) -> 11*
    __0(36,4) -> 11*
    __0(31,4) -> 11*
    __0(36,6) -> 11*
    __0(31,6) -> 11*
    __0(6,2) -> 11*
    __0(36,8) -> 11*
    __0(1,2) -> 11*
    __0(31,8) -> 11*
    __0(6,4) -> 11*
    __0(1,4) -> 11*
    __0(35,31) -> 11*
    __0(6,6) -> 11*
    __0(30,31) -> 11*
    __0(1,6) -> 11*
    __0(35,33) -> 11*
    __0(6,8) -> 11*
    __0(30,33) -> 11*
    __0(1,8) -> 11*
    __0(35,35) -> 11*
    __0(30,35) -> 11*
    __0(5,31) -> 11*
    __0(5,33) -> 11*
    __0(5,35) -> 11*
    __0(32,1) -> 11*
    __0(32,3) -> 11*
    __0(32,5) -> 11*
    __0(7,1) -> 11*
    __0(2,1) -> 11*
    __0(32,7) -> 11*
    __0(7,3) -> 11*
    __0(2,3) -> 11*
    __0(32,9) -> 11*
    __0(36,30) -> 11*
    __0(7,5) -> 11*
    __0(31,30) -> 11*
    __0(2,5) -> 11*
    __0(36,32) -> 11*
    __0(7,7) -> 11*
    __0(31,32) -> 11*
    __0(2,7) -> 11*
    __0(36,34) -> 11*
    __0(7,9) -> 11*
    __0(31,34) -> 11*
    __0(2,9) -> 11*
    __0(36,36) -> 11*
    __0(6,30) -> 11*
    __0(31,36) -> 11*
    __0(1,30) -> 11*
    __0(6,32) -> 11*
    __0(1,32) -> 11*
    __0(6,34) -> 11*
    __0(1,34) -> 11*
    __0(6,36) -> 11*
    __0(33,2) -> 11*
    __0(1,36) -> 11*
    __0(33,4) -> 11*
    __0(33,6) -> 11*
    __0(8,2) -> 11*
    __0(3,2) -> 11*
    __0(33,8) -> 11*
    __0(8,4) -> 11*
    __0(3,4) -> 11*
    __0(8,6) -> 11*
    __0(32,31) -> 11*
    __0(3,6) -> 11*
    __0(8,8) -> 11*
    __0(32,33) -> 11*
    __0(3,8) -> 11*
    __0(32,35) -> 11*
    __0(7,31) -> 11*
    __0(2,31) -> 11*
    __0(7,33) -> 11*
    __0(2,33) -> 11*
    __0(7,35) -> 11*
    __0(34,1) -> 11*
    __0(2,35) -> 11*
    __0(34,3) -> 11*
    __0(34,5) -> 11*
    __0(9,1) -> 11*
    __0(4,1) -> 11*
    __0(34,7) -> 11*
    __0(9,3) -> 11*
    __0(4,3) -> 11*
    __0(34,9) -> 11*
    __0(9,5) -> 11*
    __0(33,30) -> 11*
    __0(4,5) -> 11*
    __0(9,7) -> 11*
    __0(33,32) -> 11*
    __0(4,7) -> 11*
    __0(9,9) -> 11*
    __0(33,34) -> 11*
    __0(4,9) -> 11*
    __0(8,30) -> 11*
    __0(33,36) -> 11*
    __0(3,30) -> 11*
    __0(8,32) -> 11*
    __0(3,32) -> 11*
    __0(8,34) -> 11*
    __0(3,34) -> 11*
    __0(8,36) -> 11*
    __0(35,2) -> 11*
    __0(3,36) -> 11*
    __0(30,2) -> 11*
    __0(35,4) -> 11*
    __0(30,4) -> 11*
    __0(35,6) -> 11*
    __0(30,6) -> 11*
    __0(5,2) -> 11*
    __0(35,8) -> 11*
    __0(30,8) -> 11*
    __0(5,4) -> 11*
    __0(34,31) -> 11*
    __0(5,6) -> 11*
    __0(34,33) -> 11*
    __0(5,8) -> 11*
    __0(34,35) -> 11*
    __0(9,31) -> 11*
    __0(4,31) -> 11*
    __0(9,33) -> 11*
    __0(4,33) -> 11*
    __0(9,35) -> 11*
    __0(36,1) -> 11*
    __0(4,35) -> 11*
    __0(31,1) -> 11*
    __0(36,3) -> 11*
    __0(31,3) -> 11*
    __0(36,5) -> 11*
    __0(31,5) -> 11*
    __0(6,1) -> 11*
    __0(36,7) -> 11*
    __0(1,1) -> 11*
    __0(31,7) -> 11*
    __0(6,3) -> 11*
    __0(36,9) -> 11*
    __0(1,3) -> 11*
    __0(31,9) -> 11*
    __0(35,30) -> 11*
    __0(6,5) -> 11*
    __0(30,30) -> 11*
    __0(1,5) -> 11*
    __0(35,32) -> 11*
    __0(6,7) -> 11*
    __0(30,32) -> 11*
    __0(1,7) -> 11*
    __0(35,34) -> 11*
    __0(6,9) -> 11*
    __0(30,34) -> 11*
    __0(1,9) -> 11*
    __0(35,36) -> 11*
    __0(5,30) -> 11*
    __0(30,36) -> 11*
    __0(5,32) -> 11*
    __0(5,34) -> 11*
    __0(5,36) -> 11*
    __0(32,2) -> 11*
    __0(32,4) -> 11*
    __0(32,6) -> 11*
    __0(7,2) -> 11*
    __0(2,2) -> 11*
    __0(32,8) -> 11*
    __0(7,4) -> 11*
    __0(2,4) -> 11*
    __0(36,31) -> 11*
    __0(7,6) -> 11*
    __0(31,31) -> 11*
    __0(2,6) -> 11*
    __0(36,33) -> 11*
    __0(7,8) -> 11*
    __0(31,33) -> 11*
    __0(2,8) -> 11*
    __0(36,35) -> 11*
    mark0(35) -> 1*
    mark0(30) -> 1*
    mark0(5) -> 1*
    mark0(32) -> 1*
    mark0(7) -> 1*
    mark0(2) -> 1*
    mark0(34) -> 1*
    mark0(9) -> 1*
    mark0(4) -> 1*
    mark0(36) -> 1*
    mark0(31) -> 1*
    mark0(6) -> 1*
    mark0(1) -> 1*
    mark0(33) -> 1*
    mark0(8) -> 1*
    mark0(3) -> 1*
    nil0() -> 2*
    and0(31,35) -> 12*
    and0(6,31) -> 12*
    and0(1,31) -> 12*
    and0(6,33) -> 12*
    and0(1,33) -> 12*
    and0(6,35) -> 12*
    and0(33,1) -> 12*
    and0(1,35) -> 12*
    and0(33,3) -> 12*
    and0(33,5) -> 12*
    and0(8,1) -> 12*
    and0(3,1) -> 12*
    and0(33,7) -> 12*
    and0(8,3) -> 12*
    and0(3,3) -> 12*
    and0(33,9) -> 12*
    and0(8,5) -> 12*
    and0(32,30) -> 12*
    and0(3,5) -> 12*
    and0(8,7) -> 12*
    and0(32,32) -> 12*
    and0(3,7) -> 12*
    and0(8,9) -> 12*
    and0(32,34) -> 12*
    and0(3,9) -> 12*
    and0(7,30) -> 12*
    and0(32,36) -> 12*
    and0(2,30) -> 12*
    and0(7,32) -> 12*
    and0(2,32) -> 12*
    and0(7,34) -> 12*
    and0(2,34) -> 12*
    and0(7,36) -> 12*
    and0(34,2) -> 12*
    and0(2,36) -> 12*
    and0(34,4) -> 12*
    and0(34,6) -> 12*
    and0(9,2) -> 12*
    and0(4,2) -> 12*
    and0(34,8) -> 12*
    and0(9,4) -> 12*
    and0(4,4) -> 12*
    and0(9,6) -> 12*
    and0(33,31) -> 12*
    and0(4,6) -> 12*
    and0(9,8) -> 12*
    and0(33,33) -> 12*
    and0(4,8) -> 12*
    and0(33,35) -> 12*
    and0(8,31) -> 12*
    and0(3,31) -> 12*
    and0(8,33) -> 12*
    and0(3,33) -> 12*
    and0(8,35) -> 12*
    and0(35,1) -> 12*
    and0(3,35) -> 12*
    and0(30,1) -> 12*
    and0(35,3) -> 12*
    and0(30,3) -> 12*
    and0(35,5) -> 12*
    and0(30,5) -> 12*
    and0(5,1) -> 12*
    and0(35,7) -> 12*
    and0(30,7) -> 12*
    and0(5,3) -> 12*
    and0(35,9) -> 12*
    and0(30,9) -> 12*
    and0(34,30) -> 12*
    and0(5,5) -> 12*
    and0(34,32) -> 12*
    and0(5,7) -> 12*
    and0(34,34) -> 12*
    and0(5,9) -> 12*
    and0(9,30) -> 12*
    and0(34,36) -> 12*
    and0(4,30) -> 12*
    and0(9,32) -> 12*
    and0(4,32) -> 12*
    and0(9,34) -> 12*
    and0(4,34) -> 12*
    and0(9,36) -> 12*
    and0(36,2) -> 12*
    and0(4,36) -> 12*
    and0(31,2) -> 12*
    and0(36,4) -> 12*
    and0(31,4) -> 12*
    and0(36,6) -> 12*
    and0(31,6) -> 12*
    and0(6,2) -> 12*
    and0(36,8) -> 12*
    and0(1,2) -> 12*
    and0(31,8) -> 12*
    and0(6,4) -> 12*
    and0(1,4) -> 12*
    and0(35,31) -> 12*
    and0(6,6) -> 12*
    and0(30,31) -> 12*
    and0(1,6) -> 12*
    and0(35,33) -> 12*
    and0(6,8) -> 12*
    and0(30,33) -> 12*
    and0(1,8) -> 12*
    and0(35,35) -> 12*
    and0(30,35) -> 12*
    and0(5,31) -> 12*
    and0(5,33) -> 12*
    and0(5,35) -> 12*
    and0(32,1) -> 12*
    and0(32,3) -> 12*
    and0(32,5) -> 12*
    and0(7,1) -> 12*
    and0(2,1) -> 12*
    and0(32,7) -> 12*
    and0(7,3) -> 12*
    and0(2,3) -> 12*
    and0(32,9) -> 12*
    and0(36,30) -> 12*
    and0(7,5) -> 12*
    and0(31,30) -> 12*
    and0(2,5) -> 12*
    and0(36,32) -> 12*
    and0(7,7) -> 12*
    and0(31,32) -> 12*
    and0(2,7) -> 12*
    and0(36,34) -> 12*
    and0(7,9) -> 12*
    and0(31,34) -> 12*
    and0(2,9) -> 12*
    and0(36,36) -> 12*
    and0(6,30) -> 12*
    and0(31,36) -> 12*
    and0(1,30) -> 12*
    and0(6,32) -> 12*
    and0(1,32) -> 12*
    and0(6,34) -> 12*
    and0(1,34) -> 12*
    and0(6,36) -> 12*
    and0(33,2) -> 12*
    and0(1,36) -> 12*
    and0(33,4) -> 12*
    and0(33,6) -> 12*
    and0(8,2) -> 12*
    and0(3,2) -> 12*
    and0(33,8) -> 12*
    and0(8,4) -> 12*
    and0(3,4) -> 12*
    and0(8,6) -> 12*
    and0(32,31) -> 12*
    and0(3,6) -> 12*
    and0(8,8) -> 12*
    and0(32,33) -> 12*
    and0(3,8) -> 12*
    and0(32,35) -> 12*
    and0(7,31) -> 12*
    and0(2,31) -> 12*
    and0(7,33) -> 12*
    and0(2,33) -> 12*
    and0(7,35) -> 12*
    and0(34,1) -> 12*
    and0(2,35) -> 12*
    and0(34,3) -> 12*
    and0(34,5) -> 12*
    and0(9,1) -> 12*
    and0(4,1) -> 12*
    and0(34,7) -> 12*
    and0(9,3) -> 12*
    and0(4,3) -> 12*
    and0(34,9) -> 12*
    and0(9,5) -> 12*
    and0(33,30) -> 12*
    and0(4,5) -> 12*
    and0(9,7) -> 12*
    and0(33,32) -> 12*
    and0(4,7) -> 12*
    and0(9,9) -> 12*
    and0(33,34) -> 12*
    and0(4,9) -> 12*
    and0(8,30) -> 12*
    and0(33,36) -> 12*
    and0(3,30) -> 12*
    and0(8,32) -> 12*
    and0(3,32) -> 12*
    and0(8,34) -> 12*
    and0(3,34) -> 12*
    and0(8,36) -> 12*
    and0(35,2) -> 12*
    and0(3,36) -> 12*
    and0(30,2) -> 12*
    and0(35,4) -> 12*
    and0(30,4) -> 12*
    and0(35,6) -> 12*
    and0(30,6) -> 12*
    and0(5,2) -> 12*
    and0(35,8) -> 12*
    and0(30,8) -> 12*
    and0(5,4) -> 12*
    and0(34,31) -> 12*
    and0(5,6) -> 12*
    and0(34,33) -> 12*
    and0(5,8) -> 12*
    and0(34,35) -> 12*
    and0(9,31) -> 12*
    and0(4,31) -> 12*
    and0(9,33) -> 12*
    and0(4,33) -> 12*
    and0(9,35) -> 12*
    and0(36,1) -> 12*
    and0(4,35) -> 12*
    and0(31,1) -> 12*
    and0(36,3) -> 12*
    and0(31,3) -> 12*
    and0(36,5) -> 12*
    and0(31,5) -> 12*
    and0(6,1) -> 12*
    and0(36,7) -> 12*
    and0(1,1) -> 12*
    and0(31,7) -> 12*
    and0(6,3) -> 12*
    and0(36,9) -> 12*
    and0(1,3) -> 12*
    and0(31,9) -> 12*
    and0(35,30) -> 12*
    and0(6,5) -> 12*
    and0(30,30) -> 12*
    and0(1,5) -> 12*
    and0(35,32) -> 12*
    and0(6,7) -> 12*
    and0(30,32) -> 12*
    and0(1,7) -> 12*
    and0(35,34) -> 12*
    and0(6,9) -> 12*
    and0(30,34) -> 12*
    and0(1,9) -> 12*
    and0(35,36) -> 12*
    and0(5,30) -> 12*
    and0(30,36) -> 12*
    and0(5,32) -> 12*
    and0(5,34) -> 12*
    and0(5,36) -> 12*
    and0(32,2) -> 12*
    and0(32,4) -> 12*
    and0(32,6) -> 12*
    and0(7,2) -> 12*
    and0(2,2) -> 12*
    and0(32,8) -> 12*
    and0(7,4) -> 12*
    and0(2,4) -> 12*
    and0(36,31) -> 12*
    and0(7,6) -> 12*
    and0(31,31) -> 12*
    and0(2,6) -> 12*
    and0(36,33) -> 12*
    and0(7,8) -> 12*
    and0(31,33) -> 12*
    and0(2,8) -> 12*
    and0(36,35) -> 12*
    tt0() -> 3*
    isList0(35) -> 14*
    isList0(30) -> 14*
    isList0(5) -> 14*
    isList0(32) -> 14*
    isList0(7) -> 14*
    isList0(2) -> 14*
    isList0(34) -> 14*
    isList0(9) -> 14*
    isList0(4) -> 14*
    isList0(36) -> 14*
    isList0(31) -> 14*
    isList0(6) -> 14*
    isList0(1) -> 14*
    isList0(33) -> 14*
    isList0(8) -> 14*
    isList0(3) -> 14*
    isNeList0(35) -> 15*
    isNeList0(30) -> 15*
    isNeList0(5) -> 15*
    isNeList0(32) -> 15*
    isNeList0(7) -> 15*
    isNeList0(2) -> 15*
    isNeList0(34) -> 15*
    isNeList0(9) -> 15*
    isNeList0(4) -> 15*
    isNeList0(36) -> 15*
    isNeList0(31) -> 15*
    isNeList0(6) -> 15*
    isNeList0(1) -> 15*
    isNeList0(33) -> 15*
    isNeList0(8) -> 15*
    isNeList0(3) -> 15*
    isQid0(35) -> 16*
    isQid0(30) -> 16*
    isQid0(5) -> 16*
    isQid0(32) -> 16*
    isQid0(7) -> 16*
    isQid0(2) -> 16*
    isQid0(34) -> 16*
    isQid0(9) -> 16*
    isQid0(4) -> 16*
    isQid0(36) -> 16*
    isQid0(31) -> 16*
    isQid0(6) -> 16*
    isQid0(1) -> 16*
    isQid0(33) -> 16*
    isQid0(8) -> 16*
    isQid0(3) -> 16*
    isNePal0(35) -> 17*
    isNePal0(30) -> 17*
    isNePal0(5) -> 17*
    isNePal0(32) -> 17*
    isNePal0(7) -> 17*
    isNePal0(2) -> 17*
    isNePal0(34) -> 17*
    isNePal0(9) -> 17*
    isNePal0(4) -> 17*
    isNePal0(36) -> 17*
    isNePal0(31) -> 17*
    isNePal0(6) -> 17*
    isNePal0(1) -> 17*
    isNePal0(33) -> 17*
    isNePal0(8) -> 17*
    isNePal0(3) -> 17*
    isPal0(35) -> 18*
    isPal0(30) -> 18*
    isPal0(5) -> 18*
    isPal0(32) -> 18*
    isPal0(7) -> 18*
    isPal0(2) -> 18*
    isPal0(34) -> 18*
    isPal0(9) -> 18*
    isPal0(4) -> 18*
    isPal0(36) -> 18*
    isPal0(31) -> 18*
    isPal0(6) -> 18*
    isPal0(1) -> 18*
    isPal0(33) -> 18*
    isPal0(8) -> 18*
    isPal0(3) -> 18*
    a0() -> 4*
    e0() -> 5*
    i0() -> 6*
    o0() -> 7*
    u0() -> 8*
    proper0(35) -> 13*
    proper0(30) -> 13*
    proper0(5) -> 13*
    proper0(32) -> 13*
    proper0(7) -> 13*
    proper0(2) -> 13*
    proper0(34) -> 13*
    proper0(9) -> 13*
    proper0(4) -> 13*
    proper0(36) -> 13*
    proper0(31) -> 13*
    proper0(6) -> 13*
    proper0(1) -> 13*
    proper0(33) -> 13*
    proper0(8) -> 13*
    proper0(3) -> 13*
    ok0(35) -> 9*
    ok0(30) -> 9*
    ok0(5) -> 9*
    ok0(32) -> 9*
    ok0(7) -> 9*
    ok0(2) -> 9*
    ok0(34) -> 9*
    ok0(9) -> 9*
    ok0(4) -> 9*
    ok0(36) -> 9*
    ok0(31) -> 9*
    ok0(6) -> 9*
    ok0(1) -> 9*
    ok0(33) -> 9*
    ok0(8) -> 9*
    ok0(3) -> 9*
    top0(35) -> 19*
    top0(30) -> 19*
    top0(5) -> 19*
    top0(32) -> 19*
    top0(7) -> 19*
    top0(2) -> 19*
    top0(34) -> 19*
    top0(9) -> 19*
    top0(4) -> 19*
    top0(36) -> 19*
    top0(31) -> 19*
    top0(6) -> 19*
    top0(1) -> 19*
    top0(33) -> 19*
    top0(8) -> 19*
    top0(3) -> 19*
    top1(30) -> 19*
    top1(29) -> 19*
    top1(13) -> 19*
    active1(35) -> 10,29*
    active1(30) -> 10,29*
    active1(5) -> 29*,10,13
    active1(32) -> 10,29*
    active1(7) -> 29*,10,13
    active1(2) -> 29*,10,13
    active1(34) -> 10,29*
    active1(9) -> 29*,10,13
    active1(4) -> 29*,10,13
    active1(36) -> 10,29*
    active1(31) -> 10,29*
    active1(6) -> 29*,10,13
    active1(1) -> 29*,10,13
    active1(33) -> 10,29*
    active1(8) -> 29*,10,13
    active1(3) -> 29*,10,13
    proper1(35) -> 13*
    proper1(30) -> 13*
    proper1(5) -> 13*
    proper1(32) -> 13*
    proper1(7) -> 13*
    proper1(2) -> 13*
    proper1(34) -> 13*
    proper1(9) -> 13*
    proper1(4) -> 13*
    proper1(36) -> 13*
    proper1(31) -> 13*
    proper1(6) -> 13*
    proper1(1) -> 13*
    proper1(33) -> 13*
    proper1(8) -> 13*
    proper1(3) -> 13*
    ok1(35) -> 9,30*
    ok1(15) -> 15*
    ok1(32) -> 9,30*
    ok1(17) -> 17*
    ok1(12) -> 12*
    ok1(2) -> 30*,9,13
    ok1(34) -> 9,30*
    ok1(14) -> 14*
    ok1(36) -> 9,30*
    ok1(31) -> 9,30*
    ok1(16) -> 16*
    ok1(11) -> 11*
    ok1(33) -> 9,30*
    ok1(18) -> 18*
    isPal1(35) -> 18*
    isPal1(30) -> 18*
    isPal1(5) -> 18*
    isPal1(32) -> 18*
    isPal1(7) -> 18*
    isPal1(2) -> 18*
    isPal1(34) -> 18*
    isPal1(9) -> 18*
    isPal1(4) -> 18*
    isPal1(36) -> 18*
    isPal1(31) -> 18*
    isPal1(6) -> 18*
    isPal1(1) -> 18*
    isPal1(33) -> 18*
    isPal1(8) -> 18*
    isPal1(3) -> 18*
    isNePal1(35) -> 17*
    isNePal1(30) -> 17*
    isNePal1(5) -> 17*
    isNePal1(32) -> 17*
    isNePal1(7) -> 17*
    isNePal1(2) -> 17*
    isNePal1(34) -> 17*
    isNePal1(9) -> 17*
    isNePal1(4) -> 17*
    isNePal1(36) -> 17*
    isNePal1(31) -> 17*
    isNePal1(6) -> 17*
    isNePal1(1) -> 17*
    isNePal1(33) -> 17*
    isNePal1(8) -> 17*
    isNePal1(3) -> 17*
    isQid1(35) -> 16*
    isQid1(30) -> 16*
    isQid1(5) -> 16*
    isQid1(32) -> 16*
    isQid1(7) -> 16*
    isQid1(2) -> 16*
    isQid1(34) -> 16*
    isQid1(9) -> 16*
    isQid1(4) -> 16*
    isQid1(36) -> 16*
    isQid1(31) -> 16*
    isQid1(6) -> 16*
    isQid1(1) -> 16*
    isQid1(33) -> 16*
    isQid1(8) -> 16*
    isQid1(3) -> 16*
    isNeList1(35) -> 15*
    isNeList1(30) -> 15*
    isNeList1(5) -> 15*
    isNeList1(32) -> 15*
    isNeList1(7) -> 15*
    isNeList1(2) -> 15*
    isNeList1(34) -> 15*
    isNeList1(9) -> 15*
    isNeList1(4) -> 15*
    isNeList1(36) -> 15*
    isNeList1(31) -> 15*
    isNeList1(6) -> 15*
    isNeList1(1) -> 15*
    isNeList1(33) -> 15*
    isNeList1(8) -> 15*
    isNeList1(3) -> 15*
    isList1(35) -> 14*
    isList1(30) -> 14*
    isList1(5) -> 14*
    isList1(32) -> 14*
    isList1(7) -> 14*
    isList1(2) -> 14*
    isList1(34) -> 14*
    isList1(9) -> 14*
    isList1(4) -> 14*
    isList1(36) -> 14*
    isList1(31) -> 14*
    isList1(6) -> 14*
    isList1(1) -> 14*
    isList1(33) -> 14*
    isList1(8) -> 14*
    isList1(3) -> 14*
    and1(2,4) -> 12*
    and1(36,31) -> 12*
    and1(7,6) -> 12*
    and1(31,31) -> 12*
    and1(2,6) -> 12*
    and1(36,33) -> 12*
    and1(7,8) -> 12*
    and1(31,33) -> 12*
    and1(2,8) -> 12*
    and1(36,35) -> 12*
    and1(31,35) -> 12*
    and1(6,31) -> 12*
    and1(1,31) -> 12*
    and1(6,33) -> 12*
    and1(1,33) -> 12*
    and1(6,35) -> 12*
    and1(33,1) -> 12*
    and1(1,35) -> 12*
    and1(33,3) -> 12*
    and1(33,5) -> 12*
    and1(8,1) -> 12*
    and1(3,1) -> 12*
    and1(33,7) -> 12*
    and1(8,3) -> 12*
    and1(3,3) -> 12*
    and1(33,9) -> 12*
    and1(8,5) -> 12*
    and1(32,30) -> 12*
    and1(3,5) -> 12*
    and1(8,7) -> 12*
    and1(32,32) -> 12*
    and1(3,7) -> 12*
    and1(8,9) -> 12*
    and1(32,34) -> 12*
    and1(3,9) -> 12*
    and1(7,30) -> 12*
    and1(32,36) -> 12*
    and1(2,30) -> 12*
    and1(7,32) -> 12*
    and1(2,32) -> 12*
    and1(7,34) -> 12*
    and1(2,34) -> 12*
    and1(7,36) -> 12*
    and1(34,2) -> 12*
    and1(2,36) -> 12*
    and1(34,4) -> 12*
    and1(34,6) -> 12*
    and1(9,2) -> 12*
    and1(4,2) -> 12*
    and1(34,8) -> 12*
    and1(9,4) -> 12*
    and1(4,4) -> 12*
    and1(9,6) -> 12*
    and1(33,31) -> 12*
    and1(4,6) -> 12*
    and1(9,8) -> 12*
    and1(33,33) -> 12*
    and1(4,8) -> 12*
    and1(33,35) -> 12*
    and1(8,31) -> 12*
    and1(3,31) -> 12*
    and1(8,33) -> 12*
    and1(3,33) -> 12*
    and1(8,35) -> 12*
    and1(35,1) -> 12*
    and1(3,35) -> 12*
    and1(30,1) -> 12*
    and1(35,3) -> 12*
    and1(30,3) -> 12*
    and1(35,5) -> 12*
    and1(30,5) -> 12*
    and1(5,1) -> 12*
    and1(35,7) -> 12*
    and1(30,7) -> 12*
    and1(5,3) -> 12*
    and1(35,9) -> 12*
    and1(30,9) -> 12*
    and1(34,30) -> 12*
    and1(5,5) -> 12*
    and1(34,32) -> 12*
    and1(5,7) -> 12*
    and1(34,34) -> 12*
    and1(5,9) -> 12*
    and1(9,30) -> 12*
    and1(34,36) -> 12*
    and1(4,30) -> 12*
    and1(9,32) -> 12*
    and1(4,32) -> 12*
    and1(9,34) -> 12*
    and1(4,34) -> 12*
    and1(9,36) -> 12*
    and1(36,2) -> 12*
    and1(4,36) -> 12*
    and1(31,2) -> 12*
    and1(36,4) -> 12*
    and1(31,4) -> 12*
    and1(36,6) -> 12*
    and1(31,6) -> 12*
    and1(6,2) -> 12*
    and1(36,8) -> 12*
    and1(1,2) -> 12*
    and1(31,8) -> 12*
    and1(6,4) -> 12*
    and1(1,4) -> 12*
    and1(35,31) -> 12*
    and1(6,6) -> 12*
    and1(30,31) -> 12*
    and1(1,6) -> 12*
    and1(35,33) -> 12*
    and1(6,8) -> 12*
    and1(30,33) -> 12*
    and1(1,8) -> 12*
    and1(35,35) -> 12*
    and1(30,35) -> 12*
    and1(5,31) -> 12*
    and1(5,33) -> 12*
    and1(5,35) -> 12*
    and1(32,1) -> 12*
    and1(32,3) -> 12*
    and1(32,5) -> 12*
    and1(7,1) -> 12*
    and1(2,1) -> 12*
    and1(32,7) -> 12*
    and1(7,3) -> 12*
    and1(2,3) -> 12*
    and1(32,9) -> 12*
    and1(36,30) -> 12*
    and1(7,5) -> 12*
    and1(31,30) -> 12*
    and1(2,5) -> 12*
    and1(36,32) -> 12*
    and1(7,7) -> 12*
    and1(31,32) -> 12*
    and1(2,7) -> 12*
    and1(36,34) -> 12*
    and1(7,9) -> 12*
    and1(31,34) -> 12*
    and1(2,9) -> 12*
    and1(36,36) -> 12*
    and1(6,30) -> 12*
    and1(31,36) -> 12*
    and1(1,30) -> 12*
    and1(6,32) -> 12*
    and1(1,32) -> 12*
    and1(6,34) -> 12*
    and1(1,34) -> 12*
    and1(6,36) -> 12*
    and1(33,2) -> 12*
    and1(1,36) -> 12*
    and1(33,4) -> 12*
    and1(33,6) -> 12*
    and1(8,2) -> 12*
    and1(3,2) -> 12*
    and1(33,8) -> 12*
    and1(8,4) -> 12*
    and1(3,4) -> 12*
    and1(8,6) -> 12*
    and1(32,31) -> 12*
    and1(3,6) -> 12*
    and1(8,8) -> 12*
    and1(32,33) -> 12*
    and1(3,8) -> 12*
    and1(32,35) -> 12*
    and1(7,31) -> 12*
    and1(2,31) -> 12*
    and1(7,33) -> 12*
    and1(2,33) -> 12*
    and1(7,35) -> 12*
    and1(34,1) -> 12*
    and1(2,35) -> 12*
    and1(34,3) -> 12*
    and1(34,5) -> 12*
    and1(9,1) -> 12*
    and1(4,1) -> 12*
    and1(34,7) -> 12*
    and1(9,3) -> 12*
    and1(4,3) -> 12*
    and1(34,9) -> 12*
    and1(9,5) -> 12*
    and1(33,30) -> 12*
    and1(4,5) -> 12*
    and1(9,7) -> 12*
    and1(33,32) -> 12*
    and1(4,7) -> 12*
    and1(9,9) -> 12*
    and1(33,34) -> 12*
    and1(4,9) -> 12*
    and1(8,30) -> 12*
    and1(33,36) -> 12*
    and1(3,30) -> 12*
    and1(8,32) -> 12*
    and1(3,32) -> 12*
    and1(8,34) -> 12*
    and1(3,34) -> 12*
    and1(8,36) -> 12*
    and1(35,2) -> 12*
    and1(3,36) -> 12*
    and1(30,2) -> 12*
    and1(35,4) -> 12*
    and1(30,4) -> 12*
    and1(35,6) -> 12*
    and1(30,6) -> 12*
    and1(5,2) -> 12*
    and1(35,8) -> 12*
    and1(30,8) -> 12*
    and1(5,4) -> 12*
    and1(34,31) -> 12*
    and1(5,6) -> 12*
    and1(34,33) -> 12*
    and1(5,8) -> 12*
    and1(34,35) -> 12*
    and1(9,31) -> 12*
    and1(4,31) -> 12*
    and1(9,33) -> 12*
    and1(4,33) -> 12*
    and1(9,35) -> 12*
    and1(36,1) -> 12*
    and1(4,35) -> 12*
    and1(31,1) -> 12*
    and1(36,3) -> 12*
    and1(31,3) -> 12*
    and1(36,5) -> 12*
    and1(31,5) -> 12*
    and1(6,1) -> 12*
    and1(36,7) -> 12*
    and1(1,1) -> 12*
    and1(31,7) -> 12*
    and1(6,3) -> 12*
    and1(36,9) -> 12*
    and1(1,3) -> 12*
    and1(31,9) -> 12*
    and1(35,30) -> 12*
    and1(6,5) -> 12*
    and1(30,30) -> 12*
    and1(1,5) -> 12*
    and1(35,32) -> 12*
    and1(6,7) -> 12*
    and1(30,32) -> 12*
    and1(1,7) -> 12*
    and1(35,34) -> 12*
    and1(6,9) -> 12*
    and1(30,34) -> 12*
    and1(1,9) -> 12*
    and1(35,36) -> 12*
    and1(5,30) -> 12*
    and1(30,36) -> 12*
    and1(5,32) -> 12*
    and1(5,34) -> 12*
    and1(5,36) -> 12*
    and1(32,2) -> 12*
    and1(32,4) -> 12*
    and1(32,6) -> 12*
    and1(7,2) -> 12*
    and1(2,2) -> 12*
    and1(32,8) -> 12*
    and1(7,4) -> 12*
    __1(2,4) -> 11*
    __1(36,31) -> 11*
    __1(7,6) -> 11*
    __1(31,31) -> 11*
    __1(2,6) -> 11*
    __1(36,33) -> 11*
    __1(7,8) -> 11*
    __1(31,33) -> 11*
    __1(2,8) -> 11*
    __1(36,35) -> 11*
    __1(31,35) -> 11*
    __1(6,31) -> 11*
    __1(1,31) -> 11*
    __1(6,33) -> 11*
    __1(1,33) -> 11*
    __1(6,35) -> 11*
    __1(33,1) -> 11*
    __1(1,35) -> 11*
    __1(33,3) -> 11*
    __1(33,5) -> 11*
    __1(8,1) -> 11*
    __1(3,1) -> 11*
    __1(33,7) -> 11*
    __1(8,3) -> 11*
    __1(3,3) -> 11*
    __1(33,9) -> 11*
    __1(8,5) -> 11*
    __1(32,30) -> 11*
    __1(3,5) -> 11*
    __1(8,7) -> 11*
    __1(32,32) -> 11*
    __1(3,7) -> 11*
    __1(8,9) -> 11*
    __1(32,34) -> 11*
    __1(3,9) -> 11*
    __1(7,30) -> 11*
    __1(32,36) -> 11*
    __1(2,30) -> 11*
    __1(7,32) -> 11*
    __1(2,32) -> 11*
    __1(7,34) -> 11*
    __1(2,34) -> 11*
    __1(7,36) -> 11*
    __1(34,2) -> 11*
    __1(2,36) -> 11*
    __1(34,4) -> 11*
    __1(34,6) -> 11*
    __1(9,2) -> 11*
    __1(4,2) -> 11*
    __1(34,8) -> 11*
    __1(9,4) -> 11*
    __1(4,4) -> 11*
    __1(9,6) -> 11*
    __1(33,31) -> 11*
    __1(4,6) -> 11*
    __1(9,8) -> 11*
    __1(33,33) -> 11*
    __1(4,8) -> 11*
    __1(33,35) -> 11*
    __1(8,31) -> 11*
    __1(3,31) -> 11*
    __1(8,33) -> 11*
    __1(3,33) -> 11*
    __1(8,35) -> 11*
    __1(35,1) -> 11*
    __1(3,35) -> 11*
    __1(30,1) -> 11*
    __1(35,3) -> 11*
    __1(30,3) -> 11*
    __1(35,5) -> 11*
    __1(30,5) -> 11*
    __1(5,1) -> 11*
    __1(35,7) -> 11*
    __1(30,7) -> 11*
    __1(5,3) -> 11*
    __1(35,9) -> 11*
    __1(30,9) -> 11*
    __1(34,30) -> 11*
    __1(5,5) -> 11*
    __1(34,32) -> 11*
    __1(5,7) -> 11*
    __1(34,34) -> 11*
    __1(5,9) -> 11*
    __1(9,30) -> 11*
    __1(34,36) -> 11*
    __1(4,30) -> 11*
    __1(9,32) -> 11*
    __1(4,32) -> 11*
    __1(9,34) -> 11*
    __1(4,34) -> 11*
    __1(9,36) -> 11*
    __1(36,2) -> 11*
    __1(4,36) -> 11*
    __1(31,2) -> 11*
    __1(36,4) -> 11*
    __1(31,4) -> 11*
    __1(36,6) -> 11*
    __1(31,6) -> 11*
    __1(6,2) -> 11*
    __1(36,8) -> 11*
    __1(1,2) -> 11*
    __1(31,8) -> 11*
    __1(6,4) -> 11*
    __1(1,4) -> 11*
    __1(35,31) -> 11*
    __1(6,6) -> 11*
    __1(30,31) -> 11*
    __1(1,6) -> 11*
    __1(35,33) -> 11*
    __1(6,8) -> 11*
    __1(30,33) -> 11*
    __1(1,8) -> 11*
    __1(35,35) -> 11*
    __1(30,35) -> 11*
    __1(5,31) -> 11*
    __1(5,33) -> 11*
    __1(5,35) -> 11*
    __1(32,1) -> 11*
    __1(32,3) -> 11*
    __1(32,5) -> 11*
    __1(7,1) -> 11*
    __1(2,1) -> 11*
    __1(32,7) -> 11*
    __1(7,3) -> 11*
    __1(2,3) -> 11*
    __1(32,9) -> 11*
    __1(36,30) -> 11*
    __1(7,5) -> 11*
    __1(31,30) -> 11*
    __1(2,5) -> 11*
    __1(36,32) -> 11*
    __1(7,7) -> 11*
    __1(31,32) -> 11*
    __1(2,7) -> 11*
    __1(36,34) -> 11*
    __1(7,9) -> 11*
    __1(31,34) -> 11*
    __1(2,9) -> 11*
    __1(36,36) -> 11*
    __1(6,30) -> 11*
    __1(31,36) -> 11*
    __1(1,30) -> 11*
    __1(6,32) -> 11*
    __1(1,32) -> 11*
    __1(6,34) -> 11*
    __1(1,34) -> 11*
    __1(6,36) -> 11*
    __1(33,2) -> 11*
    __1(1,36) -> 11*
    __1(33,4) -> 11*
    __1(33,6) -> 11*
    __1(8,2) -> 11*
    __1(3,2) -> 11*
    __1(33,8) -> 11*
    __1(8,4) -> 11*
    __1(3,4) -> 11*
    __1(8,6) -> 11*
    __1(32,31) -> 11*
    __1(3,6) -> 11*
    __1(8,8) -> 11*
    __1(32,33) -> 11*
    __1(3,8) -> 11*
    __1(32,35) -> 11*
    __1(7,31) -> 11*
    __1(2,31) -> 11*
    __1(7,33) -> 11*
    __1(2,33) -> 11*
    __1(7,35) -> 11*
    __1(34,1) -> 11*
    __1(2,35) -> 11*
    __1(34,3) -> 11*
    __1(34,5) -> 11*
    __1(9,1) -> 11*
    __1(4,1) -> 11*
    __1(34,7) -> 11*
    __1(9,3) -> 11*
    __1(4,3) -> 11*
    __1(34,9) -> 11*
    __1(9,5) -> 11*
    __1(33,30) -> 11*
    __1(4,5) -> 11*
    __1(9,7) -> 11*
    __1(33,32) -> 11*
    __1(4,7) -> 11*
    __1(9,9) -> 11*
    __1(33,34) -> 11*
    __1(4,9) -> 11*
    __1(8,30) -> 11*
    __1(33,36) -> 11*
    __1(3,30) -> 11*
    __1(8,32) -> 11*
    __1(3,32) -> 11*
    __1(8,34) -> 11*
    __1(3,34) -> 11*
    __1(8,36) -> 11*
    __1(35,2) -> 11*
    __1(3,36) -> 11*
    __1(30,2) -> 11*
    __1(35,4) -> 11*
    __1(30,4) -> 11*
    __1(35,6) -> 11*
    __1(30,6) -> 11*
    __1(5,2) -> 11*
    __1(35,8) -> 11*
    __1(30,8) -> 11*
    __1(5,4) -> 11*
    __1(34,31) -> 11*
    __1(5,6) -> 11*
    __1(34,33) -> 11*
    __1(5,8) -> 11*
    __1(34,35) -> 11*
    __1(9,31) -> 11*
    __1(4,31) -> 11*
    __1(9,33) -> 11*
    __1(4,33) -> 11*
    __1(9,35) -> 11*
    __1(36,1) -> 11*
    __1(4,35) -> 11*
    __1(31,1) -> 11*
    __1(36,3) -> 11*
    __1(31,3) -> 11*
    __1(36,5) -> 11*
    __1(31,5) -> 11*
    __1(6,1) -> 11*
    __1(36,7) -> 11*
    __1(1,1) -> 11*
    __1(31,7) -> 11*
    __1(6,3) -> 11*
    __1(36,9) -> 11*
    __1(1,3) -> 11*
    __1(31,9) -> 11*
    __1(35,30) -> 11*
    __1(6,5) -> 11*
    __1(30,30) -> 11*
    __1(1,5) -> 11*
    __1(35,32) -> 11*
    __1(6,7) -> 11*
    __1(30,32) -> 11*
    __1(1,7) -> 11*
    __1(35,34) -> 11*
    __1(6,9) -> 11*
    __1(30,34) -> 11*
    __1(1,9) -> 11*
    __1(35,36) -> 11*
    __1(5,30) -> 11*
    __1(30,36) -> 11*
    __1(5,32) -> 11*
    __1(5,34) -> 11*
    __1(5,36) -> 11*
    __1(32,2) -> 11*
    __1(32,4) -> 11*
    __1(32,6) -> 11*
    __1(7,2) -> 11*
    __1(2,2) -> 11*
    __1(32,8) -> 11*
    __1(7,4) -> 11*
    u1() -> 31*,8,2
    o1() -> 32*,7,2
    i1() -> 33*,6,2
    e1() -> 34*,5,2
    a1() -> 35*,4,2
    tt1() -> 36*,3,2
    nil1() -> 2*
    mark1(12) -> 12*
    mark1(11) -> 11*
    top2(10) -> 19*
    top2(29) -> 19*
    active2(35) -> 29*,10
    active2(32) -> 29*,10
    active2(2) -> 13,29*,10
    active2(34) -> 29*,10
    active2(36) -> 29*,10
    active2(31) -> 29*,10
    active2(33) -> 29*,10
    ok2(35) -> 9,30*
    ok2(15) -> 15*
    ok2(32) -> 9,30*
    ok2(17) -> 17*
    ok2(12) -> 12*
    ok2(2) -> 9,30*,13
    ok2(34) -> 9,30*
    ok2(14) -> 14*
    ok2(36) -> 9,30*
    ok2(31) -> 9,30*
    ok2(16) -> 16*
    ok2(11) -> 11*
    ok2(33) -> 9,30*
    ok2(18) -> 18*
    isPal2(35) -> 18*
    isPal2(32) -> 18*
    isPal2(2) -> 18*
    isPal2(34) -> 18*
    isPal2(36) -> 18*
    isPal2(31) -> 18*
    isPal2(33) -> 18*
    isNePal2(35) -> 17*
    isNePal2(32) -> 17*
    isNePal2(2) -> 17*
    isNePal2(34) -> 17*
    isNePal2(36) -> 17*
    isNePal2(31) -> 17*
    isNePal2(33) -> 17*
    isQid2(35) -> 16*
    isQid2(32) -> 16*
    isQid2(2) -> 16*
    isQid2(34) -> 16*
    isQid2(36) -> 16*
    isQid2(31) -> 16*
    isQid2(33) -> 16*
    isNeList2(35) -> 15*
    isNeList2(32) -> 15*
    isNeList2(2) -> 15*
    isNeList2(34) -> 15*
    isNeList2(36) -> 15*
    isNeList2(31) -> 15*
    isNeList2(33) -> 15*
    isList2(35) -> 14*
    isList2(32) -> 14*
    isList2(2) -> 14*
    isList2(34) -> 14*
    isList2(36) -> 14*
    isList2(31) -> 14*
    isList2(33) -> 14*
    and2(2,2) -> 12*
    and2(36,31) -> 12*
    and2(31,31) -> 12*
    and2(36,33) -> 12*
    and2(31,33) -> 12*
    and2(36,35) -> 12*
    and2(31,35) -> 12*
    and2(32,32) -> 12*
    and2(32,34) -> 12*
    and2(32,36) -> 12*
    and2(2,32) -> 12*
    and2(2,34) -> 12*
    and2(34,2) -> 12*
    and2(2,36) -> 12*
    and2(33,31) -> 12*
    and2(33,33) -> 12*
    and2(33,35) -> 12*
    and2(34,32) -> 12*
    and2(34,34) -> 12*
    and2(34,36) -> 12*
    and2(36,2) -> 12*
    and2(31,2) -> 12*
    and2(35,31) -> 12*
    and2(35,33) -> 12*
    and2(35,35) -> 12*
    and2(36,32) -> 12*
    and2(31,32) -> 12*
    and2(36,34) -> 12*
    and2(31,34) -> 12*
    and2(36,36) -> 12*
    and2(31,36) -> 12*
    and2(33,2) -> 12*
    and2(32,31) -> 12*
    and2(32,33) -> 12*
    and2(32,35) -> 12*
    and2(2,31) -> 12*
    and2(2,33) -> 12*
    and2(2,35) -> 12*
    and2(33,32) -> 12*
    and2(33,34) -> 12*
    and2(33,36) -> 12*
    and2(35,2) -> 12*
    and2(34,31) -> 12*
    and2(34,33) -> 12*
    and2(34,35) -> 12*
    and2(35,32) -> 12*
    and2(35,34) -> 12*
    and2(35,36) -> 12*
    and2(32,2) -> 12*
    __2(2,2) -> 11*
    __2(36,31) -> 11*
    __2(31,31) -> 11*
    __2(36,33) -> 11*
    __2(31,33) -> 11*
    __2(36,35) -> 11*
    __2(31,35) -> 11*
    __2(32,32) -> 11*
    __2(32,34) -> 11*
    __2(32,36) -> 11*
    __2(2,32) -> 11*
    __2(2,34) -> 11*
    __2(34,2) -> 11*
    __2(2,36) -> 11*
    __2(33,31) -> 11*
    __2(33,33) -> 11*
    __2(33,35) -> 11*
    __2(34,32) -> 11*
    __2(34,34) -> 11*
    __2(34,36) -> 11*
    __2(36,2) -> 11*
    __2(31,2) -> 11*
    __2(35,31) -> 11*
    __2(35,33) -> 11*
    __2(35,35) -> 11*
    __2(36,32) -> 11*
    __2(31,32) -> 11*
    __2(36,34) -> 11*
    __2(31,34) -> 11*
    __2(36,36) -> 11*
    __2(31,36) -> 11*
    __2(33,2) -> 11*
    __2(32,31) -> 11*
    __2(32,33) -> 11*
    __2(32,35) -> 11*
    __2(2,31) -> 11*
    __2(2,33) -> 11*
    __2(2,35) -> 11*
    __2(33,32) -> 11*
    __2(33,34) -> 11*
    __2(33,36) -> 11*
    __2(35,2) -> 11*
    __2(34,31) -> 11*
    __2(34,33) -> 11*
    __2(34,35) -> 11*
    __2(35,32) -> 11*
    __2(35,34) -> 11*
    __2(35,36) -> 11*
    __2(32,2) -> 11*
    u2() -> 8,31*,2
    o2() -> 7,32*,2
    i2() -> 6,33*,2
    e2() -> 5,34*,2
    a2() -> 4,35*,2
    tt2() -> 3,36*,2
    nil2() -> 2*
  problem:
   
  Qed

Tool IRC1

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 PALINDROME nokinds C

stdout:

YES(?,O(n^1))

Tool IRC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 PALINDROME nokinds C

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z)))
     , active(__(X, nil())) -> mark(X)
     , active(__(nil(), X)) -> mark(X)
     , active(and(tt(), X)) -> mark(X)
     , active(isList(V)) -> mark(isNeList(V))
     , active(isList(nil())) -> mark(tt())
     , active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2)))
     , active(isNeList(V)) -> mark(isQid(V))
     , active(isNeList(__(V1, V2))) ->
       mark(and(isList(V1), isNeList(V2)))
     , active(isNeList(__(V1, V2))) ->
       mark(and(isNeList(V1), isList(V2)))
     , active(isNePal(V)) -> mark(isQid(V))
     , active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P)))
     , active(isPal(V)) -> mark(isNePal(V))
     , active(isPal(nil())) -> mark(tt())
     , active(isQid(a())) -> mark(tt())
     , active(isQid(e())) -> mark(tt())
     , active(isQid(i())) -> mark(tt())
     , active(isQid(o())) -> mark(tt())
     , active(isQid(u())) -> mark(tt())
     , active(__(X1, X2)) -> __(active(X1), X2)
     , active(__(X1, X2)) -> __(X1, active(X2))
     , active(and(X1, X2)) -> and(active(X1), X2)
     , __(mark(X1), X2) -> mark(__(X1, X2))
     , __(X1, mark(X2)) -> mark(__(X1, X2))
     , and(mark(X1), X2) -> mark(and(X1, X2))
     , proper(__(X1, X2)) -> __(proper(X1), proper(X2))
     , proper(nil()) -> ok(nil())
     , proper(and(X1, X2)) -> and(proper(X1), proper(X2))
     , proper(tt()) -> ok(tt())
     , proper(isList(X)) -> isList(proper(X))
     , proper(isNeList(X)) -> isNeList(proper(X))
     , proper(isQid(X)) -> isQid(proper(X))
     , proper(isNePal(X)) -> isNePal(proper(X))
     , proper(isPal(X)) -> isPal(proper(X))
     , proper(a()) -> ok(a())
     , proper(e()) -> ok(e())
     , proper(i()) -> ok(i())
     , proper(o()) -> ok(o())
     , proper(u()) -> ok(u())
     , __(ok(X1), ok(X2)) -> ok(__(X1, X2))
     , and(ok(X1), ok(X2)) -> ok(and(X1, X2))
     , isList(ok(X)) -> ok(isList(X))
     , isNeList(ok(X)) -> ok(isNeList(X))
     , isQid(ok(X)) -> ok(isQid(X))
     , isNePal(ok(X)) -> ok(isNePal(X))
     , isPal(ok(X)) -> ok(isPal(X))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X))}

Proof Output:    
  'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
  
  Details:
  --------
    'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with minimal-enrichment and initial automaton 'match''
     --------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z)))
          , active(__(X, nil())) -> mark(X)
          , active(__(nil(), X)) -> mark(X)
          , active(and(tt(), X)) -> mark(X)
          , active(isList(V)) -> mark(isNeList(V))
          , active(isList(nil())) -> mark(tt())
          , active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2)))
          , active(isNeList(V)) -> mark(isQid(V))
          , active(isNeList(__(V1, V2))) ->
            mark(and(isList(V1), isNeList(V2)))
          , active(isNeList(__(V1, V2))) ->
            mark(and(isNeList(V1), isList(V2)))
          , active(isNePal(V)) -> mark(isQid(V))
          , active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P)))
          , active(isPal(V)) -> mark(isNePal(V))
          , active(isPal(nil())) -> mark(tt())
          , active(isQid(a())) -> mark(tt())
          , active(isQid(e())) -> mark(tt())
          , active(isQid(i())) -> mark(tt())
          , active(isQid(o())) -> mark(tt())
          , active(isQid(u())) -> mark(tt())
          , active(__(X1, X2)) -> __(active(X1), X2)
          , active(__(X1, X2)) -> __(X1, active(X2))
          , active(and(X1, X2)) -> and(active(X1), X2)
          , __(mark(X1), X2) -> mark(__(X1, X2))
          , __(X1, mark(X2)) -> mark(__(X1, X2))
          , and(mark(X1), X2) -> mark(and(X1, X2))
          , proper(__(X1, X2)) -> __(proper(X1), proper(X2))
          , proper(nil()) -> ok(nil())
          , proper(and(X1, X2)) -> and(proper(X1), proper(X2))
          , proper(tt()) -> ok(tt())
          , proper(isList(X)) -> isList(proper(X))
          , proper(isNeList(X)) -> isNeList(proper(X))
          , proper(isQid(X)) -> isQid(proper(X))
          , proper(isNePal(X)) -> isNePal(proper(X))
          , proper(isPal(X)) -> isPal(proper(X))
          , proper(a()) -> ok(a())
          , proper(e()) -> ok(e())
          , proper(i()) -> ok(i())
          , proper(o()) -> ok(o())
          , proper(u()) -> ok(u())
          , __(ok(X1), ok(X2)) -> ok(__(X1, X2))
          , and(ok(X1), ok(X2)) -> ok(and(X1, X2))
          , isList(ok(X)) -> ok(isList(X))
          , isNeList(ok(X)) -> ok(isNeList(X))
          , isQid(ok(X)) -> ok(isQid(X))
          , isNePal(ok(X)) -> ok(isNePal(X))
          , isPal(ok(X)) -> ok(isPal(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}
     
     Proof Output:    
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_1(2) -> 5
        , active_2(4) -> 6
        , ___0(2, 2) -> 1
        , ___1(2, 2) -> 3
        , mark_0(2) -> 2
        , mark_1(3) -> 1
        , mark_1(3) -> 3
        , nil_0() -> 2
        , nil_1() -> 4
        , and_0(2, 2) -> 1
        , and_1(2, 2) -> 3
        , tt_0() -> 2
        , tt_1() -> 4
        , isList_0(2) -> 1
        , isList_1(2) -> 3
        , isNeList_0(2) -> 1
        , isNeList_1(2) -> 3
        , isQid_0(2) -> 1
        , isQid_1(2) -> 3
        , isNePal_0(2) -> 1
        , isNePal_1(2) -> 3
        , isPal_0(2) -> 1
        , isPal_1(2) -> 3
        , a_0() -> 2
        , a_1() -> 4
        , e_0() -> 2
        , e_1() -> 4
        , i_0() -> 2
        , i_1() -> 4
        , o_0() -> 2
        , o_1() -> 4
        , u_0() -> 2
        , u_1() -> 4
        , proper_0(2) -> 1
        , proper_1(2) -> 5
        , ok_0(2) -> 2
        , ok_1(3) -> 1
        , ok_1(3) -> 3
        , ok_1(4) -> 1
        , ok_1(4) -> 5
        , top_0(2) -> 1
        , top_1(5) -> 1
        , top_2(6) -> 1}

Tool RC1

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 PALINDROME nokinds C

stdout:

YES(?,O(n^1))

Tool RC2

Execution TimeUnknown
Answer
YES(?,O(n^1))
InputTransformed CSR 04 PALINDROME nokinds C

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z)))
     , active(__(X, nil())) -> mark(X)
     , active(__(nil(), X)) -> mark(X)
     , active(and(tt(), X)) -> mark(X)
     , active(isList(V)) -> mark(isNeList(V))
     , active(isList(nil())) -> mark(tt())
     , active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2)))
     , active(isNeList(V)) -> mark(isQid(V))
     , active(isNeList(__(V1, V2))) ->
       mark(and(isList(V1), isNeList(V2)))
     , active(isNeList(__(V1, V2))) ->
       mark(and(isNeList(V1), isList(V2)))
     , active(isNePal(V)) -> mark(isQid(V))
     , active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P)))
     , active(isPal(V)) -> mark(isNePal(V))
     , active(isPal(nil())) -> mark(tt())
     , active(isQid(a())) -> mark(tt())
     , active(isQid(e())) -> mark(tt())
     , active(isQid(i())) -> mark(tt())
     , active(isQid(o())) -> mark(tt())
     , active(isQid(u())) -> mark(tt())
     , active(__(X1, X2)) -> __(active(X1), X2)
     , active(__(X1, X2)) -> __(X1, active(X2))
     , active(and(X1, X2)) -> and(active(X1), X2)
     , __(mark(X1), X2) -> mark(__(X1, X2))
     , __(X1, mark(X2)) -> mark(__(X1, X2))
     , and(mark(X1), X2) -> mark(and(X1, X2))
     , proper(__(X1, X2)) -> __(proper(X1), proper(X2))
     , proper(nil()) -> ok(nil())
     , proper(and(X1, X2)) -> and(proper(X1), proper(X2))
     , proper(tt()) -> ok(tt())
     , proper(isList(X)) -> isList(proper(X))
     , proper(isNeList(X)) -> isNeList(proper(X))
     , proper(isQid(X)) -> isQid(proper(X))
     , proper(isNePal(X)) -> isNePal(proper(X))
     , proper(isPal(X)) -> isPal(proper(X))
     , proper(a()) -> ok(a())
     , proper(e()) -> ok(e())
     , proper(i()) -> ok(i())
     , proper(o()) -> ok(o())
     , proper(u()) -> ok(u())
     , __(ok(X1), ok(X2)) -> ok(__(X1, X2))
     , and(ok(X1), ok(X2)) -> ok(and(X1, X2))
     , isList(ok(X)) -> ok(isList(X))
     , isNeList(ok(X)) -> ok(isNeList(X))
     , isQid(ok(X)) -> ok(isQid(X))
     , isNePal(ok(X)) -> ok(isNePal(X))
     , isPal(ok(X)) -> ok(isPal(X))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X))}

Proof Output:    
  'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
  
  Details:
  --------
    'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
     'Bounds with minimal-enrichment and initial automaton 'match''
     --------------------------------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z)))
          , active(__(X, nil())) -> mark(X)
          , active(__(nil(), X)) -> mark(X)
          , active(and(tt(), X)) -> mark(X)
          , active(isList(V)) -> mark(isNeList(V))
          , active(isList(nil())) -> mark(tt())
          , active(isList(__(V1, V2))) -> mark(and(isList(V1), isList(V2)))
          , active(isNeList(V)) -> mark(isQid(V))
          , active(isNeList(__(V1, V2))) ->
            mark(and(isList(V1), isNeList(V2)))
          , active(isNeList(__(V1, V2))) ->
            mark(and(isNeList(V1), isList(V2)))
          , active(isNePal(V)) -> mark(isQid(V))
          , active(isNePal(__(I, __(P, I)))) -> mark(and(isQid(I), isPal(P)))
          , active(isPal(V)) -> mark(isNePal(V))
          , active(isPal(nil())) -> mark(tt())
          , active(isQid(a())) -> mark(tt())
          , active(isQid(e())) -> mark(tt())
          , active(isQid(i())) -> mark(tt())
          , active(isQid(o())) -> mark(tt())
          , active(isQid(u())) -> mark(tt())
          , active(__(X1, X2)) -> __(active(X1), X2)
          , active(__(X1, X2)) -> __(X1, active(X2))
          , active(and(X1, X2)) -> and(active(X1), X2)
          , __(mark(X1), X2) -> mark(__(X1, X2))
          , __(X1, mark(X2)) -> mark(__(X1, X2))
          , and(mark(X1), X2) -> mark(and(X1, X2))
          , proper(__(X1, X2)) -> __(proper(X1), proper(X2))
          , proper(nil()) -> ok(nil())
          , proper(and(X1, X2)) -> and(proper(X1), proper(X2))
          , proper(tt()) -> ok(tt())
          , proper(isList(X)) -> isList(proper(X))
          , proper(isNeList(X)) -> isNeList(proper(X))
          , proper(isQid(X)) -> isQid(proper(X))
          , proper(isNePal(X)) -> isNePal(proper(X))
          , proper(isPal(X)) -> isPal(proper(X))
          , proper(a()) -> ok(a())
          , proper(e()) -> ok(e())
          , proper(i()) -> ok(i())
          , proper(o()) -> ok(o())
          , proper(u()) -> ok(u())
          , __(ok(X1), ok(X2)) -> ok(__(X1, X2))
          , and(ok(X1), ok(X2)) -> ok(and(X1, X2))
          , isList(ok(X)) -> ok(isList(X))
          , isNeList(ok(X)) -> ok(isNeList(X))
          , isQid(ok(X)) -> ok(isQid(X))
          , isNePal(ok(X)) -> ok(isNePal(X))
          , isPal(ok(X)) -> ok(isPal(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}
     
     Proof Output:    
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_1(2) -> 5
        , active_2(4) -> 6
        , ___0(2, 2) -> 1
        , ___1(2, 2) -> 3
        , mark_0(2) -> 2
        , mark_1(3) -> 1
        , mark_1(3) -> 3
        , nil_0() -> 2
        , nil_1() -> 4
        , and_0(2, 2) -> 1
        , and_1(2, 2) -> 3
        , tt_0() -> 2
        , tt_1() -> 4
        , isList_0(2) -> 1
        , isList_1(2) -> 3
        , isNeList_0(2) -> 1
        , isNeList_1(2) -> 3
        , isQid_0(2) -> 1
        , isQid_1(2) -> 3
        , isNePal_0(2) -> 1
        , isNePal_1(2) -> 3
        , isPal_0(2) -> 1
        , isPal_1(2) -> 3
        , a_0() -> 2
        , a_1() -> 4
        , e_0() -> 2
        , e_1() -> 4
        , i_0() -> 2
        , i_1() -> 4
        , o_0() -> 2
        , o_1() -> 4
        , u_0() -> 2
        , u_1() -> 4
        , proper_0(2) -> 1
        , proper_1(2) -> 5
        , ok_0(2) -> 2
        , ok_1(3) -> 1
        , ok_1(3) -> 3
        , ok_1(4) -> 1
        , ok_1(4) -> 5
        , top_0(2) -> 1
        , top_1(5) -> 1
        , top_2(6) -> 1}