YES

Problem:
 digits() -> d(0())
 d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
 if(true(),x) -> cons(x,d(s(x)))
 if(false(),x) -> nil()
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)

Proof:
 DP Processor:
  DPs:
   digits#() -> d#(0())
   d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0()))))))))))
   d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
   if#(true(),x) -> d#(s(x))
   le#(s(x),s(y)) -> le#(x,y)
  TRS:
   digits() -> d(0())
   d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
   if(true(),x) -> cons(x,d(s(x)))
   if(false(),x) -> nil()
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
  EDG Processor:
   DPs:
    digits#() -> d#(0())
    d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0()))))))))))
    d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
    if#(true(),x) -> d#(s(x))
    le#(s(x),s(y)) -> le#(x,y)
   TRS:
    digits() -> d(0())
    d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
    if(true(),x) -> cons(x,d(s(x)))
    if(false(),x) -> nil()
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
   graph:
    if#(true(),x) -> d#(s(x)) ->
    d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0()))))))))))
    if#(true(),x) -> d#(s(x)) ->
    d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
    le#(s(x),s(y)) -> le#(x,y) ->
    le#(s(x),s(y)) -> le#(x,y)
    d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x) ->
    if#(true(),x) -> d#(s(x))
    d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0())))))))))) ->
    le#(s(x),s(y)) -> le#(x,y)
    digits#() -> d#(0()) -> d#(x) -> le#(x,s(s(s(s(s(s(s(s(s(0()))))))))))
    digits#() -> d#(0()) -> d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 7/25
    DPs:
     if#(true(),x) -> d#(s(x))
     d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
    TRS:
     digits() -> d(0())
     d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
     if(true(),x) -> cons(x,d(s(x)))
     if(false(),x) -> nil()
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
    Bounds Processor:
     bound: 10
     enrichment: top-dp
     automaton:
      final states: {29}
      transitions:
       04() -> 161*
       false2() -> 133*
       false3() -> 157*
       true4() -> 171*
       d{#,5}(184) -> 16,29,18
       s5(192) -> 193*
       s5(187) -> 188*
       s5(189) -> 190*
       s5(191) -> 192*
       s5(186) -> 187*
       s5(193) -> 194*
       s5(188) -> 189*
       s5(190) -> 191*
       s5(185) -> 186*
       s5(160) -> 184*
       if{#,5}(195,184) -> 18,16,29
       le5(77,190) -> 195*
       le5(27,186) -> 195*
       le5(22,186) -> 195*
       le5(17,186) -> 195*
       le5(27,188) -> 195*
       le5(22,188) -> 195*
       le5(17,188) -> 195*
       le5(184,194) -> 195*
       le5(28,185) -> 195*
       le5(23,185) -> 195*
       le5(18,185) -> 195*
       le5(28,187) -> 195*
       le5(23,187) -> 195*
       le5(18,187) -> 195*
       le5(28,189) -> 195*
       le5(23,189) -> 195*
       le5(134,192) -> 195*
       le5(18,189) -> 195*
       le5(29,186) -> 195*
       le5(160,193) -> 195*
       le5(24,186) -> 195*
       le5(29,188) -> 195*
       le5(24,188) -> 195*
       le5(25,185) -> 195*
       le5(20,185) -> 195*
       le5(25,187) -> 195*
       le5(20,187) -> 195*
       le5(25,189) -> 195*
       le5(20,189) -> 195*
       le5(26,186) -> 195*
       le5(21,186) -> 195*
       le5(16,186) -> 195*
       le5(26,188) -> 195*
       le5(21,188) -> 195*
       le5(16,188) -> 195*
       le5(122,191) -> 195*
       le5(27,185) -> 195*
       le5(22,185) -> 195*
       le5(17,185) -> 195*
       le5(27,187) -> 195*
       le5(22,187) -> 195*
       le5(17,187) -> 195*
       le5(27,189) -> 195*
       le5(22,189) -> 195*
       le5(17,189) -> 195*
       le5(28,186) -> 195*
       le5(23,186) -> 195*
       le5(18,186) -> 195*
       le5(28,188) -> 195*
       le5(23,188) -> 195*
       le5(18,188) -> 195*
       le5(29,185) -> 195*
       le5(24,185) -> 195*
       le5(29,187) -> 195*
       le5(24,187) -> 195*
       le5(29,189) -> 195*
       le5(24,189) -> 195*
       le5(25,186) -> 195*
       le5(20,186) -> 195*
       le5(25,188) -> 195*
       le5(20,188) -> 195*
       le5(26,185) -> 195*
       le5(21,185) -> 195*
       le5(16,185) -> 195*
       le5(26,187) -> 195*
       le5(21,187) -> 195*
       le5(16,187) -> 195*
       le5(26,189) -> 195*
       le5(21,189) -> 195*
       le5(16,189) -> 195*
       05() -> 185*
       false4() -> 171*
       true5() -> 195*
       d{#,6}(198) -> 29,18,16
       s6(207) -> 208*
       s6(202) -> 203*
       s6(204) -> 205*
       s6(199) -> 200*
       s6(184) -> 198*
       s6(206) -> 207*
       s6(201) -> 202*
       s6(203) -> 204*
       s6(205) -> 206*
       s6(200) -> 201*
       if{#,6}(209,198) -> 16,29,18
       le6(26,199) -> 209*
       le6(21,199) -> 209*
       le6(16,199) -> 209*
       le6(26,201) -> 209*
       le6(21,201) -> 209*
       le6(16,201) -> 209*
       le6(122,204) -> 209*
       le6(27,200) -> 209*
       le6(22,200) -> 209*
       le6(17,200) -> 209*
       le6(27,202) -> 209*
       le6(22,202) -> 209*
       le6(17,202) -> 209*
       le6(28,199) -> 209*
       le6(23,199) -> 209*
       le6(18,199) -> 209*
       le6(28,201) -> 209*
       le6(23,201) -> 209*
       le6(18,201) -> 209*
       le6(29,200) -> 209*
       le6(24,200) -> 209*
       le6(29,202) -> 209*
       le6(24,202) -> 209*
       le6(25,199) -> 209*
       le6(20,199) -> 209*
       le6(25,201) -> 209*
       le6(20,201) -> 209*
       le6(26,200) -> 209*
       le6(21,200) -> 209*
       le6(16,200) -> 209*
       le6(26,202) -> 209*
       le6(21,202) -> 209*
       le6(16,202) -> 209*
       le6(77,203) -> 209*
       le6(198,208) -> 209*
       le6(27,199) -> 209*
       le6(22,199) -> 209*
       le6(17,199) -> 209*
       le6(27,201) -> 209*
       le6(22,201) -> 209*
       le6(17,201) -> 209*
       le6(184,207) -> 209*
       le6(28,200) -> 209*
       le6(23,200) -> 209*
       le6(18,200) -> 209*
       le6(28,202) -> 209*
       le6(23,202) -> 209*
       le6(134,205) -> 209*
       le6(18,202) -> 209*
       le6(29,199) -> 209*
       le6(160,206) -> 209*
       le6(24,199) -> 209*
       le6(29,201) -> 209*
       le6(24,201) -> 209*
       le6(25,200) -> 209*
       le6(20,200) -> 209*
       le6(25,202) -> 209*
       le6(20,202) -> 209*
       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}(17,25) -> 16*
       if{#,0}(27,27) -> 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*
       06() -> 199*
       true0() -> 20,17
       false5() -> 195*
       d{#,0}(25) -> 18*
       d{#,0}(20) -> 18*
       d{#,0}(27) -> 18*
       d{#,0}(22) -> 18*
       d{#,0}(17) -> 18*
       d{#,0}(29) -> 18*
       d{#,0}(24) -> 18*
       d{#,0}(26) -> 18*
       d{#,0}(21) -> 18*
       d{#,0}(16) -> 18*
       d{#,0}(28) -> 29*
       d{#,0}(23) -> 18*
       d{#,0}(18) -> 18*
       true6() -> 209*
       s0(25) -> 28*
       s0(20) -> 28*
       s0(27) -> 28*
       s0(22) -> 28*
       s0(17) -> 28*
       s0(29) -> 28*
       s0(24) -> 28*
       s0(26) -> 28*
       s0(21) -> 28*
       s0(16) -> 28*
       s0(28) -> 28*
       s0(23) -> 28*
       s0(18) -> 28*
       d{#,7}(222) -> 18,16,29
       le0(27,16) -> 20*
       le0(22,16) -> 20*
       le0(17,16) -> 20*
       le0(27,18) -> 20*
       le0(22,18) -> 20*
       le0(27,20) -> 20*
       le0(17,18) -> 20*
       le0(22,20) -> 20*
       le0(17,20) -> 20*
       le0(27,22) -> 20*
       le0(22,22) -> 20*
       le0(17,22) -> 20*
       le0(27,24) -> 20*
       le0(22,24) -> 20*
       le0(17,24) -> 20*
       le0(27,26) -> 20*
       le0(22,26) -> 20*
       le0(27,28) -> 20*
       le0(17,26) -> 20*
       le0(22,28) -> 20*
       le0(17,28) -> 20*
       le0(28,17) -> 20*
       le0(23,17) -> 20*
       le0(18,17) -> 20*
       le0(28,21) -> 20*
       le0(23,21) -> 20*
       le0(28,23) -> 20*
       le0(18,21) -> 20*
       le0(23,23) -> 20*
       le0(28,25) -> 20*
       le0(18,23) -> 20*
       le0(23,25) -> 20*
       le0(28,27) -> 20*
       le0(18,25) -> 20*
       le0(23,27) -> 20*
       le0(28,29) -> 20*
       le0(18,27) -> 20*
       le0(23,29) -> 20*
       le0(18,29) -> 20*
       le0(29,16) -> 20*
       le0(24,16) -> 20*
       le0(29,18) -> 20*
       le0(24,18) -> 20*
       le0(29,20) -> 20*
       le0(24,20) -> 20*
       le0(29,22) -> 20*
       le0(24,22) -> 20*
       le0(29,24) -> 20*
       le0(24,24) -> 20*
       le0(29,26) -> 20*
       le0(24,26) -> 20*
       le0(29,28) -> 20*
       le0(24,28) -> 20*
       le0(25,17) -> 20*
       le0(20,17) -> 20*
       le0(25,21) -> 20*
       le0(20,21) -> 20*
       le0(25,23) -> 20*
       le0(20,23) -> 20*
       le0(25,25) -> 20*
       le0(20,25) -> 20*
       le0(25,27) -> 20*
       le0(20,27) -> 20*
       le0(25,29) -> 20*
       le0(20,29) -> 20*
       le0(26,16) -> 20*
       le0(21,16) -> 20*
       le0(16,16) -> 20*
       le0(26,18) -> 20*
       le0(21,18) -> 20*
       le0(16,18) -> 20*
       le0(26,20) -> 20*
       le0(21,20) -> 20*
       le0(16,20) -> 20*
       le0(26,22) -> 20*
       le0(21,22) -> 20*
       le0(16,22) -> 20*
       le0(26,24) -> 20*
       le0(21,24) -> 20*
       le0(16,24) -> 20*
       le0(26,26) -> 20*
       le0(21,26) -> 20*
       le0(26,28) -> 20*
       le0(16,26) -> 20*
       le0(21,28) -> 20*
       le0(16,28) -> 20*
       le0(27,17) -> 20*
       le0(22,17) -> 20*
       le0(17,17) -> 20*
       le0(27,21) -> 20*
       le0(22,21) -> 20*
       le0(17,21) -> 20*
       le0(27,23) -> 20*
       le0(22,23) -> 20*
       le0(17,23) -> 20*
       le0(27,25) -> 20*
       le0(22,25) -> 20*
       le0(27,27) -> 20*
       le0(17,25) -> 20*
       le0(22,27) -> 20*
       le0(27,29) -> 20*
       le0(17,27) -> 20*
       le0(22,29) -> 20*
       le0(17,29) -> 20*
       le0(28,16) -> 20*
       le0(23,16) -> 20*
       le0(28,18) -> 20*
       le0(18,16) -> 20*
       le0(23,18) -> 20*
       le0(28,20) -> 20*
       le0(18,18) -> 20*
       le0(23,20) -> 20*
       le0(28,22) -> 20*
       le0(18,20) -> 20*
       le0(23,22) -> 20*
       le0(28,24) -> 20*
       le0(18,22) -> 20*
       le0(23,24) -> 20*
       le0(28,26) -> 20*
       le0(18,24) -> 20*
       le0(23,26) -> 20*
       le0(28,28) -> 20*
       le0(18,26) -> 20*
       le0(23,28) -> 20*
       le0(18,28) -> 20*
       le0(29,17) -> 20*
       le0(24,17) -> 20*
       le0(29,21) -> 20*
       le0(24,21) -> 20*
       le0(29,23) -> 20*
       le0(24,23) -> 20*
       le0(29,25) -> 20*
       le0(24,25) -> 20*
       le0(29,27) -> 20*
       le0(24,27) -> 20*
       le0(29,29) -> 20*
       le0(24,29) -> 20*
       le0(25,16) -> 20*
       le0(20,16) -> 20*
       le0(25,18) -> 20*
       le0(20,18) -> 20*
       le0(25,20) -> 20*
       le0(20,20) -> 20*
       le0(25,22) -> 20*
       le0(20,22) -> 20*
       le0(25,24) -> 20*
       le0(20,24) -> 20*
       le0(25,26) -> 20*
       le0(20,26) -> 20*
       le0(25,28) -> 20*
       le0(20,28) -> 20*
       le0(26,17) -> 20*
       le0(21,17) -> 20*
       le0(16,17) -> 20*
       le0(26,21) -> 20*
       le0(21,21) -> 20*
       le0(16,21) -> 20*
       le0(26,23) -> 20*
       le0(21,23) -> 20*
       le0(16,23) -> 20*
       le0(26,25) -> 20*
       le0(21,25) -> 20*
       le0(16,25) -> 20*
       le0(26,27) -> 20*
       le0(21,27) -> 20*
       le0(26,29) -> 20*
       le0(16,27) -> 20*
       le0(21,29) -> 20*
       le0(16,29) -> 20*
       s7(227) -> 228*
       s7(229) -> 230*
       s7(224) -> 225*
       s7(231) -> 232*
       s7(226) -> 227*
       s7(228) -> 229*
       s7(223) -> 224*
       s7(198) -> 222*
       s7(230) -> 231*
       s7(225) -> 226*
       00() -> 21*
       if{#,7}(233,222) -> 29,18,16
       digits0() -> 22*
       le7(25,224) -> 233*
       le7(20,224) -> 233*
       le7(222,232) -> 233*
       le7(26,223) -> 233*
       le7(21,223) -> 233*
       le7(16,223) -> 233*
       le7(26,225) -> 233*
       le7(21,225) -> 233*
       le7(16,225) -> 233*
       le7(77,226) -> 233*
       le7(198,231) -> 233*
       le7(27,224) -> 233*
       le7(22,224) -> 233*
       le7(17,224) -> 233*
       le7(184,230) -> 233*
       le7(28,223) -> 233*
       le7(23,223) -> 233*
       le7(18,223) -> 233*
       le7(28,225) -> 233*
       le7(23,225) -> 233*
       le7(134,228) -> 233*
       le7(18,225) -> 233*
       le7(160,229) -> 233*
       le7(29,224) -> 233*
       le7(24,224) -> 233*
       le7(25,223) -> 233*
       le7(20,223) -> 233*
       le7(25,225) -> 233*
       le7(20,225) -> 233*
       le7(26,224) -> 233*
       le7(21,224) -> 233*
       le7(16,224) -> 233*
       le7(122,227) -> 233*
       le7(27,223) -> 233*
       le7(22,223) -> 233*
       le7(17,223) -> 233*
       le7(27,225) -> 233*
       le7(22,225) -> 233*
       le7(17,225) -> 233*
       le7(28,224) -> 233*
       le7(23,224) -> 233*
       le7(18,224) -> 233*
       le7(29,223) -> 233*
       le7(24,223) -> 233*
       le7(29,225) -> 233*
       le7(24,225) -> 233*
       d0(25) -> 23*
       d0(20) -> 23*
       d0(27) -> 23*
       d0(22) -> 23*
       d0(17) -> 23*
       d0(29) -> 23*
       d0(24) -> 23*
       d0(26) -> 23*
       d0(21) -> 22,23
       d0(16) -> 23*
       d0(28) -> 23*
       d0(23) -> 23*
       d0(18) -> 23*
       07() -> 223*
       if0(27,16) -> 24*
       if0(22,16) -> 24*
       if0(17,16) -> 24*
       if0(27,18) -> 24*
       if0(22,18) -> 24*
       if0(27,20) -> 24*
       if0(17,18) -> 24*
       if0(22,20) -> 24*
       if0(17,20) -> 24*
       if0(27,22) -> 24*
       if0(22,22) -> 24*
       if0(17,22) -> 24*
       if0(27,24) -> 24*
       if0(22,24) -> 24*
       if0(17,24) -> 24*
       if0(27,26) -> 24*
       if0(22,26) -> 24*
       if0(27,28) -> 24*
       if0(17,26) -> 24*
       if0(22,28) -> 24*
       if0(17,28) -> 24*
       if0(28,17) -> 24*
       if0(23,17) -> 24*
       if0(18,17) -> 24*
       if0(28,21) -> 24*
       if0(23,21) -> 24*
       if0(28,23) -> 24*
       if0(18,21) -> 24*
       if0(23,23) -> 24*
       if0(28,25) -> 24*
       if0(18,23) -> 24*
       if0(23,25) -> 24*
       if0(28,27) -> 24*
       if0(18,25) -> 24*
       if0(23,27) -> 24*
       if0(28,29) -> 24*
       if0(18,27) -> 24*
       if0(23,29) -> 24*
       if0(18,29) -> 24*
       if0(29,16) -> 24*
       if0(24,16) -> 24*
       if0(29,18) -> 24*
       if0(24,18) -> 24*
       if0(29,20) -> 24*
       if0(24,20) -> 24*
       if0(29,22) -> 24*
       if0(24,22) -> 24*
       if0(29,24) -> 24*
       if0(24,24) -> 24*
       if0(29,26) -> 24*
       if0(24,26) -> 24*
       if0(29,28) -> 24*
       if0(24,28) -> 24*
       if0(25,17) -> 24*
       if0(20,17) -> 23,24
       if0(25,21) -> 24*
       if0(20,21) -> 22,23,24
       if0(25,23) -> 24*
       if0(20,23) -> 23,24
       if0(25,25) -> 24*
       if0(20,25) -> 23,24
       if0(25,27) -> 24*
       if0(20,27) -> 23,24
       if0(25,29) -> 24*
       if0(20,29) -> 23,24
       if0(26,16) -> 24*
       if0(21,16) -> 24*
       if0(16,16) -> 24*
       if0(26,18) -> 24*
       if0(21,18) -> 24*
       if0(16,18) -> 24*
       if0(26,20) -> 24*
       if0(21,20) -> 24*
       if0(16,20) -> 24*
       if0(26,22) -> 24*
       if0(21,22) -> 24*
       if0(16,22) -> 24*
       if0(26,24) -> 24*
       if0(21,24) -> 24*
       if0(16,24) -> 24*
       if0(26,26) -> 24*
       if0(21,26) -> 24*
       if0(26,28) -> 24*
       if0(16,26) -> 24*
       if0(21,28) -> 24*
       if0(16,28) -> 24*
       if0(27,17) -> 24*
       if0(22,17) -> 24*
       if0(17,17) -> 24*
       if0(27,21) -> 24*
       if0(22,21) -> 24*
       if0(17,21) -> 24*
       if0(27,23) -> 24*
       if0(22,23) -> 24*
       if0(17,23) -> 24*
       if0(27,25) -> 24*
       if0(22,25) -> 24*
       if0(27,27) -> 24*
       if0(17,25) -> 24*
       if0(22,27) -> 24*
       if0(27,29) -> 24*
       if0(17,27) -> 24*
       if0(22,29) -> 24*
       if0(17,29) -> 24*
       if0(28,16) -> 24*
       if0(23,16) -> 24*
       if0(28,18) -> 24*
       if0(18,16) -> 24*
       if0(23,18) -> 24*
       if0(28,20) -> 24*
       if0(18,18) -> 24*
       if0(23,20) -> 24*
       if0(28,22) -> 24*
       if0(18,20) -> 24*
       if0(23,22) -> 24*
       if0(28,24) -> 24*
       if0(18,22) -> 24*
       if0(23,24) -> 24*
       if0(28,26) -> 24*
       if0(18,24) -> 24*
       if0(23,26) -> 24*
       if0(28,28) -> 24*
       if0(18,26) -> 24*
       if0(23,28) -> 24*
       if0(18,28) -> 24*
       if0(29,17) -> 24*
       if0(24,17) -> 24*
       if0(29,21) -> 24*
       if0(24,21) -> 24*
       if0(29,23) -> 24*
       if0(24,23) -> 24*
       if0(29,25) -> 24*
       if0(24,25) -> 24*
       if0(29,27) -> 24*
       if0(24,27) -> 24*
       if0(29,29) -> 24*
       if0(24,29) -> 24*
       if0(25,16) -> 24*
       if0(20,16) -> 23,24
       if0(25,18) -> 24*
       if0(20,18) -> 23,24
       if0(25,20) -> 24*
       if0(20,20) -> 23,24
       if0(25,22) -> 24*
       if0(20,22) -> 23,24
       if0(25,24) -> 24*
       if0(20,24) -> 23,24
       if0(25,26) -> 24*
       if0(20,26) -> 23,24
       if0(25,28) -> 24*
       if0(20,28) -> 23,24
       if0(26,17) -> 24*
       if0(21,17) -> 24*
       if0(16,17) -> 24*
       if0(26,21) -> 24*
       if0(21,21) -> 24*
       if0(16,21) -> 24*
       if0(26,23) -> 24*
       if0(21,23) -> 24*
       if0(16,23) -> 24*
       if0(26,25) -> 24*
       if0(21,25) -> 24*
       if0(16,25) -> 24*
       if0(26,27) -> 24*
       if0(21,27) -> 24*
       if0(26,29) -> 24*
       if0(16,27) -> 24*
       if0(21,29) -> 24*
       if0(16,29) -> 24*
       false6() -> 209*
       cons0(27,16) -> 25*
       cons0(22,16) -> 25*
       cons0(17,16) -> 25*
       cons0(27,18) -> 25*
       cons0(22,18) -> 25*
       cons0(27,20) -> 25*
       cons0(17,18) -> 25*
       cons0(22,20) -> 25*
       cons0(17,20) -> 25*
       cons0(27,22) -> 25*
       cons0(22,22) -> 25*
       cons0(17,22) -> 25*
       cons0(27,24) -> 25*
       cons0(22,24) -> 25*
       cons0(17,24) -> 25*
       cons0(27,26) -> 25*
       cons0(22,26) -> 25*
       cons0(27,28) -> 25*
       cons0(17,26) -> 25*
       cons0(22,28) -> 25*
       cons0(17,28) -> 25*
       cons0(28,17) -> 25*
       cons0(23,17) -> 25*
       cons0(18,17) -> 25*
       cons0(28,21) -> 25*
       cons0(23,21) -> 25*
       cons0(28,23) -> 23,24,25
       cons0(18,21) -> 25*
       cons0(23,23) -> 23,24,25
       cons0(28,25) -> 25*
       cons0(18,23) -> 23,24,25
       cons0(23,25) -> 25*
       cons0(28,27) -> 25*
       cons0(18,25) -> 25*
       cons0(23,27) -> 25*
       cons0(28,29) -> 25*
       cons0(18,27) -> 25*
       cons0(23,29) -> 25*
       cons0(18,29) -> 25*
       cons0(29,16) -> 25*
       cons0(24,16) -> 25*
       cons0(29,18) -> 25*
       cons0(24,18) -> 25*
       cons0(29,20) -> 25*
       cons0(24,20) -> 25*
       cons0(29,22) -> 25*
       cons0(24,22) -> 25*
       cons0(29,24) -> 25*
       cons0(24,24) -> 25*
       cons0(29,26) -> 25*
       cons0(24,26) -> 25*
       cons0(29,28) -> 25*
       cons0(24,28) -> 25*
       cons0(25,17) -> 25*
       cons0(20,17) -> 25*
       cons0(25,21) -> 25*
       cons0(20,21) -> 25*
       cons0(25,23) -> 23,24,25
       cons0(20,23) -> 23,24,25
       cons0(25,25) -> 25*
       cons0(20,25) -> 25*
       cons0(25,27) -> 25*
       cons0(20,27) -> 25*
       cons0(25,29) -> 25*
       cons0(20,29) -> 25*
       cons0(26,16) -> 25*
       cons0(21,16) -> 25*
       cons0(16,16) -> 25*
       cons0(26,18) -> 25*
       cons0(21,18) -> 25*
       cons0(16,18) -> 25*
       cons0(26,20) -> 25*
       cons0(21,20) -> 25*
       cons0(16,20) -> 25*
       cons0(26,22) -> 25*
       cons0(21,22) -> 25*
       cons0(16,22) -> 25*
       cons0(26,24) -> 25*
       cons0(21,24) -> 25*
       cons0(16,24) -> 25*
       cons0(26,26) -> 25*
       cons0(21,26) -> 25*
       cons0(26,28) -> 25*
       cons0(16,26) -> 25*
       cons0(21,28) -> 25*
       cons0(16,28) -> 25*
       cons0(27,17) -> 25*
       cons0(22,17) -> 25*
       cons0(17,17) -> 25*
       cons0(27,21) -> 25*
       cons0(22,21) -> 25*
       cons0(17,21) -> 25*
       cons0(27,23) -> 23,24,25
       cons0(22,23) -> 23,24,25
       cons0(17,23) -> 23,24,25
       cons0(27,25) -> 25*
       cons0(22,25) -> 25*
       cons0(27,27) -> 25*
       cons0(17,25) -> 25*
       cons0(22,27) -> 25*
       cons0(27,29) -> 25*
       cons0(17,27) -> 25*
       cons0(22,29) -> 25*
       cons0(17,29) -> 25*
       cons0(28,16) -> 25*
       cons0(23,16) -> 25*
       cons0(28,18) -> 25*
       cons0(18,16) -> 25*
       cons0(23,18) -> 25*
       cons0(28,20) -> 25*
       cons0(18,18) -> 25*
       cons0(23,20) -> 25*
       cons0(28,22) -> 25*
       cons0(18,20) -> 25*
       cons0(23,22) -> 25*
       cons0(28,24) -> 25*
       cons0(18,22) -> 25*
       cons0(23,24) -> 25*
       cons0(28,26) -> 25*
       cons0(18,24) -> 25*
       cons0(23,26) -> 25*
       cons0(28,28) -> 25*
       cons0(18,26) -> 25*
       cons0(23,28) -> 25*
       cons0(18,28) -> 25*
       cons0(29,17) -> 25*
       cons0(24,17) -> 25*
       cons0(29,21) -> 25*
       cons0(24,21) -> 25*
       cons0(29,23) -> 23,24,25
       cons0(24,23) -> 23,24,25
       cons0(29,25) -> 25*
       cons0(24,25) -> 25*
       cons0(29,27) -> 25*
       cons0(24,27) -> 25*
       cons0(29,29) -> 25*
       cons0(24,29) -> 25*
       cons0(25,16) -> 25*
       cons0(20,16) -> 25*
       cons0(25,18) -> 25*
       cons0(20,18) -> 25*
       cons0(25,20) -> 25*
       cons0(20,20) -> 25*
       cons0(25,22) -> 25*
       cons0(20,22) -> 25*
       cons0(25,24) -> 25*
       cons0(20,24) -> 25*
       cons0(25,26) -> 25*
       cons0(20,26) -> 25*
       cons0(25,28) -> 25*
       cons0(20,28) -> 25*
       cons0(26,17) -> 25*
       cons0(21,17) -> 25*
       cons0(16,17) -> 25*
       cons0(26,21) -> 25*
       cons0(21,21) -> 25*
       cons0(16,21) -> 25*
       cons0(26,23) -> 23,24,25
       cons0(21,23) -> 22,23,24,25
       cons0(16,23) -> 23,24,25
       cons0(26,25) -> 25*
       cons0(21,25) -> 25*
       cons0(16,25) -> 25*
       cons0(26,27) -> 25*
       cons0(21,27) -> 25*
       cons0(26,29) -> 25*
       cons0(16,27) -> 25*
       cons0(21,29) -> 25*
       cons0(16,29) -> 25*
       true7() -> 233*
       false0() -> 20,26
       d{#,8}(234) -> 16,29,18
       nil0() -> 22,23,24,27
       s8(242) -> 243*
       s8(237) -> 238*
       s8(222) -> 234*
       s8(244) -> 245*
       s8(239) -> 240*
       s8(241) -> 242*
       s8(243) -> 244*
       s8(238) -> 239*
       s8(245) -> 246*
       s8(240) -> 241*
       d{#,1}(77) -> 18,29,16
       if{#,8}(247,234) -> 18,16,29
       s1(25) -> 77*
       s1(20) -> 77*
       s1(117) -> 118*
       s1(112) -> 113*
       s1(27) -> 77*
       s1(22) -> 77*
       s1(17) -> 77*
       s1(119) -> 120*
       s1(114) -> 115*
       s1(29) -> 77*
       s1(24) -> 77*
       s1(116) -> 117*
       s1(111) -> 112*
       s1(26) -> 77*
       s1(21) -> 77*
       s1(16) -> 77*
       s1(118) -> 119*
       s1(113) -> 114*
       s1(28) -> 77*
       s1(23) -> 77*
       s1(18) -> 77*
       s1(115) -> 116*
       le8(29,237) -> 247*
       le8(24,237) -> 247*
       le8(184,243) -> 247*
       le8(25,238) -> 247*
       le8(20,238) -> 247*
       le8(160,242) -> 247*
       le8(26,237) -> 247*
       le8(21,237) -> 247*
       le8(16,237) -> 247*
       le8(122,240) -> 247*
       le8(27,238) -> 247*
       le8(22,238) -> 247*
       le8(17,238) -> 247*
       le8(28,237) -> 247*
       le8(23,237) -> 247*
       le8(18,237) -> 247*
       le8(29,238) -> 247*
       le8(24,238) -> 247*
       le8(234,246) -> 247*
       le8(25,237) -> 247*
       le8(20,237) -> 247*
       le8(26,238) -> 247*
       le8(21,238) -> 247*
       le8(16,238) -> 247*
       le8(77,239) -> 247*
       le8(27,237) -> 247*
       le8(22,237) -> 247*
       le8(17,237) -> 247*
       le8(222,245) -> 247*
       le8(28,238) -> 247*
       le8(23,238) -> 247*
       le8(134,241) -> 247*
       le8(18,238) -> 247*
       le8(198,244) -> 247*
       if{#,1}(121,77) -> 29,18,16
       08() -> 237*
       le1(25,117) -> 121*
       le1(17,111) -> 121*
       le1(20,117) -> 121*
       le1(25,119) -> 121*
       le1(20,119) -> 121*
       le1(26,114) -> 121*
       le1(21,114) -> 121*
       le1(16,114) -> 121*
       le1(26,116) -> 121*
       le1(28,112) -> 121*
       le1(21,116) -> 121*
       le1(23,112) -> 121*
       le1(16,116) -> 121*
       le1(26,118) -> 121*
       le1(18,112) -> 121*
       le1(21,118) -> 121*
       le1(16,118) -> 121*
       le1(27,113) -> 121*
       le1(22,113) -> 121*
       le1(17,113) -> 121*
       le1(27,115) -> 121*
       le1(29,111) -> 121*
       le1(22,115) -> 121*
       le1(24,111) -> 121*
       le1(17,115) -> 121*
       le1(27,117) -> 121*
       le1(22,117) -> 121*
       le1(17,117) -> 121*
       le1(27,119) -> 121*
       le1(22,119) -> 121*
       le1(17,119) -> 121*
       le1(28,114) -> 121*
       le1(23,114) -> 121*
       le1(18,114) -> 121*
       le1(28,116) -> 121*
       le1(23,116) -> 121*
       le1(25,112) -> 121*
       le1(18,116) -> 121*
       le1(28,118) -> 121*
       le1(20,112) -> 121*
       le1(23,118) -> 121*
       le1(18,118) -> 121*
       le1(29,113) -> 121*
       le1(24,113) -> 121*
       le1(29,115) -> 121*
       le1(24,115) -> 121*
       le1(26,111) -> 121*
       le1(29,117) -> 121*
       le1(21,111) -> 121*
       le1(24,117) -> 121*
       le1(16,111) -> 121*
       le1(29,119) -> 121*
       le1(24,119) -> 121*
       le1(25,114) -> 121*
       le1(20,114) -> 121*
       le1(25,116) -> 121*
       le1(27,112) -> 121*
       le1(20,116) -> 121*
       le1(22,112) -> 121*
       le1(25,118) -> 121*
       le1(17,112) -> 121*
       le1(20,118) -> 121*
       le1(26,113) -> 121*
       le1(21,113) -> 121*
       le1(16,113) -> 121*
       le1(26,115) -> 121*
       le1(28,111) -> 121*
       le1(21,115) -> 121*
       le1(23,111) -> 121*
       le1(16,115) -> 121*
       le1(26,117) -> 121*
       le1(18,111) -> 121*
       le1(21,117) -> 121*
       le1(16,117) -> 121*
       le1(26,119) -> 121*
       le1(21,119) -> 121*
       le1(16,119) -> 121*
       le1(77,120) -> 121*
       le1(27,114) -> 121*
       le1(22,114) -> 121*
       le1(17,114) -> 121*
       le1(27,116) -> 121*
       le1(29,112) -> 121*
       le1(22,116) -> 121*
       le1(24,112) -> 121*
       le1(17,116) -> 121*
       le1(27,118) -> 121*
       le1(22,118) -> 121*
       le1(17,118) -> 121*
       le1(28,113) -> 121*
       le1(23,113) -> 121*
       le1(18,113) -> 121*
       le1(28,115) -> 121*
       le1(23,115) -> 121*
       le1(25,111) -> 121*
       le1(18,115) -> 121*
       le1(28,117) -> 121*
       le1(20,111) -> 121*
       le1(23,117) -> 121*
       le1(18,117) -> 121*
       le1(28,119) -> 121*
       le1(23,119) -> 121*
       le1(18,119) -> 121*
       le1(29,114) -> 121*
       le1(24,114) -> 121*
       le1(29,116) -> 121*
       le1(24,116) -> 121*
       le1(26,112) -> 121*
       le1(29,118) -> 121*
       le1(21,112) -> 121*
       le1(24,118) -> 121*
       le1(16,112) -> 121*
       le1(25,113) -> 121*
       le1(20,113) -> 121*
       le1(25,115) -> 121*
       le1(27,111) -> 121*
       le1(20,115) -> 121*
       le1(22,111) -> 121*
       false7() -> 233*
       01() -> 111*
       true8() -> 247*
       true1() -> 121*
       d{#,9}(260) -> 29,18,16
       d{#,2}(122) -> 16,29,18
       s9(267) -> 268*
       s9(262) -> 263*
       s9(269) -> 270*
       s9(264) -> 265*
       s9(234) -> 260*
       s9(266) -> 267*
       s9(261) -> 262*
       s9(268) -> 269*
       s9(263) -> 264*
       s9(265) -> 266*
       s2(127) -> 128*
       s2(77) -> 122*
       s2(129) -> 130*
       s2(124) -> 125*
       s2(131) -> 132*
       s2(126) -> 127*
       s2(128) -> 129*
       s2(123) -> 124*
       s2(130) -> 131*
       s2(125) -> 126*
       false8() -> 247*
       if{#,2}(133,122) -> 18,16,29
       if{#,9}(271,260) -> 16,29,18
       le2(25,123) -> 133*
       le2(20,123) -> 133*
       le2(25,125) -> 133*
       le2(20,125) -> 133*
       le2(25,127) -> 133*
       le2(20,127) -> 133*
       le2(25,129) -> 133*
       le2(20,129) -> 133*
       le2(26,124) -> 133*
       le2(21,124) -> 133*
       le2(16,124) -> 133*
       le2(26,126) -> 133*
       le2(21,126) -> 133*
       le2(16,126) -> 133*
       le2(26,128) -> 133*
       le2(21,128) -> 133*
       le2(16,128) -> 133*
       le2(26,130) -> 133*
       le2(21,130) -> 133*
       le2(16,130) -> 133*
       le2(77,131) -> 133*
       le2(27,123) -> 133*
       le2(22,123) -> 133*
       le2(17,123) -> 133*
       le2(27,125) -> 133*
       le2(22,125) -> 133*
       le2(17,125) -> 133*
       le2(27,127) -> 133*
       le2(22,127) -> 133*
       le2(17,127) -> 133*
       le2(27,129) -> 133*
       le2(22,129) -> 133*
       le2(17,129) -> 133*
       le2(28,124) -> 133*
       le2(23,124) -> 133*
       le2(18,124) -> 133*
       le2(28,126) -> 133*
       le2(23,126) -> 133*
       le2(18,126) -> 133*
       le2(28,128) -> 133*
       le2(23,128) -> 133*
       le2(18,128) -> 133*
       le2(28,130) -> 133*
       le2(23,130) -> 133*
       le2(18,130) -> 133*
       le2(29,123) -> 133*
       le2(24,123) -> 133*
       le2(29,125) -> 133*
       le2(24,125) -> 133*
       le2(29,127) -> 133*
       le2(24,127) -> 133*
       le2(29,129) -> 133*
       le2(24,129) -> 133*
       le2(25,124) -> 133*
       le2(20,124) -> 133*
       le2(25,126) -> 133*
       le2(20,126) -> 133*
       le2(25,128) -> 133*
       le2(20,128) -> 133*
       le2(25,130) -> 133*
       le2(20,130) -> 133*
       le2(26,123) -> 133*
       le2(21,123) -> 133*
       le2(16,123) -> 133*
       le2(26,125) -> 133*
       le2(21,125) -> 133*
       le2(16,125) -> 133*
       le2(26,127) -> 133*
       le2(21,127) -> 133*
       le2(16,127) -> 133*
       le2(26,129) -> 133*
       le2(21,129) -> 133*
       le2(16,129) -> 133*
       le2(122,132) -> 133*
       le2(27,124) -> 133*
       le2(22,124) -> 133*
       le2(17,124) -> 133*
       le2(27,126) -> 133*
       le2(22,126) -> 133*
       le2(17,126) -> 133*
       le2(27,128) -> 133*
       le2(22,128) -> 133*
       le2(17,128) -> 133*
       le2(27,130) -> 133*
       le2(22,130) -> 133*
       le2(17,130) -> 133*
       le2(28,123) -> 133*
       le2(23,123) -> 133*
       le2(18,123) -> 133*
       le2(28,125) -> 133*
       le2(23,125) -> 133*
       le2(18,125) -> 133*
       le2(28,127) -> 133*
       le2(23,127) -> 133*
       le2(18,127) -> 133*
       le2(28,129) -> 133*
       le2(23,129) -> 133*
       le2(18,129) -> 133*
       le2(29,124) -> 133*
       le2(24,124) -> 133*
       le2(29,126) -> 133*
       le2(24,126) -> 133*
       le2(29,128) -> 133*
       le2(24,128) -> 133*
       le2(29,130) -> 133*
       le2(24,130) -> 133*
       le9(122,263) -> 271*
       le9(27,261) -> 271*
       le9(22,261) -> 271*
       le9(17,261) -> 271*
       le9(234,269) -> 271*
       le9(260,270) -> 271*
       le9(29,261) -> 271*
       le9(24,261) -> 271*
       le9(222,268) -> 271*
       le9(26,261) -> 271*
       le9(21,261) -> 271*
       le9(16,261) -> 271*
       le9(77,262) -> 271*
       le9(198,267) -> 271*
       le9(184,266) -> 271*
       le9(28,261) -> 271*
       le9(23,261) -> 271*
       le9(134,264) -> 271*
       le9(18,261) -> 271*
       le9(160,265) -> 271*
       le9(25,261) -> 271*
       le9(20,261) -> 271*
       02() -> 123*
       09() -> 261*
       true2() -> 133*
       false9() -> 271*
       d{#,3}(134) -> 29,18,16
       true9() -> 271*
       s3(152) -> 153*
       s3(147) -> 148*
       s3(122) -> 134*
       s3(154) -> 155*
       s3(149) -> 150*
       s3(151) -> 152*
       s3(153) -> 154*
       s3(148) -> 149*
       s3(155) -> 156*
       s3(150) -> 151*
       d{#,10}(272) -> 18,16,29
       if{#,3}(157,134) -> 16,29,18
       s10(277) -> 278*
       s10(279) -> 280*
       s10(274) -> 275*
       s10(281) -> 282*
       s10(276) -> 277*
       s10(278) -> 279*
       s10(273) -> 274*
       s10(280) -> 281*
       s10(275) -> 276*
       s10(260) -> 272*
       le3(134,156) -> 157*
       le3(18,153) -> 157*
       le3(29,148) -> 157*
       le3(24,148) -> 157*
       le3(29,150) -> 157*
       le3(24,150) -> 157*
       le3(29,152) -> 157*
       le3(24,152) -> 157*
       le3(25,147) -> 157*
       le3(20,147) -> 157*
       le3(25,149) -> 157*
       le3(20,149) -> 157*
       le3(25,151) -> 157*
       le3(20,151) -> 157*
       le3(25,153) -> 157*
       le3(20,153) -> 157*
       le3(26,148) -> 157*
       le3(21,148) -> 157*
       le3(16,148) -> 157*
       le3(26,150) -> 157*
       le3(21,150) -> 157*
       le3(16,150) -> 157*
       le3(26,152) -> 157*
       le3(21,152) -> 157*
       le3(16,152) -> 157*
       le3(122,155) -> 157*
       le3(27,147) -> 157*
       le3(22,147) -> 157*
       le3(17,147) -> 157*
       le3(27,149) -> 157*
       le3(22,149) -> 157*
       le3(17,149) -> 157*
       le3(27,151) -> 157*
       le3(22,151) -> 157*
       le3(17,151) -> 157*
       le3(27,153) -> 157*
       le3(22,153) -> 157*
       le3(17,153) -> 157*
       le3(28,148) -> 157*
       le3(23,148) -> 157*
       le3(18,148) -> 157*
       le3(28,150) -> 157*
       le3(23,150) -> 157*
       le3(18,150) -> 157*
       le3(28,152) -> 157*
       le3(23,152) -> 157*
       le3(18,152) -> 157*
       le3(29,147) -> 157*
       le3(24,147) -> 157*
       le3(29,149) -> 157*
       le3(24,149) -> 157*
       le3(29,151) -> 157*
       le3(24,151) -> 157*
       le3(29,153) -> 157*
       le3(24,153) -> 157*
       le3(25,148) -> 157*
       le3(20,148) -> 157*
       le3(25,150) -> 157*
       le3(20,150) -> 157*
       le3(25,152) -> 157*
       le3(20,152) -> 157*
       le3(26,147) -> 157*
       le3(21,147) -> 157*
       le3(16,147) -> 157*
       le3(26,149) -> 157*
       le3(21,149) -> 157*
       le3(16,149) -> 157*
       le3(26,151) -> 157*
       le3(21,151) -> 157*
       le3(16,151) -> 157*
       le3(26,153) -> 157*
       le3(21,153) -> 157*
       le3(16,153) -> 157*
       le3(77,154) -> 157*
       le3(27,148) -> 157*
       le3(22,148) -> 157*
       le3(17,148) -> 157*
       le3(27,150) -> 157*
       le3(22,150) -> 157*
       le3(17,150) -> 157*
       le3(27,152) -> 157*
       le3(22,152) -> 157*
       le3(17,152) -> 157*
       le3(28,147) -> 157*
       le3(23,147) -> 157*
       le3(18,147) -> 157*
       le3(28,149) -> 157*
       le3(23,149) -> 157*
       le3(18,149) -> 157*
       le3(28,151) -> 157*
       le3(23,151) -> 157*
       le3(18,151) -> 157*
       le3(28,153) -> 157*
       le3(23,153) -> 157*
       if{#,10}(283,272) -> 29,18,16
       03() -> 147*
       le10(222,279) -> 283*
       le10(77,273) -> 283*
       le10(198,278) -> 283*
       le10(184,277) -> 283*
       le10(134,275) -> 283*
       le10(160,276) -> 283*
       le10(272,282) -> 283*
       le10(122,274) -> 283*
       le10(234,280) -> 283*
       le10(260,281) -> 283*
       false1() -> 121*
       010() -> 273*
       true3() -> 157*
       false10() -> 283*
       d{#,4}(160) -> 18,16,29
       s4(167) -> 168*
       s4(162) -> 163*
       s4(169) -> 170*
       s4(164) -> 165*
       s4(134) -> 160*
       s4(166) -> 167*
       s4(161) -> 162*
       s4(168) -> 169*
       s4(163) -> 164*
       s4(165) -> 166*
       if{#,4}(171,160) -> 29,18,16
       le4(28,161) -> 171*
       le4(23,161) -> 171*
       le4(18,161) -> 171*
       le4(28,163) -> 171*
       le4(23,163) -> 171*
       le4(18,163) -> 171*
       le4(28,165) -> 171*
       le4(23,165) -> 171*
       le4(18,165) -> 171*
       le4(29,162) -> 171*
       le4(24,162) -> 171*
       le4(29,164) -> 171*
       le4(24,164) -> 171*
       le4(29,166) -> 171*
       le4(24,166) -> 171*
       le4(25,161) -> 171*
       le4(20,161) -> 171*
       le4(25,163) -> 171*
       le4(20,163) -> 171*
       le4(25,165) -> 171*
       le4(20,165) -> 171*
       le4(26,162) -> 171*
       le4(21,162) -> 171*
       le4(16,162) -> 171*
       le4(26,164) -> 171*
       le4(21,164) -> 171*
       le4(16,164) -> 171*
       le4(26,166) -> 171*
       le4(21,166) -> 171*
       le4(16,166) -> 171*
       le4(77,167) -> 171*
       le4(27,161) -> 171*
       le4(22,161) -> 171*
       le4(17,161) -> 171*
       le4(27,163) -> 171*
       le4(22,163) -> 171*
       le4(17,163) -> 171*
       le4(27,165) -> 171*
       le4(22,165) -> 171*
       le4(17,165) -> 171*
       le4(28,162) -> 171*
       le4(23,162) -> 171*
       le4(18,162) -> 171*
       le4(28,164) -> 171*
       le4(23,164) -> 171*
       le4(18,164) -> 171*
       le4(28,166) -> 171*
       le4(23,166) -> 171*
       le4(134,169) -> 171*
       le4(18,166) -> 171*
       le4(29,161) -> 171*
       le4(24,161) -> 171*
       le4(29,163) -> 171*
       le4(160,170) -> 171*
       le4(24,163) -> 171*
       le4(29,165) -> 171*
       le4(24,165) -> 171*
       le4(25,162) -> 171*
       le4(20,162) -> 171*
       le4(25,164) -> 171*
       le4(20,164) -> 171*
       le4(25,166) -> 171*
       le4(20,166) -> 171*
       le4(26,161) -> 171*
       le4(21,161) -> 171*
       le4(16,161) -> 171*
       le4(26,163) -> 171*
       le4(21,163) -> 171*
       le4(16,163) -> 171*
       le4(26,165) -> 171*
       le4(21,165) -> 171*
       le4(16,165) -> 171*
       le4(122,168) -> 171*
       le4(27,162) -> 171*
       le4(22,162) -> 171*
       le4(17,162) -> 171*
       le4(27,164) -> 171*
       le4(22,164) -> 171*
       le4(17,164) -> 171*
       le4(27,166) -> 171*
       le4(22,166) -> 171*
       le4(17,166) -> 171*
     problem:
      DPs:
       d#(x) -> if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
      TRS:
       digits() -> d(0())
       d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
       if(true(),x) -> cons(x,d(s(x)))
       if(false(),x) -> nil()
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [if#](x0, x1) = 0,
       
       [d#](x0) = 1,
       
       [nil] = 0,
       
       [false] = 0,
       
       [cons](x0, x1) = 0,
       
       [true] = 0,
       
       [if](x0, x1) = 0,
       
       [le](x0, x1) = 0,
       
       [s](x0) = 0,
       
       [d](x0) = 0,
       
       [0] = 0,
       
       [digits] = 0
      orientation:
       d#(x) = 1 >= 0 = if#(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
       
       digits() = 0 >= 0 = d(0())
       
       d(x) = 0 >= 0 = if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
       
       if(true(),x) = 0 >= 0 = cons(x,d(s(x)))
       
       if(false(),x) = 0 >= 0 = nil()
       
       le(0(),y) = 0 >= 0 = true()
       
       le(s(x),0()) = 0 >= 0 = false()
       
       le(s(x),s(y)) = 0 >= 0 = le(x,y)
      problem:
       DPs:
        
       TRS:
        digits() -> d(0())
        d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
        if(true(),x) -> cons(x,d(s(x)))
        if(false(),x) -> nil()
        le(0(),y) -> true()
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
      Qed
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     digits() -> d(0())
     d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
     if(true(),x) -> cons(x,d(s(x)))
     if(false(),x) -> nil()
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      TRS:
       digits() -> d(0())
       d(x) -> if(le(x,s(s(s(s(s(s(s(s(s(0())))))))))),x)
       if(true(),x) -> cons(x,d(s(x)))
       if(false(),x) -> nil()
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
     Qed