YES

Problem:
 1024() -> 1024_1(0())
 1024_1(x) -> if(lt(x,10()),x)
 if(true(),x) -> double(1024_1(s(x)))
 if(false(),x) -> s(0())
 lt(0(),s(y)) -> true()
 lt(x,0()) -> false()
 lt(s(x),s(y)) -> lt(x,y)
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 10() -> double(s(double(s(s(0())))))

Proof:
 DP Processor:
  DPs:
   1024#() -> 1024_1#(0())
   1024_1#(x) -> 10#()
   1024_1#(x) -> lt#(x,10())
   1024_1#(x) -> if#(lt(x,10()),x)
   if#(true(),x) -> 1024_1#(s(x))
   if#(true(),x) -> double#(1024_1(s(x)))
   lt#(s(x),s(y)) -> lt#(x,y)
   double#(s(x)) -> double#(x)
   10#() -> double#(s(s(0())))
   10#() -> double#(s(double(s(s(0())))))
  TRS:
   1024() -> 1024_1(0())
   1024_1(x) -> if(lt(x,10()),x)
   if(true(),x) -> double(1024_1(s(x)))
   if(false(),x) -> s(0())
   lt(0(),s(y)) -> true()
   lt(x,0()) -> false()
   lt(s(x),s(y)) -> lt(x,y)
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   10() -> double(s(double(s(s(0())))))
  EDG Processor:
   DPs:
    1024#() -> 1024_1#(0())
    1024_1#(x) -> 10#()
    1024_1#(x) -> lt#(x,10())
    1024_1#(x) -> if#(lt(x,10()),x)
    if#(true(),x) -> 1024_1#(s(x))
    if#(true(),x) -> double#(1024_1(s(x)))
    lt#(s(x),s(y)) -> lt#(x,y)
    double#(s(x)) -> double#(x)
    10#() -> double#(s(s(0())))
    10#() -> double#(s(double(s(s(0())))))
   TRS:
    1024() -> 1024_1(0())
    1024_1(x) -> if(lt(x,10()),x)
    if(true(),x) -> double(1024_1(s(x)))
    if(false(),x) -> s(0())
    lt(0(),s(y)) -> true()
    lt(x,0()) -> false()
    lt(s(x),s(y)) -> lt(x,y)
    double(0()) -> 0()
    double(s(x)) -> s(s(double(x)))
    10() -> double(s(double(s(s(0())))))
   graph:
    double#(s(x)) -> double#(x) ->
    double#(s(x)) -> double#(x)
    if#(true(),x) -> double#(1024_1(s(x))) ->
    double#(s(x)) -> double#(x)
    if#(true(),x) -> 1024_1#(s(x)) -> 1024_1#(x) -> 10#()
    if#(true(),x) -> 1024_1#(s(x)) -> 1024_1#(x) -> lt#(x,10())
    if#(true(),x) -> 1024_1#(s(x)) -> 1024_1#(x) -> if#(lt(x,10()),x)
    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
    10#() -> double#(s(double(s(s(0()))))) ->
    double#(s(x)) -> double#(x)
    10#() -> double#(s(s(0()))) -> double#(s(x)) -> double#(x)
    1024_1#(x) -> if#(lt(x,10()),x) ->
    if#(true(),x) -> 1024_1#(s(x))
    1024_1#(x) -> if#(lt(x,10()),x) ->
    if#(true(),x) -> double#(1024_1(s(x)))
    1024_1#(x) -> lt#(x,10()) -> lt#(s(x),s(y)) -> lt#(x,y)
    1024_1#(x) -> 10#() -> 10#() -> double#(s(s(0())))
    1024_1#(x) -> 10#() -> 10#() -> double#(s(double(s(s(0())))))
    1024#() -> 1024_1#(0()) -> 1024_1#(x) -> 10#()
    1024#() -> 1024_1#(0()) -> 1024_1#(x) -> lt#(x,10())
    1024#() -> 1024_1#(0()) -> 1024_1#(x) -> if#(lt(x,10()),x)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 16/100
    DPs:
     if#(true(),x) -> 1024_1#(s(x))
     1024_1#(x) -> if#(lt(x,10()),x)
    TRS:
     1024() -> 1024_1(0())
     1024_1(x) -> if(lt(x,10()),x)
     if(true(),x) -> double(1024_1(s(x)))
     if(false(),x) -> s(0())
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     10() -> double(s(double(s(s(0())))))
    Bounds Processor:
     bound: 10
     enrichment: top-dp
     automaton:
      final states: {29}
      transitions:
       1024_1{#,9}(301) -> 29,18,16
       s9(322) -> 317*
       s9(317) -> 318*
       s9(324) -> 321*
       s9(319) -> 320*
       s9(314) -> 311*
       s9(309) -> 310*
       s9(279) -> 301*
       s9(326) -> 323*
       s9(321) -> 322*
       s9(316) -> 306*
       s9(311) -> 312*
       s9(323) -> 324*
       s9(318) -> 315*
       s9(313) -> 314*
       s9(308) -> 309*
       s9(325) -> 326*
       s9(320) -> 313*
       s9(315) -> 316*
       if{#,9}(307,301) -> 16,29,18
       lt9(17,326) -> 307*
       lt9(250,315) -> 307*
       lt9(301,306) -> 307*
       lt9(28,325) -> 307*
       lt9(23,325) -> 307*
       lt9(18,325) -> 307*
       lt9(99,324) -> 307*
       lt9(226,318) -> 307*
       lt9(130,321) -> 307*
       lt9(29,326) -> 307*
       lt9(24,326) -> 307*
       lt9(25,325) -> 307*
       lt9(20,325) -> 307*
       lt9(26,326) -> 307*
       lt9(21,326) -> 307*
       lt9(16,326) -> 307*
       lt9(158,322) -> 307*
       lt9(199,317) -> 307*
       lt9(27,325) -> 307*
       lt9(22,325) -> 307*
       lt9(17,325) -> 307*
       lt9(28,326) -> 307*
       lt9(23,326) -> 307*
       lt9(18,326) -> 307*
       lt9(59,323) -> 307*
       lt9(29,325) -> 307*
       lt9(24,325) -> 307*
       lt9(25,326) -> 307*
       lt9(20,326) -> 307*
       lt9(26,325) -> 307*
       lt9(279,316) -> 307*
       lt9(21,325) -> 307*
       lt9(16,325) -> 307*
       lt9(27,326) -> 307*
       lt9(22,326) -> 307*
       109() -> 306*
       double9(312) -> 306*
       double9(319) -> 325*
       double9(314) -> 317*
       double9(309) -> 313*
       double9(311) -> 315*
       double9(313) -> 321*
       double9(308) -> 319*
       double9(320) -> 323*
       double9(310) -> 311*
       09() -> 325,319,308
       false8() -> 281*
       true9() -> 307*
       1024_1{#,10}(327) -> 18,16,29
       s10(347) -> 348*
       s10(342) -> 337*
       s10(337) -> 338*
       s10(344) -> 339*
       s10(339) -> 340*
       s10(346) -> 343*
       s10(341) -> 342*
       s10(336) -> 328*
       s10(331) -> 332*
       s10(301) -> 327*
       s10(348) -> 345*
       s10(343) -> 344*
       s10(338) -> 333*
       s10(333) -> 334*
       s10(345) -> 346*
       s10(340) -> 335*
       s10(335) -> 336*
       s10(330) -> 331*
       false9() -> 307*
       if{#,10}(329,327) -> 29,18,16
       lt10(26,347) -> 329*
       lt10(21,347) -> 329*
       lt10(16,347) -> 329*
       lt10(158,343) -> 329*
       lt10(199,344) -> 329*
       lt10(301,336) -> 329*
       lt10(28,347) -> 329*
       lt10(23,347) -> 329*
       lt10(18,347) -> 329*
       lt10(59,348) -> 329*
       lt10(25,347) -> 329*
       lt10(20,347) -> 329*
       lt10(279,335) -> 329*
       lt10(27,347) -> 329*
       lt10(22,347) -> 329*
       lt10(17,347) -> 329*
       lt10(250,340) -> 329*
       lt10(327,328) -> 329*
       lt10(99,345) -> 329*
       lt10(226,339) -> 329*
       lt10(130,346) -> 329*
       lt10(29,347) -> 329*
       lt10(24,347) -> 329*
       1010() -> 328*
       double10(342) -> 345*
       double10(337) -> 343*
       double10(332) -> 333*
       double10(334) -> 328*
       double10(341) -> 347*
       double10(331) -> 337*
       double10(338) -> 339*
       double10(333) -> 335*
       double10(330) -> 341*
       010() -> 347,341,330
       if{#,0}(27,16) -> 16*
       if{#,0}(22,16) -> 16*
       if{#,0}(17,16) -> 16*
       if{#,0}(27,18) -> 16*
       if{#,0}(22,18) -> 16*
       if{#,0}(27,20) -> 16*
       if{#,0}(17,18) -> 16*
       if{#,0}(22,20) -> 16*
       if{#,0}(17,20) -> 16*
       if{#,0}(27,22) -> 16*
       if{#,0}(22,22) -> 16*
       if{#,0}(17,22) -> 16*
       if{#,0}(27,24) -> 16*
       if{#,0}(22,24) -> 16*
       if{#,0}(17,24) -> 16*
       if{#,0}(27,26) -> 16*
       if{#,0}(22,26) -> 16*
       if{#,0}(27,28) -> 16*
       if{#,0}(17,26) -> 16*
       if{#,0}(22,28) -> 16*
       if{#,0}(17,28) -> 16*
       if{#,0}(28,17) -> 16*
       if{#,0}(23,17) -> 16*
       if{#,0}(18,17) -> 16*
       if{#,0}(28,21) -> 16*
       if{#,0}(23,21) -> 16*
       if{#,0}(28,23) -> 16*
       if{#,0}(18,21) -> 16*
       if{#,0}(23,23) -> 16*
       if{#,0}(28,25) -> 16*
       if{#,0}(18,23) -> 16*
       if{#,0}(23,25) -> 16*
       if{#,0}(28,27) -> 16*
       if{#,0}(18,25) -> 16*
       if{#,0}(23,27) -> 16*
       if{#,0}(28,29) -> 16*
       if{#,0}(18,27) -> 16*
       if{#,0}(23,29) -> 16*
       if{#,0}(18,29) -> 16*
       if{#,0}(29,16) -> 16*
       if{#,0}(24,16) -> 16*
       if{#,0}(29,18) -> 16*
       if{#,0}(24,18) -> 16*
       if{#,0}(29,20) -> 16*
       if{#,0}(24,20) -> 16*
       if{#,0}(29,22) -> 16*
       if{#,0}(24,22) -> 16*
       if{#,0}(29,24) -> 16*
       if{#,0}(24,24) -> 16*
       if{#,0}(29,26) -> 16*
       if{#,0}(24,26) -> 16*
       if{#,0}(29,28) -> 16*
       if{#,0}(24,28) -> 16*
       if{#,0}(25,17) -> 16*
       if{#,0}(20,17) -> 18,16
       if{#,0}(25,21) -> 16*
       if{#,0}(20,21) -> 18,16
       if{#,0}(25,23) -> 16*
       if{#,0}(20,23) -> 18,16
       if{#,0}(25,25) -> 16*
       if{#,0}(20,25) -> 18,16
       if{#,0}(25,27) -> 16*
       if{#,0}(20,27) -> 18,16
       if{#,0}(25,29) -> 16*
       if{#,0}(20,29) -> 18,16
       if{#,0}(26,16) -> 16*
       if{#,0}(21,16) -> 16*
       if{#,0}(16,16) -> 16*
       if{#,0}(26,18) -> 16*
       if{#,0}(21,18) -> 16*
       if{#,0}(16,18) -> 16*
       if{#,0}(26,20) -> 16*
       if{#,0}(21,20) -> 16*
       if{#,0}(16,20) -> 16*
       if{#,0}(26,22) -> 16*
       if{#,0}(21,22) -> 16*
       if{#,0}(16,22) -> 16*
       if{#,0}(26,24) -> 16*
       if{#,0}(21,24) -> 16*
       if{#,0}(16,24) -> 16*
       if{#,0}(26,26) -> 16*
       if{#,0}(21,26) -> 16*
       if{#,0}(26,28) -> 16*
       if{#,0}(16,26) -> 16*
       if{#,0}(21,28) -> 16*
       if{#,0}(16,28) -> 16*
       if{#,0}(27,17) -> 16*
       if{#,0}(22,17) -> 16*
       if{#,0}(17,17) -> 16*
       if{#,0}(27,21) -> 16*
       if{#,0}(22,21) -> 16*
       if{#,0}(17,21) -> 16*
       if{#,0}(27,23) -> 16*
       if{#,0}(22,23) -> 16*
       if{#,0}(17,23) -> 16*
       if{#,0}(27,25) -> 16*
       if{#,0}(22,25) -> 16*
       if{#,0}(27,27) -> 16*
       if{#,0}(17,25) -> 16*
       if{#,0}(22,27) -> 16*
       if{#,0}(27,29) -> 16*
       if{#,0}(17,27) -> 16*
       if{#,0}(22,29) -> 16*
       if{#,0}(17,29) -> 16*
       if{#,0}(28,16) -> 16*
       if{#,0}(23,16) -> 16*
       if{#,0}(28,18) -> 16*
       if{#,0}(18,16) -> 16*
       if{#,0}(23,18) -> 16*
       if{#,0}(28,20) -> 16*
       if{#,0}(18,18) -> 16*
       if{#,0}(23,20) -> 16*
       if{#,0}(28,22) -> 16*
       if{#,0}(18,20) -> 16*
       if{#,0}(23,22) -> 16*
       if{#,0}(28,24) -> 16*
       if{#,0}(18,22) -> 16*
       if{#,0}(23,24) -> 16*
       if{#,0}(28,26) -> 16*
       if{#,0}(18,24) -> 16*
       if{#,0}(23,26) -> 16*
       if{#,0}(28,28) -> 16*
       if{#,0}(18,26) -> 16*
       if{#,0}(23,28) -> 16*
       if{#,0}(18,28) -> 16*
       if{#,0}(29,17) -> 16*
       if{#,0}(24,17) -> 16*
       if{#,0}(29,21) -> 16*
       if{#,0}(24,21) -> 16*
       if{#,0}(29,23) -> 16*
       if{#,0}(24,23) -> 16*
       if{#,0}(29,25) -> 16*
       if{#,0}(24,25) -> 16*
       if{#,0}(29,27) -> 16*
       if{#,0}(24,27) -> 16*
       if{#,0}(29,29) -> 16*
       if{#,0}(24,29) -> 16*
       if{#,0}(25,16) -> 16*
       if{#,0}(20,16) -> 18,16
       if{#,0}(25,18) -> 16*
       if{#,0}(20,18) -> 18,16
       if{#,0}(25,20) -> 16*
       if{#,0}(20,20) -> 18,16
       if{#,0}(25,22) -> 16*
       if{#,0}(20,22) -> 18,16
       if{#,0}(25,24) -> 16*
       if{#,0}(20,24) -> 18,16
       if{#,0}(25,26) -> 16*
       if{#,0}(20,26) -> 18,16
       if{#,0}(25,28) -> 16*
       if{#,0}(20,28) -> 29,16
       if{#,0}(26,17) -> 16*
       if{#,0}(21,17) -> 16*
       if{#,0}(16,17) -> 16*
       if{#,0}(26,21) -> 16*
       if{#,0}(21,21) -> 16*
       if{#,0}(16,21) -> 16*
       if{#,0}(26,23) -> 16*
       if{#,0}(21,23) -> 16*
       if{#,0}(16,23) -> 16*
       if{#,0}(26,25) -> 16*
       if{#,0}(21,25) -> 16*
       if{#,0}(16,25) -> 16*
       if{#,0}(26,27) -> 16*
       if{#,0}(21,27) -> 16*
       if{#,0}(26,29) -> 16*
       if{#,0}(16,27) -> 16*
       if{#,0}(21,29) -> 16*
       if{#,0}(16,29) -> 16*
       false10() -> 329*
       true0() -> 20,17
       1024_1{#,0}(25) -> 18*
       1024_1{#,0}(20) -> 18*
       1024_1{#,0}(27) -> 18*
       1024_1{#,0}(22) -> 18*
       1024_1{#,0}(17) -> 18*
       1024_1{#,0}(29) -> 18*
       1024_1{#,0}(24) -> 18*
       1024_1{#,0}(26) -> 18*
       1024_1{#,0}(21) -> 18*
       1024_1{#,0}(16) -> 18*
       1024_1{#,0}(28) -> 29*
       1024_1{#,0}(23) -> 18*
       1024_1{#,0}(18) -> 18*
       s0(25) -> 28*
       s0(20) -> 28*
       s0(27) -> 28*
       s0(22) -> 28*
       s0(17) -> 28*
       s0(29) -> 28*
       s0(24) -> 22,23,25,28
       s0(26) -> 28*
       s0(21) -> 28*
       s0(16) -> 28*
       s0(28) -> 22,23,25,21,26,28
       s0(23) -> 28*
       s0(18) -> 28*
       lt0(27,16) -> 20*
       lt0(22,16) -> 20*
       lt0(17,16) -> 20*
       lt0(27,18) -> 20*
       lt0(22,18) -> 20*
       lt0(27,20) -> 20*
       lt0(17,18) -> 20*
       lt0(22,20) -> 20*
       lt0(17,20) -> 20*
       lt0(27,22) -> 20*
       lt0(22,22) -> 20*
       lt0(17,22) -> 20*
       lt0(27,24) -> 20*
       lt0(22,24) -> 20*
       lt0(17,24) -> 20*
       lt0(27,26) -> 20*
       lt0(22,26) -> 20*
       lt0(27,28) -> 20*
       lt0(17,26) -> 20*
       lt0(22,28) -> 20*
       lt0(17,28) -> 20*
       lt0(28,17) -> 20*
       lt0(23,17) -> 20*
       lt0(18,17) -> 20*
       lt0(28,21) -> 20*
       lt0(23,21) -> 20*
       lt0(28,23) -> 20*
       lt0(18,21) -> 20*
       lt0(23,23) -> 20*
       lt0(28,25) -> 20*
       lt0(18,23) -> 20*
       lt0(23,25) -> 20*
       lt0(28,27) -> 20*
       lt0(18,25) -> 20*
       lt0(23,27) -> 20*
       lt0(28,29) -> 20*
       lt0(18,27) -> 20*
       lt0(23,29) -> 20*
       lt0(18,29) -> 20*
       lt0(29,16) -> 20*
       lt0(24,16) -> 20*
       lt0(29,18) -> 20*
       lt0(24,18) -> 20*
       lt0(29,20) -> 20*
       lt0(24,20) -> 20*
       lt0(29,22) -> 20*
       lt0(24,22) -> 20*
       lt0(29,24) -> 20*
       lt0(24,24) -> 20*
       lt0(29,26) -> 20*
       lt0(24,26) -> 20*
       lt0(29,28) -> 20*
       lt0(24,28) -> 20*
       lt0(25,17) -> 20*
       lt0(20,17) -> 20*
       lt0(25,21) -> 20*
       lt0(20,21) -> 20*
       lt0(25,23) -> 20*
       lt0(20,23) -> 20*
       lt0(25,25) -> 20*
       lt0(20,25) -> 20*
       lt0(25,27) -> 20*
       lt0(20,27) -> 20*
       lt0(25,29) -> 20*
       lt0(20,29) -> 20*
       lt0(26,16) -> 20*
       lt0(21,16) -> 20*
       lt0(16,16) -> 20*
       lt0(26,18) -> 20*
       lt0(21,18) -> 20*
       lt0(16,18) -> 20*
       lt0(26,20) -> 20*
       lt0(21,20) -> 20*
       lt0(16,20) -> 20*
       lt0(26,22) -> 20*
       lt0(21,22) -> 20*
       lt0(16,22) -> 20*
       lt0(26,24) -> 20*
       lt0(21,24) -> 20*
       lt0(16,24) -> 20*
       lt0(26,26) -> 20*
       lt0(21,26) -> 20*
       lt0(26,28) -> 20*
       lt0(16,26) -> 20*
       lt0(21,28) -> 20*
       lt0(16,28) -> 20*
       lt0(27,17) -> 20*
       lt0(22,17) -> 20*
       lt0(17,17) -> 20*
       lt0(27,21) -> 20*
       lt0(22,21) -> 20*
       lt0(17,21) -> 20*
       lt0(27,23) -> 20*
       lt0(22,23) -> 20*
       lt0(17,23) -> 20*
       lt0(27,25) -> 20*
       lt0(22,25) -> 20*
       lt0(27,27) -> 20*
       lt0(17,25) -> 20*
       lt0(22,27) -> 20*
       lt0(27,29) -> 20*
       lt0(17,27) -> 20*
       lt0(22,29) -> 20*
       lt0(17,29) -> 20*
       lt0(28,16) -> 20*
       lt0(23,16) -> 20*
       lt0(28,18) -> 20*
       lt0(18,16) -> 20*
       lt0(23,18) -> 20*
       lt0(28,20) -> 20*
       lt0(18,18) -> 20*
       lt0(23,20) -> 20*
       lt0(28,22) -> 20*
       lt0(18,20) -> 20*
       lt0(23,22) -> 20*
       lt0(28,24) -> 20*
       lt0(18,22) -> 20*
       lt0(23,24) -> 20*
       lt0(28,26) -> 20*
       lt0(18,24) -> 20*
       lt0(23,26) -> 20*
       lt0(28,28) -> 20*
       lt0(18,26) -> 20*
       lt0(23,28) -> 20*
       lt0(18,28) -> 20*
       lt0(29,17) -> 20*
       lt0(24,17) -> 20*
       lt0(29,21) -> 20*
       lt0(24,21) -> 20*
       lt0(29,23) -> 20*
       lt0(24,23) -> 20*
       lt0(29,25) -> 20*
       lt0(24,25) -> 20*
       lt0(29,27) -> 20*
       lt0(24,27) -> 20*
       lt0(29,29) -> 20*
       lt0(24,29) -> 20*
       lt0(25,16) -> 20*
       lt0(20,16) -> 20*
       lt0(25,18) -> 20*
       lt0(20,18) -> 20*
       lt0(25,20) -> 20*
       lt0(20,20) -> 20*
       lt0(25,22) -> 20*
       lt0(20,22) -> 20*
       lt0(25,24) -> 20*
       lt0(20,24) -> 20*
       lt0(25,26) -> 20*
       lt0(20,26) -> 20*
       lt0(25,28) -> 20*
       lt0(20,28) -> 20*
       lt0(26,17) -> 20*
       lt0(21,17) -> 20*
       lt0(16,17) -> 20*
       lt0(26,21) -> 20*
       lt0(21,21) -> 20*
       lt0(16,21) -> 20*
       lt0(26,23) -> 20*
       lt0(21,23) -> 20*
       lt0(16,23) -> 20*
       lt0(26,25) -> 20*
       lt0(21,25) -> 20*
       lt0(16,25) -> 20*
       lt0(26,27) -> 20*
       lt0(21,27) -> 20*
       lt0(26,29) -> 20*
       lt0(16,27) -> 20*
       lt0(21,29) -> 20*
       lt0(16,29) -> 20*
       100() -> 21*
       10240() -> 22*
       1024_10(25) -> 23*
       1024_10(20) -> 23*
       1024_10(27) -> 23*
       1024_10(22) -> 23*
       1024_10(17) -> 23*
       1024_10(29) -> 23*
       1024_10(24) -> 22,23
       1024_10(26) -> 23*
       1024_10(21) -> 23*
       1024_10(16) -> 23*
       1024_10(28) -> 23*
       1024_10(23) -> 23*
       1024_10(18) -> 23*
       00() -> 26,24
       if0(27,16) -> 25*
       if0(22,16) -> 25*
       if0(17,16) -> 25*
       if0(27,18) -> 25*
       if0(22,18) -> 25*
       if0(27,20) -> 25*
       if0(17,18) -> 25*
       if0(22,20) -> 25*
       if0(17,20) -> 25*
       if0(27,22) -> 25*
       if0(22,22) -> 25*
       if0(17,22) -> 25*
       if0(27,24) -> 25*
       if0(22,24) -> 25*
       if0(17,24) -> 25*
       if0(27,26) -> 25*
       if0(22,26) -> 25*
       if0(27,28) -> 25*
       if0(17,26) -> 25*
       if0(22,28) -> 25*
       if0(17,28) -> 25*
       if0(28,17) -> 25*
       if0(23,17) -> 25*
       if0(18,17) -> 25*
       if0(28,21) -> 25*
       if0(23,21) -> 25*
       if0(28,23) -> 25*
       if0(18,21) -> 25*
       if0(23,23) -> 25*
       if0(28,25) -> 25*
       if0(18,23) -> 25*
       if0(23,25) -> 25*
       if0(28,27) -> 25*
       if0(18,25) -> 25*
       if0(23,27) -> 25*
       if0(28,29) -> 25*
       if0(18,27) -> 25*
       if0(23,29) -> 25*
       if0(18,29) -> 25*
       if0(29,16) -> 25*
       if0(24,16) -> 25*
       if0(29,18) -> 25*
       if0(24,18) -> 25*
       if0(29,20) -> 25*
       if0(24,20) -> 25*
       if0(29,22) -> 25*
       if0(24,22) -> 25*
       if0(29,24) -> 25*
       if0(24,24) -> 25*
       if0(29,26) -> 25*
       if0(24,26) -> 25*
       if0(29,28) -> 25*
       if0(24,28) -> 25*
       if0(25,17) -> 25*
       if0(20,17) -> 23,25
       if0(25,21) -> 25*
       if0(20,21) -> 23,25
       if0(25,23) -> 25*
       if0(20,23) -> 23,25
       if0(25,25) -> 25*
       if0(20,25) -> 23,25
       if0(25,27) -> 25*
       if0(20,27) -> 23,25
       if0(25,29) -> 25*
       if0(20,29) -> 23,25
       if0(26,16) -> 25*
       if0(21,16) -> 25*
       if0(16,16) -> 25*
       if0(26,18) -> 25*
       if0(21,18) -> 25*
       if0(16,18) -> 25*
       if0(26,20) -> 25*
       if0(21,20) -> 25*
       if0(16,20) -> 25*
       if0(26,22) -> 25*
       if0(21,22) -> 25*
       if0(16,22) -> 25*
       if0(26,24) -> 25*
       if0(21,24) -> 25*
       if0(16,24) -> 25*
       if0(26,26) -> 25*
       if0(21,26) -> 25*
       if0(26,28) -> 25*
       if0(16,26) -> 25*
       if0(21,28) -> 25*
       if0(16,28) -> 25*
       if0(27,17) -> 25*
       if0(22,17) -> 25*
       if0(17,17) -> 25*
       if0(27,21) -> 25*
       if0(22,21) -> 25*
       if0(17,21) -> 25*
       if0(27,23) -> 25*
       if0(22,23) -> 25*
       if0(27,25) -> 25*
       if0(17,23) -> 25*
       if0(22,25) -> 25*
       if0(27,27) -> 25*
       if0(17,25) -> 25*
       if0(22,27) -> 25*
       if0(27,29) -> 25*
       if0(17,27) -> 25*
       if0(22,29) -> 25*
       if0(17,29) -> 25*
       if0(28,16) -> 25*
       if0(23,16) -> 25*
       if0(28,18) -> 25*
       if0(18,16) -> 25*
       if0(23,18) -> 25*
       if0(28,20) -> 25*
       if0(18,18) -> 25*
       if0(23,20) -> 25*
       if0(28,22) -> 25*
       if0(18,20) -> 25*
       if0(23,22) -> 25*
       if0(28,24) -> 25*
       if0(18,22) -> 25*
       if0(23,24) -> 25*
       if0(28,26) -> 25*
       if0(18,24) -> 25*
       if0(23,26) -> 25*
       if0(28,28) -> 25*
       if0(18,26) -> 25*
       if0(23,28) -> 25*
       if0(18,28) -> 25*
       if0(29,17) -> 25*
       if0(24,17) -> 25*
       if0(29,21) -> 25*
       if0(24,21) -> 25*
       if0(29,23) -> 25*
       if0(24,23) -> 25*
       if0(29,25) -> 25*
       if0(24,25) -> 25*
       if0(29,27) -> 25*
       if0(24,27) -> 25*
       if0(29,29) -> 25*
       if0(24,29) -> 25*
       if0(25,16) -> 25*
       if0(20,16) -> 23,25
       if0(25,18) -> 25*
       if0(20,18) -> 23,25
       if0(25,20) -> 25*
       if0(20,20) -> 23,25
       if0(25,22) -> 25*
       if0(20,22) -> 23,25
       if0(25,24) -> 25*
       if0(20,24) -> 22,23,25
       if0(25,26) -> 25*
       if0(20,26) -> 23,25
       if0(25,28) -> 25*
       if0(20,28) -> 23,25
       if0(26,17) -> 25*
       if0(21,17) -> 25*
       if0(16,17) -> 25*
       if0(26,21) -> 25*
       if0(21,21) -> 25*
       if0(16,21) -> 25*
       if0(26,23) -> 25*
       if0(21,23) -> 25*
       if0(16,23) -> 25*
       if0(26,25) -> 25*
       if0(21,25) -> 25*
       if0(16,25) -> 25*
       if0(26,27) -> 25*
       if0(21,27) -> 25*
       if0(26,29) -> 25*
       if0(16,27) -> 25*
       if0(21,29) -> 25*
       if0(16,29) -> 25*
       double0(25) -> 26*
       double0(20) -> 26*
       double0(27) -> 26*
       double0(22) -> 26*
       double0(17) -> 26*
       double0(29) -> 26*
       double0(24) -> 26*
       double0(26) -> 26*
       double0(21) -> 26*
       double0(16) -> 26*
       double0(28) -> 21,26
       double0(23) -> 22,23,25,26
       double0(18) -> 26*
       false0() -> 20,27
       1024_1{#,1}(59) -> 18,29,16
       s1(95) -> 96*
       s1(85) -> 86*
       s1(25) -> 59*
       s1(20) -> 59*
       s1(112) -> 105*
       s1(97) -> 98*
       s1(92) -> 75*
       s1(87) -> 88*
       s1(27) -> 59*
       s1(22) -> 59*
       s1(17) -> 59*
       s1(114) -> 111*
       s1(94) -> 87*
       s1(84) -> 85*
       s1(29) -> 59*
       s1(24) -> 59*
       s1(111) -> 112*
       s1(106) -> 95*
       s1(96) -> 91*
       s1(91) -> 92*
       s1(26) -> 59*
       s1(21) -> 59*
       s1(16) -> 59*
       s1(113) -> 114*
       s1(98) -> 93*
       s1(93) -> 94*
       s1(28) -> 59*
       s1(23) -> 59*
       s1(18) -> 59*
       s1(105) -> 106*
       if{#,1}(76,59) -> 29,18,16
       lt1(28,92) -> 76*
       lt1(22,111) -> 76*
       lt1(23,92) -> 76*
       lt1(17,111) -> 76*
       lt1(18,92) -> 76*
       lt1(28,96) -> 76*
       lt1(23,96) -> 76*
       lt1(18,96) -> 76*
       lt1(28,106) -> 76*
       lt1(23,106) -> 76*
       lt1(18,106) -> 76*
       lt1(26,114) -> 76*
       lt1(21,114) -> 76*
       lt1(29,91) -> 76*
       lt1(16,114) -> 76*
       lt1(24,91) -> 76*
       lt1(28,112) -> 76*
       lt1(23,112) -> 76*
       lt1(18,112) -> 76*
       lt1(29,95) -> 76*
       lt1(24,95) -> 76*
       lt1(29,105) -> 76*
       lt1(24,105) -> 76*
       lt1(27,113) -> 76*
       lt1(22,113) -> 76*
       lt1(17,113) -> 76*
       lt1(29,111) -> 76*
       lt1(24,111) -> 76*
       lt1(25,92) -> 76*
       lt1(20,92) -> 76*
       lt1(25,96) -> 76*
       lt1(20,96) -> 76*
       lt1(25,106) -> 76*
       lt1(20,106) -> 76*
       lt1(28,114) -> 76*
       lt1(23,114) -> 76*
       lt1(18,114) -> 76*
       lt1(26,91) -> 76*
       lt1(21,91) -> 76*
       lt1(25,112) -> 76*
       lt1(16,91) -> 76*
       lt1(20,112) -> 76*
       lt1(26,95) -> 76*
       lt1(21,95) -> 76*
       lt1(16,95) -> 76*
       lt1(26,105) -> 76*
       lt1(21,105) -> 76*
       lt1(16,105) -> 76*
       lt1(29,113) -> 76*
       lt1(24,113) -> 76*
       lt1(26,111) -> 76*
       lt1(27,92) -> 76*
       lt1(21,111) -> 76*
       lt1(22,92) -> 76*
       lt1(16,111) -> 76*
       lt1(17,92) -> 76*
       lt1(27,96) -> 76*
       lt1(22,96) -> 76*
       lt1(17,96) -> 76*
       lt1(27,106) -> 76*
       lt1(22,106) -> 76*
       lt1(17,106) -> 76*
       lt1(25,114) -> 76*
       lt1(20,114) -> 76*
       lt1(28,91) -> 76*
       lt1(23,91) -> 76*
       lt1(27,112) -> 76*
       lt1(18,91) -> 76*
       lt1(22,112) -> 76*
       lt1(17,112) -> 76*
       lt1(28,95) -> 76*
       lt1(23,95) -> 76*
       lt1(18,95) -> 76*
       lt1(28,105) -> 76*
       lt1(23,105) -> 76*
       lt1(18,105) -> 76*
       lt1(26,113) -> 76*
       lt1(21,113) -> 76*
       lt1(16,113) -> 76*
       lt1(28,111) -> 76*
       lt1(29,92) -> 76*
       lt1(23,111) -> 76*
       lt1(24,92) -> 76*
       lt1(18,111) -> 76*
       lt1(29,96) -> 76*
       lt1(24,96) -> 76*
       lt1(29,106) -> 76*
       lt1(24,106) -> 76*
       lt1(27,114) -> 76*
       lt1(22,114) -> 76*
       lt1(17,114) -> 76*
       lt1(25,91) -> 76*
       lt1(29,112) -> 76*
       lt1(20,91) -> 76*
       lt1(24,112) -> 76*
       lt1(25,95) -> 76*
       lt1(20,95) -> 76*
       lt1(25,105) -> 76*
       lt1(20,105) -> 76*
       lt1(28,113) -> 76*
       lt1(23,113) -> 76*
       lt1(18,113) -> 76*
       lt1(25,111) -> 76*
       lt1(26,92) -> 76*
       lt1(20,111) -> 76*
       lt1(21,92) -> 76*
       lt1(16,92) -> 76*
       lt1(26,96) -> 76*
       lt1(21,96) -> 76*
       lt1(16,96) -> 76*
       lt1(26,106) -> 76*
       lt1(21,106) -> 76*
       lt1(16,106) -> 76*
       lt1(29,114) -> 76*
       lt1(24,114) -> 76*
       lt1(27,91) -> 76*
       lt1(22,91) -> 76*
       lt1(26,112) -> 76*
       lt1(17,91) -> 76*
       lt1(21,112) -> 76*
       lt1(16,112) -> 76*
       lt1(27,95) -> 76*
       lt1(22,95) -> 76*
       lt1(17,95) -> 76*
       lt1(27,105) -> 76*
       lt1(22,105) -> 76*
       lt1(17,105) -> 76*
       lt1(25,113) -> 76*
       lt1(59,75) -> 76*
       lt1(20,113) -> 76*
       lt1(27,111) -> 76*
       101() -> 75*
       double1(85) -> 93*
       double1(97) -> 113*
       double1(87) -> 91*
       double1(94) -> 95*
       double1(84) -> 97*
       double1(86) -> 87*
       double1(98) -> 111*
       double1(93) -> 105*
       double1(88) -> 75*
       01() -> 113,97,84
       true1() -> 76*
       1024_1{#,2}(99) -> 16,29,18
       s2(132) -> 128*
       s2(127) -> 122*
       s2(122) -> 123*
       s2(129) -> 124*
       s2(124) -> 125*
       s2(59) -> 99*
       s2(136) -> 131*
       s2(131) -> 132*
       s2(126) -> 127*
       s2(121) -> 107*
       s2(116) -> 117*
       s2(128) -> 129*
       s2(123) -> 118*
       s2(118) -> 119*
       s2(135) -> 136*
       s2(125) -> 120*
       s2(120) -> 121*
       s2(115) -> 116*
       if{#,2}(108,99) -> 18,16,29
       lt2(29,136) -> 108*
       lt2(24,136) -> 108*
       lt2(25,125) -> 108*
       lt2(20,125) -> 108*
       lt2(25,129) -> 108*
       lt2(20,129) -> 108*
       lt2(25,131) -> 108*
       lt2(20,131) -> 108*
       lt2(25,135) -> 108*
       lt2(20,135) -> 108*
       lt2(99,107) -> 108*
       lt2(26,120) -> 108*
       lt2(21,120) -> 108*
       lt2(16,120) -> 108*
       lt2(26,124) -> 108*
       lt2(21,124) -> 108*
       lt2(16,124) -> 108*
       lt2(26,128) -> 108*
       lt2(21,128) -> 108*
       lt2(16,128) -> 108*
       lt2(26,132) -> 108*
       lt2(21,132) -> 108*
       lt2(16,132) -> 108*
       lt2(26,136) -> 108*
       lt2(21,136) -> 108*
       lt2(16,136) -> 108*
       lt2(27,125) -> 108*
       lt2(22,125) -> 108*
       lt2(17,125) -> 108*
       lt2(27,129) -> 108*
       lt2(22,129) -> 108*
       lt2(27,131) -> 108*
       lt2(17,129) -> 108*
       lt2(22,131) -> 108*
       lt2(17,131) -> 108*
       lt2(27,135) -> 108*
       lt2(22,135) -> 108*
       lt2(17,135) -> 108*
       lt2(28,120) -> 108*
       lt2(23,120) -> 108*
       lt2(18,120) -> 108*
       lt2(28,124) -> 108*
       lt2(23,124) -> 108*
       lt2(18,124) -> 108*
       lt2(28,128) -> 108*
       lt2(23,128) -> 108*
       lt2(18,128) -> 108*
       lt2(28,132) -> 108*
       lt2(23,132) -> 108*
       lt2(18,132) -> 108*
       lt2(59,121) -> 108*
       lt2(28,136) -> 108*
       lt2(23,136) -> 108*
       lt2(18,136) -> 108*
       lt2(29,125) -> 108*
       lt2(24,125) -> 108*
       lt2(29,129) -> 108*
       lt2(24,129) -> 108*
       lt2(29,131) -> 108*
       lt2(24,131) -> 108*
       lt2(29,135) -> 108*
       lt2(24,135) -> 108*
       lt2(25,120) -> 108*
       lt2(20,120) -> 108*
       lt2(25,124) -> 108*
       lt2(20,124) -> 108*
       lt2(25,128) -> 108*
       lt2(20,128) -> 108*
       lt2(25,132) -> 108*
       lt2(20,132) -> 108*
       lt2(25,136) -> 108*
       lt2(20,136) -> 108*
       lt2(26,125) -> 108*
       lt2(21,125) -> 108*
       lt2(16,125) -> 108*
       lt2(26,129) -> 108*
       lt2(21,129) -> 108*
       lt2(26,131) -> 108*
       lt2(16,129) -> 108*
       lt2(21,131) -> 108*
       lt2(16,131) -> 108*
       lt2(26,135) -> 108*
       lt2(21,135) -> 108*
       lt2(16,135) -> 108*
       lt2(27,120) -> 108*
       lt2(22,120) -> 108*
       lt2(17,120) -> 108*
       lt2(27,124) -> 108*
       lt2(22,124) -> 108*
       lt2(17,124) -> 108*
       lt2(27,128) -> 108*
       lt2(22,128) -> 108*
       lt2(17,128) -> 108*
       lt2(27,132) -> 108*
       lt2(22,132) -> 108*
       lt2(17,132) -> 108*
       lt2(27,136) -> 108*
       lt2(22,136) -> 108*
       lt2(17,136) -> 108*
       lt2(28,125) -> 108*
       lt2(23,125) -> 108*
       lt2(18,125) -> 108*
       lt2(28,129) -> 108*
       lt2(23,129) -> 108*
       lt2(28,131) -> 108*
       lt2(18,129) -> 108*
       lt2(23,131) -> 108*
       lt2(18,131) -> 108*
       lt2(28,135) -> 108*
       lt2(23,135) -> 108*
       lt2(18,135) -> 108*
       lt2(29,120) -> 108*
       lt2(24,120) -> 108*
       lt2(29,124) -> 108*
       lt2(24,124) -> 108*
       lt2(29,128) -> 108*
       lt2(24,128) -> 108*
       lt2(29,132) -> 108*
       lt2(24,132) -> 108*
       102() -> 107*
       double2(127) -> 131*
       double2(122) -> 128*
       double2(117) -> 118*
       double2(119) -> 107*
       double2(126) -> 135*
       double2(116) -> 122*
       double2(123) -> 124*
       double2(118) -> 120*
       double2(115) -> 126*
       02() -> 135,126,115
       true2() -> 108*
       1024_1{#,3}(130) -> 29,18,16
       s3(167) -> 156*
       s3(157) -> 154*
       s3(147) -> 142*
       s3(142) -> 143*
       s3(137) -> 138*
       s3(154) -> 155*
       s3(149) -> 144*
       s3(144) -> 145*
       s3(99) -> 130*
       s3(166) -> 167*
       s3(156) -> 157*
       s3(146) -> 147*
       s3(148) -> 149*
       s3(143) -> 133*
       s3(138) -> 139*
       s3(155) -> 146*
       s3(145) -> 140*
       s3(140) -> 141*
       if{#,3}(134,130) -> 16,29,18
       lt3(28,155) -> 134*
       lt3(59,142) -> 134*
       lt3(23,155) -> 134*
       lt3(28,157) -> 134*
       lt3(18,155) -> 134*
       lt3(23,157) -> 134*
       lt3(18,157) -> 134*
       lt3(29,146) -> 134*
       lt3(24,146) -> 134*
       lt3(28,167) -> 134*
       lt3(23,167) -> 134*
       lt3(18,167) -> 134*
       lt3(29,154) -> 134*
       lt3(24,154) -> 134*
       lt3(29,156) -> 134*
       lt3(24,156) -> 134*
       lt3(29,166) -> 134*
       lt3(24,166) -> 134*
       lt3(25,147) -> 134*
       lt3(20,147) -> 134*
       lt3(25,155) -> 134*
       lt3(20,155) -> 134*
       lt3(25,157) -> 134*
       lt3(20,157) -> 134*
       lt3(26,146) -> 134*
       lt3(21,146) -> 134*
       lt3(25,167) -> 134*
       lt3(16,146) -> 134*
       lt3(20,167) -> 134*
       lt3(26,154) -> 134*
       lt3(21,154) -> 134*
       lt3(26,156) -> 134*
       lt3(16,154) -> 134*
       lt3(21,156) -> 134*
       lt3(16,156) -> 134*
       lt3(26,166) -> 134*
       lt3(27,147) -> 134*
       lt3(21,166) -> 134*
       lt3(22,147) -> 134*
       lt3(16,166) -> 134*
       lt3(17,147) -> 134*
       lt3(27,155) -> 134*
       lt3(22,155) -> 134*
       lt3(27,157) -> 134*
       lt3(17,155) -> 134*
       lt3(22,157) -> 134*
       lt3(17,157) -> 134*
       lt3(28,146) -> 134*
       lt3(23,146) -> 134*
       lt3(27,167) -> 134*
       lt3(18,146) -> 134*
       lt3(22,167) -> 134*
       lt3(99,143) -> 134*
       lt3(17,167) -> 134*
       lt3(28,154) -> 134*
       lt3(23,154) -> 134*
       lt3(28,156) -> 134*
       lt3(18,154) -> 134*
       lt3(23,156) -> 134*
       lt3(18,156) -> 134*
       lt3(28,166) -> 134*
       lt3(29,147) -> 134*
       lt3(23,166) -> 134*
       lt3(24,147) -> 134*
       lt3(18,166) -> 134*
       lt3(29,155) -> 134*
       lt3(24,155) -> 134*
       lt3(29,157) -> 134*
       lt3(24,157) -> 134*
       lt3(25,146) -> 134*
       lt3(29,167) -> 134*
       lt3(20,146) -> 134*
       lt3(24,167) -> 134*
       lt3(25,154) -> 134*
       lt3(20,154) -> 134*
       lt3(25,156) -> 134*
       lt3(20,156) -> 134*
       lt3(25,166) -> 134*
       lt3(26,147) -> 134*
       lt3(20,166) -> 134*
       lt3(21,147) -> 134*
       lt3(16,147) -> 134*
       lt3(26,155) -> 134*
       lt3(21,155) -> 134*
       lt3(26,157) -> 134*
       lt3(16,155) -> 134*
       lt3(21,157) -> 134*
       lt3(16,157) -> 134*
       lt3(27,146) -> 134*
       lt3(22,146) -> 134*
       lt3(26,167) -> 134*
       lt3(17,146) -> 134*
       lt3(21,167) -> 134*
       lt3(16,167) -> 134*
       lt3(27,154) -> 134*
       lt3(22,154) -> 134*
       lt3(27,156) -> 134*
       lt3(17,154) -> 134*
       lt3(22,156) -> 134*
       lt3(17,156) -> 134*
       lt3(27,166) -> 134*
       lt3(28,147) -> 134*
       lt3(22,166) -> 134*
       lt3(23,147) -> 134*
       lt3(17,166) -> 134*
       lt3(18,147) -> 134*
       lt3(130,133) -> 134*
       103() -> 133*
       double3(137) -> 148*
       double3(149) -> 156*
       double3(144) -> 154*
       double3(139) -> 140*
       double3(141) -> 133*
       double3(148) -> 166*
       double3(138) -> 144*
       double3(145) -> 146*
       double3(140) -> 142*
       03() -> 166,148,137
       false1() -> 76*
       true3() -> 134*
       1024_1{#,4}(158) -> 18,16,29
       s4(197) -> 198*
       s4(187) -> 188*
       s4(182) -> 168*
       s4(172) -> 173*
       s4(189) -> 190*
       s4(184) -> 175*
       s4(196) -> 189*
       s4(186) -> 181*
       s4(181) -> 182*
       s4(198) -> 195*
       s4(188) -> 183*
       s4(183) -> 184*
       s4(173) -> 174*
       s4(195) -> 196*
       s4(190) -> 185*
       s4(185) -> 186*
       s4(175) -> 176*
       s4(130) -> 158*
       false2() -> 108*
       if{#,4}(169,158) -> 29,18,16
       lt4(26,195) -> 169*
       lt4(21,195) -> 169*
       lt4(26,197) -> 169*
       lt4(16,195) -> 169*
       lt4(21,197) -> 169*
       lt4(16,197) -> 169*
       lt4(27,190) -> 169*
       lt4(22,190) -> 169*
       lt4(17,190) -> 169*
       lt4(27,196) -> 169*
       lt4(22,196) -> 169*
       lt4(27,198) -> 169*
       lt4(17,196) -> 169*
       lt4(22,198) -> 169*
       lt4(17,198) -> 169*
       lt4(28,185) -> 169*
       lt4(23,185) -> 169*
       lt4(18,185) -> 169*
       lt4(28,189) -> 169*
       lt4(23,189) -> 169*
       lt4(18,189) -> 169*
       lt4(28,195) -> 169*
       lt4(23,195) -> 169*
       lt4(28,197) -> 169*
       lt4(18,195) -> 169*
       lt4(23,197) -> 169*
       lt4(18,197) -> 169*
       lt4(59,186) -> 169*
       lt4(29,190) -> 169*
       lt4(24,190) -> 169*
       lt4(29,196) -> 169*
       lt4(24,196) -> 169*
       lt4(29,198) -> 169*
       lt4(24,198) -> 169*
       lt4(25,185) -> 169*
       lt4(20,185) -> 169*
       lt4(25,189) -> 169*
       lt4(20,189) -> 169*
       lt4(25,195) -> 169*
       lt4(20,195) -> 169*
       lt4(25,197) -> 169*
       lt4(20,197) -> 169*
       lt4(158,168) -> 169*
       lt4(26,190) -> 169*
       lt4(21,190) -> 169*
       lt4(16,190) -> 169*
       lt4(26,196) -> 169*
       lt4(21,196) -> 169*
       lt4(26,198) -> 169*
       lt4(16,196) -> 169*
       lt4(21,198) -> 169*
       lt4(16,198) -> 169*
       lt4(27,185) -> 169*
       lt4(22,185) -> 169*
       lt4(17,185) -> 169*
       lt4(27,189) -> 169*
       lt4(22,189) -> 169*
       lt4(17,189) -> 169*
       lt4(27,195) -> 169*
       lt4(22,195) -> 169*
       lt4(27,197) -> 169*
       lt4(17,195) -> 169*
       lt4(22,197) -> 169*
       lt4(17,197) -> 169*
       lt4(99,181) -> 169*
       lt4(28,190) -> 169*
       lt4(23,190) -> 169*
       lt4(18,190) -> 169*
       lt4(28,196) -> 169*
       lt4(23,196) -> 169*
       lt4(28,198) -> 169*
       lt4(18,196) -> 169*
       lt4(23,198) -> 169*
       lt4(18,198) -> 169*
       lt4(130,182) -> 169*
       lt4(29,185) -> 169*
       lt4(24,185) -> 169*
       lt4(29,189) -> 169*
       lt4(24,189) -> 169*
       lt4(29,195) -> 169*
       lt4(24,195) -> 169*
       lt4(29,197) -> 169*
       lt4(24,197) -> 169*
       lt4(25,190) -> 169*
       lt4(20,190) -> 169*
       lt4(25,196) -> 169*
       lt4(20,196) -> 169*
       lt4(25,198) -> 169*
       lt4(20,198) -> 169*
       lt4(26,185) -> 169*
       lt4(21,185) -> 169*
       lt4(16,185) -> 169*
       lt4(26,189) -> 169*
       lt4(21,189) -> 169*
       lt4(16,189) -> 169*
       104() -> 168*
       double4(187) -> 197*
       double4(172) -> 187*
       double4(184) -> 185*
       double4(174) -> 175*
       double4(176) -> 168*
       double4(188) -> 195*
       double4(183) -> 189*
       double4(173) -> 183*
       double4(175) -> 181*
       04() -> 197,187,172
       false3() -> 134*
       true4() -> 169*
       1024_1{#,5}(199) -> 16,29,18
       s5(222) -> 223*
       s5(217) -> 212*
       s5(212) -> 213*
       s5(207) -> 208*
       s5(224) -> 225*
       s5(219) -> 214*
       s5(214) -> 215*
       s5(221) -> 216*
       s5(216) -> 217*
       s5(223) -> 220*
       s5(218) -> 219*
       s5(213) -> 200*
       s5(208) -> 209*
       s5(158) -> 199*
       s5(225) -> 222*
       s5(220) -> 221*
       s5(215) -> 210*
       s5(210) -> 211*
       if{#,5}(201,199) -> 18,16,29
       lt5(25,220) -> 201*
       lt5(20,220) -> 201*
       lt5(25,222) -> 201*
       lt5(20,222) -> 201*
       lt5(25,224) -> 201*
       lt5(20,224) -> 201*
       lt5(26,221) -> 201*
       lt5(21,221) -> 201*
       lt5(26,223) -> 201*
       lt5(16,221) -> 201*
       lt5(21,223) -> 201*
       lt5(26,225) -> 201*
       lt5(16,223) -> 201*
       lt5(199,200) -> 201*
       lt5(21,225) -> 201*
       lt5(158,213) -> 201*
       lt5(16,225) -> 201*
       lt5(27,220) -> 201*
       lt5(22,220) -> 201*
       lt5(27,222) -> 201*
       lt5(17,220) -> 201*
       lt5(22,222) -> 201*
       lt5(27,224) -> 201*
       lt5(17,222) -> 201*
       lt5(22,224) -> 201*
       lt5(17,224) -> 201*
       lt5(28,221) -> 201*
       lt5(23,221) -> 201*
       lt5(28,223) -> 201*
       lt5(18,221) -> 201*
       lt5(23,223) -> 201*
       lt5(28,225) -> 201*
       lt5(18,223) -> 201*
       lt5(23,225) -> 201*
       lt5(18,225) -> 201*
       lt5(59,216) -> 201*
       lt5(29,220) -> 201*
       lt5(24,220) -> 201*
       lt5(29,222) -> 201*
       lt5(24,222) -> 201*
       lt5(29,224) -> 201*
       lt5(24,224) -> 201*
       lt5(25,221) -> 201*
       lt5(20,221) -> 201*
       lt5(25,223) -> 201*
       lt5(20,223) -> 201*
       lt5(25,225) -> 201*
       lt5(20,225) -> 201*
       lt5(26,220) -> 201*
       lt5(21,220) -> 201*
       lt5(26,222) -> 201*
       lt5(16,220) -> 201*
       lt5(21,222) -> 201*
       lt5(26,224) -> 201*
       lt5(16,222) -> 201*
       lt5(21,224) -> 201*
       lt5(16,224) -> 201*
       lt5(27,221) -> 201*
       lt5(22,221) -> 201*
       lt5(27,223) -> 201*
       lt5(17,221) -> 201*
       lt5(22,223) -> 201*
       lt5(27,225) -> 201*
       lt5(17,223) -> 201*
       lt5(22,225) -> 201*
       lt5(17,225) -> 201*
       lt5(28,220) -> 201*
       lt5(23,220) -> 201*
       lt5(28,222) -> 201*
       lt5(18,220) -> 201*
       lt5(99,217) -> 201*
       lt5(23,222) -> 201*
       lt5(28,224) -> 201*
       lt5(18,222) -> 201*
       lt5(23,224) -> 201*
       lt5(18,224) -> 201*
       lt5(130,212) -> 201*
       lt5(29,221) -> 201*
       lt5(24,221) -> 201*
       lt5(29,223) -> 201*
       lt5(24,223) -> 201*
       lt5(29,225) -> 201*
       lt5(24,225) -> 201*
       105() -> 200*
       double5(207) -> 218*
       double5(219) -> 222*
       double5(214) -> 220*
       double5(209) -> 210*
       double5(211) -> 200*
       double5(218) -> 224*
       double5(208) -> 214*
       double5(215) -> 216*
       double5(210) -> 212*
       05() -> 224,218,207
       false4() -> 169*
       true5() -> 201*
       1024_1{#,6}(226) -> 29,18,16
       s6(247) -> 244*
       s6(242) -> 243*
       s6(237) -> 227*
       s6(232) -> 233*
       s6(249) -> 246*
       s6(244) -> 245*
       s6(239) -> 232*
       s6(229) -> 230*
       s6(199) -> 226*
       s6(246) -> 247*
       s6(241) -> 238*
       s6(236) -> 237*
       s6(248) -> 249*
       s6(243) -> 236*
       s6(238) -> 239*
       s6(245) -> 242*
       s6(240) -> 241*
       s6(230) -> 231*
       if{#,6}(228,226) -> 16,29,18
       lt6(27,247) -> 228*
       lt6(22,247) -> 228*
       lt6(27,249) -> 228*
       lt6(17,247) -> 228*
       lt6(22,249) -> 228*
       lt6(17,249) -> 228*
       lt6(28,244) -> 228*
       lt6(23,244) -> 228*
       lt6(28,246) -> 228*
       lt6(18,244) -> 228*
       lt6(23,246) -> 228*
       lt6(28,248) -> 228*
       lt6(18,246) -> 228*
       lt6(23,248) -> 228*
       lt6(18,248) -> 228*
       lt6(59,245) -> 228*
       lt6(29,247) -> 228*
       lt6(24,247) -> 228*
       lt6(29,249) -> 228*
       lt6(24,249) -> 228*
       lt6(25,244) -> 228*
       lt6(20,244) -> 228*
       lt6(25,246) -> 228*
       lt6(20,246) -> 228*
       lt6(25,248) -> 228*
       lt6(20,248) -> 228*
       lt6(26,247) -> 228*
       lt6(21,247) -> 228*
       lt6(26,249) -> 228*
       lt6(16,247) -> 228*
       lt6(21,249) -> 228*
       lt6(16,249) -> 228*
       lt6(99,242) -> 228*
       lt6(27,244) -> 228*
       lt6(22,244) -> 228*
       lt6(27,246) -> 228*
       lt6(17,244) -> 228*
       lt6(22,246) -> 228*
       lt6(27,248) -> 228*
       lt6(17,246) -> 228*
       lt6(22,248) -> 228*
       lt6(17,248) -> 228*
       lt6(28,247) -> 228*
       lt6(23,247) -> 228*
       lt6(28,249) -> 228*
       lt6(18,247) -> 228*
       lt6(23,249) -> 228*
       lt6(18,249) -> 228*
       lt6(130,243) -> 228*
       lt6(29,244) -> 228*
       lt6(24,244) -> 228*
       lt6(29,246) -> 228*
       lt6(24,246) -> 228*
       lt6(29,248) -> 228*
       lt6(24,248) -> 228*
       lt6(158,236) -> 228*
       lt6(25,247) -> 228*
       lt6(199,237) -> 228*
       lt6(20,247) -> 228*
       lt6(25,249) -> 228*
       lt6(20,249) -> 228*
       lt6(26,244) -> 228*
       lt6(21,244) -> 228*
       lt6(26,246) -> 228*
       lt6(16,244) -> 228*
       lt6(21,246) -> 228*
       lt6(26,248) -> 228*
       lt6(16,246) -> 228*
       lt6(21,248) -> 228*
       lt6(16,248) -> 228*
       lt6(226,227) -> 228*
       106() -> 227*
       double6(232) -> 236*
       double6(239) -> 242*
       double6(229) -> 240*
       double6(241) -> 246*
       double6(231) -> 232*
       double6(238) -> 244*
       double6(233) -> 227*
       double6(240) -> 248*
       double6(230) -> 238*
       06() -> 248,240,229
       false5() -> 201*
       true6() -> 228*
       1024_1{#,7}(250) -> 18,16,29
       s7(277) -> 278*
       s7(267) -> 258*
       s7(274) -> 264*
       s7(264) -> 265*
       s7(259) -> 256*
       s7(254) -> 255*
       s7(276) -> 273*
       s7(266) -> 267*
       s7(261) -> 251*
       s7(256) -> 257*
       s7(226) -> 250*
       s7(278) -> 275*
       s7(273) -> 274*
       s7(258) -> 259*
       s7(253) -> 254*
       s7(275) -> 276*
       s7(265) -> 260*
       s7(260) -> 261*
       if{#,7}(252,250) -> 29,18,16
       lt7(25,275) -> 252*
       lt7(20,275) -> 252*
       lt7(25,277) -> 252*
       lt7(20,277) -> 252*
       lt7(26,276) -> 252*
       lt7(21,276) -> 252*
       lt7(26,278) -> 252*
       lt7(16,276) -> 252*
       lt7(21,278) -> 252*
       lt7(16,278) -> 252*
       lt7(27,275) -> 252*
       lt7(22,275) -> 252*
       lt7(27,277) -> 252*
       lt7(17,275) -> 252*
       lt7(22,277) -> 252*
       lt7(17,277) -> 252*
       lt7(28,276) -> 252*
       lt7(23,276) -> 252*
       lt7(28,278) -> 252*
       lt7(18,276) -> 252*
       lt7(23,278) -> 252*
       lt7(18,278) -> 252*
       lt7(226,261) -> 252*
       lt7(130,264) -> 252*
       lt7(59,273) -> 252*
       lt7(29,275) -> 252*
       lt7(24,275) -> 252*
       lt7(29,277) -> 252*
       lt7(24,277) -> 252*
       lt7(25,276) -> 252*
       lt7(20,276) -> 252*
       lt7(25,278) -> 252*
       lt7(20,278) -> 252*
       lt7(26,275) -> 252*
       lt7(21,275) -> 252*
       lt7(26,277) -> 252*
       lt7(16,275) -> 252*
       lt7(21,277) -> 252*
       lt7(158,265) -> 252*
       lt7(16,277) -> 252*
       lt7(199,260) -> 252*
       lt7(250,251) -> 252*
       lt7(27,276) -> 252*
       lt7(22,276) -> 252*
       lt7(27,278) -> 252*
       lt7(17,276) -> 252*
       lt7(22,278) -> 252*
       lt7(17,278) -> 252*
       lt7(28,275) -> 252*
       lt7(23,275) -> 252*
       lt7(28,277) -> 252*
       lt7(18,275) -> 252*
       lt7(23,277) -> 252*
       lt7(18,277) -> 252*
       lt7(99,274) -> 252*
       lt7(29,276) -> 252*
       lt7(24,276) -> 252*
       lt7(29,278) -> 252*
       lt7(24,278) -> 252*
       107() -> 251*
       double7(267) -> 275*
       double7(257) -> 251*
       double7(259) -> 264*
       double7(254) -> 258*
       double7(266) -> 277*
       double7(256) -> 260*
       double7(258) -> 273*
       double7(253) -> 266*
       double7(255) -> 256*
       07() -> 277,266,253
       false6() -> 228*
       true7() -> 252*
       1024_1{#,8}(279) -> 16,29,18
       s8(297) -> 298*
       s8(292) -> 287*
       s8(287) -> 288*
       s8(282) -> 283*
       s8(299) -> 300*
       s8(294) -> 289*
       s8(289) -> 290*
       s8(296) -> 291*
       s8(291) -> 292*
       s8(298) -> 295*
       s8(293) -> 294*
       s8(288) -> 280*
       s8(283) -> 284*
       s8(300) -> 297*
       s8(295) -> 296*
       s8(290) -> 285*
       s8(285) -> 286*
       s8(250) -> 279*
       if{#,8}(281,279) -> 18,16,29
       lt8(59,298) -> 281*
       lt8(29,300) -> 281*
       lt8(24,300) -> 281*
       lt8(25,297) -> 281*
       lt8(20,297) -> 281*
       lt8(25,299) -> 281*
       lt8(20,299) -> 281*
       lt8(26,300) -> 281*
       lt8(21,300) -> 281*
       lt8(16,300) -> 281*
       lt8(27,297) -> 281*
       lt8(22,297) -> 281*
       lt8(27,299) -> 281*
       lt8(17,297) -> 281*
       lt8(22,299) -> 281*
       lt8(17,299) -> 281*
       lt8(250,288) -> 281*
       lt8(28,300) -> 281*
       lt8(99,295) -> 281*
       lt8(23,300) -> 281*
       lt8(18,300) -> 281*
       lt8(226,287) -> 281*
       lt8(130,296) -> 281*
       lt8(29,297) -> 281*
       lt8(24,297) -> 281*
       lt8(29,299) -> 281*
       lt8(24,299) -> 281*
       lt8(25,300) -> 281*
       lt8(20,300) -> 281*
       lt8(279,280) -> 281*
       lt8(26,297) -> 281*
       lt8(21,297) -> 281*
       lt8(26,299) -> 281*
       lt8(16,297) -> 281*
       lt8(21,299) -> 281*
       lt8(16,299) -> 281*
       lt8(158,291) -> 281*
       lt8(199,292) -> 281*
       lt8(27,300) -> 281*
       lt8(22,300) -> 281*
       lt8(17,300) -> 281*
       lt8(28,297) -> 281*
       lt8(23,297) -> 281*
       lt8(28,299) -> 281*
       lt8(18,297) -> 281*
       lt8(23,299) -> 281*
       lt8(18,299) -> 281*
       108() -> 280*
       double8(282) -> 293*
       double8(294) -> 297*
       double8(289) -> 295*
       double8(284) -> 285*
       double8(286) -> 280*
       double8(293) -> 299*
       double8(283) -> 289*
       double8(290) -> 291*
       double8(285) -> 287*
       08() -> 299,293,282
       false7() -> 252*
       true8() -> 281*
     problem:
      DPs:
       1024_1#(x) -> if#(lt(x,10()),x)
      TRS:
       1024() -> 1024_1(0())
       1024_1(x) -> if(lt(x,10()),x)
       if(true(),x) -> double(1024_1(s(x)))
       if(false(),x) -> s(0())
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       10() -> double(s(double(s(s(0())))))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [if#](x0, x1) = 0,
       
       [1024_1#](x0) = 1,
       
       [false] = 0,
       
       [double](x0) = 0,
       
       [s](x0) = 0,
       
       [true] = 0,
       
       [if](x0, x1) = 0,
       
       [lt](x0, x1) = 0,
       
       [10] = 0,
       
       [1024_1](x0) = 0,
       
       [0] = 0,
       
       [1024] = 0
      orientation:
       1024_1#(x) = 1 >= 0 = if#(lt(x,10()),x)
       
       1024() = 0 >= 0 = 1024_1(0())
       
       1024_1(x) = 0 >= 0 = if(lt(x,10()),x)
       
       if(true(),x) = 0 >= 0 = double(1024_1(s(x)))
       
       if(false(),x) = 0 >= 0 = s(0())
       
       lt(0(),s(y)) = 0 >= 0 = true()
       
       lt(x,0()) = 0 >= 0 = false()
       
       lt(s(x),s(y)) = 0 >= 0 = lt(x,y)
       
       double(0()) = 0 >= 0 = 0()
       
       double(s(x)) = 0 >= 0 = s(s(double(x)))
       
       10() = 0 >= 0 = double(s(double(s(s(0())))))
      problem:
       DPs:
        
       TRS:
        1024() -> 1024_1(0())
        1024_1(x) -> if(lt(x,10()),x)
        if(true(),x) -> double(1024_1(s(x)))
        if(false(),x) -> s(0())
        lt(0(),s(y)) -> true()
        lt(x,0()) -> false()
        lt(s(x),s(y)) -> lt(x,y)
        double(0()) -> 0()
        double(s(x)) -> s(s(double(x)))
        10() -> double(s(double(s(s(0())))))
      Qed
    
    DPs:
     lt#(s(x),s(y)) -> lt#(x,y)
    TRS:
     1024() -> 1024_1(0())
     1024_1(x) -> if(lt(x,10()),x)
     if(true(),x) -> double(1024_1(s(x)))
     if(false(),x) -> s(0())
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     10() -> double(s(double(s(s(0())))))
    Subterm Criterion Processor:
     simple projection:
      pi(lt#) = 1
     problem:
      DPs:
       
      TRS:
       1024() -> 1024_1(0())
       1024_1(x) -> if(lt(x,10()),x)
       if(true(),x) -> double(1024_1(s(x)))
       if(false(),x) -> s(0())
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       10() -> double(s(double(s(s(0())))))
     Qed
    
    DPs:
     double#(s(x)) -> double#(x)
    TRS:
     1024() -> 1024_1(0())
     1024_1(x) -> if(lt(x,10()),x)
     if(true(),x) -> double(1024_1(s(x)))
     if(false(),x) -> s(0())
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     10() -> double(s(double(s(s(0())))))
    Subterm Criterion Processor:
     simple projection:
      pi(double#) = 0
     problem:
      DPs:
       
      TRS:
       1024() -> 1024_1(0())
       1024_1(x) -> if(lt(x,10()),x)
       if(true(),x) -> double(1024_1(s(x)))
       if(false(),x) -> s(0())
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       10() -> double(s(double(s(s(0())))))
     Qed