MAYBE
Time: 0.007869
TRS:
 {               lessE(l, t, n) -> if(le(length l, n), le(length toList t, n), l, t, n),
             lessElements(l, t) -> lessE(l, t, 0()),
         if(true(), b, l, t, n) -> l,
   if(false(), true(), l, t, n) -> t,
  if(false(), false(), l, t, n) -> lessE(l, t, s n),
                     le(0(), m) -> true(),
                   le(s n, 0()) -> false(),
                   le(s n, s m) -> le(n, m),
                   length nil() -> 0(),
              length cons(n, l) -> s length l,
                  toList leaf() -> nil(),
         toList node(t1, n, t2) -> append(toList t1, cons(n, toList t2)),
              append(nil(), l2) -> l2,
        append(cons(n, l1), l2) -> cons(n, append(l1, l2)),
                            a() -> c(),
                            a() -> d()}
 DP:
  DP:
   {               lessE#(l, t, n) -> if#(le(length l, n), le(length toList t, n), l, t, n),
                   lessE#(l, t, n) -> le#(length l, n),
                   lessE#(l, t, n) -> le#(length toList t, n),
                   lessE#(l, t, n) -> length# l,
                   lessE#(l, t, n) -> length# toList t,
                   lessE#(l, t, n) -> toList# t,
               lessElements#(l, t) -> lessE#(l, t, 0()),
    if#(false(), false(), l, t, n) -> lessE#(l, t, s n),
                     le#(s n, s m) -> le#(n, m),
                length# cons(n, l) -> length# l,
           toList# node(t1, n, t2) -> toList# t1,
           toList# node(t1, n, t2) -> toList# t2,
           toList# node(t1, n, t2) -> append#(toList t1, cons(n, toList t2)),
          append#(cons(n, l1), l2) -> append#(l1, l2)}
  TRS:
  {               lessE(l, t, n) -> if(le(length l, n), le(length toList t, n), l, t, n),
              lessElements(l, t) -> lessE(l, t, 0()),
          if(true(), b, l, t, n) -> l,
    if(false(), true(), l, t, n) -> t,
   if(false(), false(), l, t, n) -> lessE(l, t, s n),
                      le(0(), m) -> true(),
                    le(s n, 0()) -> false(),
                    le(s n, s m) -> le(n, m),
                    length nil() -> 0(),
               length cons(n, l) -> s length l,
                   toList leaf() -> nil(),
          toList node(t1, n, t2) -> append(toList t1, cons(n, toList t2)),
               append(nil(), l2) -> l2,
         append(cons(n, l1), l2) -> cons(n, append(l1, l2)),
                             a() -> c(),
                             a() -> d()}
  UR:
   {             le(0(), m) -> true(),
               le(s n, 0()) -> false(),
               le(s n, s m) -> le(n, m),
               length nil() -> 0(),
          length cons(n, l) -> s length l,
              toList leaf() -> nil(),
     toList node(t1, n, t2) -> append(toList t1, cons(n, toList t2)),
          append(nil(), l2) -> l2,
    append(cons(n, l1), l2) -> cons(n, append(l1, l2)),
                    b(x, y) -> x,
                    b(x, y) -> y}
   EDG:
    {(lessE#(l, t, n) -> if#(le(length l, n), le(length toList t, n), l, t, n), if#(false(), false(), l, t, n) -> lessE#(l, t, s n))
     (if#(false(), false(), l, t, n) -> lessE#(l, t, s n), lessE#(l, t, n) -> toList# t)
     (if#(false(), false(), l, t, n) -> lessE#(l, t, s n), lessE#(l, t, n) -> length# toList t)
     (if#(false(), false(), l, t, n) -> lessE#(l, t, s n), lessE#(l, t, n) -> length# l)
     (if#(false(), false(), l, t, n) -> lessE#(l, t, s n), lessE#(l, t, n) -> le#(length toList t, n))
     (if#(false(), false(), l, t, n) -> lessE#(l, t, s n), lessE#(l, t, n) -> le#(length l, n))
     (if#(false(), false(), l, t, n) -> lessE#(l, t, s n), lessE#(l, t, n) -> if#(le(length l, n), le(length toList t, n), l, t, n))
     (toList# node(t1, n, t2) -> append#(toList t1, cons(n, toList t2)), append#(cons(n, l1), l2) -> append#(l1, l2))
     (lessE#(l, t, n) -> le#(length l, n), le#(s n, s m) -> le#(n, m))
     (lessE#(l, t, n) -> length# l, length# cons(n, l) -> length# l)
     (lessElements#(l, t) -> lessE#(l, t, 0()), lessE#(l, t, n) -> toList# t)
     (lessElements#(l, t) -> lessE#(l, t, 0()), lessE#(l, t, n) -> length# toList t)
     (lessElements#(l, t) -> lessE#(l, t, 0()), lessE#(l, t, n) -> length# l)
     (lessElements#(l, t) -> lessE#(l, t, 0()), lessE#(l, t, n) -> le#(length toList t, n))
     (lessElements#(l, t) -> lessE#(l, t, 0()), lessE#(l, t, n) -> le#(length l, n))
     (lessElements#(l, t) -> lessE#(l, t, 0()), lessE#(l, t, n) -> if#(le(length l, n), le(length toList t, n), l, t, n))
     (le#(s n, s m) -> le#(n, m), le#(s n, s m) -> le#(n, m))
     (append#(cons(n, l1), l2) -> append#(l1, l2), append#(cons(n, l1), l2) -> append#(l1, l2))
     (length# cons(n, l) -> length# l, length# cons(n, l) -> length# l)
     (lessE#(l, t, n) -> le#(length toList t, n), le#(s n, s m) -> le#(n, m))
     (toList# node(t1, n, t2) -> toList# t1, toList# node(t1, n, t2) -> toList# t1)
     (toList# node(t1, n, t2) -> toList# t1, toList# node(t1, n, t2) -> toList# t2)
     (toList# node(t1, n, t2) -> toList# t1, toList# node(t1, n, t2) -> append#(toList t1, cons(n, toList t2)))
     (lessE#(l, t, n) -> length# toList t, length# cons(n, l) -> length# l)
     (lessE#(l, t, n) -> toList# t, toList# node(t1, n, t2) -> toList# t1)
     (lessE#(l, t, n) -> toList# t, toList# node(t1, n, t2) -> toList# t2)
     (lessE#(l, t, n) -> toList# t, toList# node(t1, n, t2) -> append#(toList t1, cons(n, toList t2)))
     (toList# node(t1, n, t2) -> toList# t2, toList# node(t1, n, t2) -> toList# t1)
     (toList# node(t1, n, t2) -> toList# t2, toList# node(t1, n, t2) -> toList# t2)
     (toList# node(t1, n, t2) -> toList# t2, toList# node(t1, n, t2) -> append#(toList t1, cons(n, toList t2)))}
    STATUS:
     arrows: 0.846939
     SCCS (5):
      Scc:
       {               lessE#(l, t, n) -> if#(le(length l, n), le(length toList t, n), l, t, n),
        if#(false(), false(), l, t, n) -> lessE#(l, t, s n)}
      Scc:
       {length# cons(n, l) -> length# l}
      Scc:
       {le#(s n, s m) -> le#(n, m)}
      Scc:
       {toList# node(t1, n, t2) -> toList# t1,
        toList# node(t1, n, t2) -> toList# t2}
      Scc:
       {append#(cons(n, l1), l2) -> append#(l1, l2)}
      
      
      SCC (2):
       Strict:
        {               lessE#(l, t, n) -> if#(le(length l, n), le(length toList t, n), l, t, n),
         if#(false(), false(), l, t, n) -> lessE#(l, t, s n)}
       Weak:
       {               lessE(l, t, n) -> if(le(length l, n), le(length toList t, n), l, t, n),
                   lessElements(l, t) -> lessE(l, t, 0()),
               if(true(), b, l, t, n) -> l,
         if(false(), true(), l, t, n) -> t,
        if(false(), false(), l, t, n) -> lessE(l, t, s n),
                           le(0(), m) -> true(),
                         le(s n, 0()) -> false(),
                         le(s n, s m) -> le(n, m),
                         length nil() -> 0(),
                    length cons(n, l) -> s length l,
                        toList leaf() -> nil(),
               toList node(t1, n, t2) -> append(toList t1, cons(n, toList t2)),
                    append(nil(), l2) -> l2,
              append(cons(n, l1), l2) -> cons(n, append(l1, l2)),
                                  a() -> c(),
                                  a() -> d()}
       Open
      
      
      
      SCC (1):
       Strict:
        {length# cons(n, l) -> length# l}
       Weak:
       {               lessE(l, t, n) -> if(le(length l, n), le(length toList t, n), l, t, n),
                   lessElements(l, t) -> lessE(l, t, 0()),
               if(true(), b, l, t, n) -> l,
         if(false(), true(), l, t, n) -> t,
        if(false(), false(), l, t, n) -> lessE(l, t, s n),
                           le(0(), m) -> true(),
                         le(s n, 0()) -> false(),
                         le(s n, s m) -> le(n, m),
                         length nil() -> 0(),
                    length cons(n, l) -> s length l,
                        toList leaf() -> nil(),
               toList node(t1, n, t2) -> append(toList t1, cons(n, toList t2)),
                    append(nil(), l2) -> l2,
              append(cons(n, l1), l2) -> cons(n, append(l1, l2)),
                                  a() -> c(),
                                  a() -> d()}
       Open
      
      
      SCC (1):
       Strict:
        {le#(s n, s m) -> le#(n, m)}
       Weak:
       {               lessE(l, t, n) -> if(le(length l, n), le(length toList t, n), l, t, n),
                   lessElements(l, t) -> lessE(l, t, 0()),
               if(true(), b, l, t, n) -> l,
         if(false(), true(), l, t, n) -> t,
        if(false(), false(), l, t, n) -> lessE(l, t, s n),
                           le(0(), m) -> true(),
                         le(s n, 0()) -> false(),
                         le(s n, s m) -> le(n, m),
                         length nil() -> 0(),
                    length cons(n, l) -> s length l,
                        toList leaf() -> nil(),
               toList node(t1, n, t2) -> append(toList t1, cons(n, toList t2)),
                    append(nil(), l2) -> l2,
              append(cons(n, l1), l2) -> cons(n, append(l1, l2)),
                                  a() -> c(),
                                  a() -> d()}
       Open
      SCC (2):
       Strict:
        {toList# node(t1, n, t2) -> toList# t1,
         toList# node(t1, n, t2) -> toList# t2}
       Weak:
       {               lessE(l, t, n) -> if(le(length l, n), le(length toList t, n), l, t, n),
                   lessElements(l, t) -> lessE(l, t, 0()),
               if(true(), b, l, t, n) -> l,
         if(false(), true(), l, t, n) -> t,
        if(false(), false(), l, t, n) -> lessE(l, t, s n),
                           le(0(), m) -> true(),
                         le(s n, 0()) -> false(),
                         le(s n, s m) -> le(n, m),
                         length nil() -> 0(),
                    length cons(n, l) -> s length l,
                        toList leaf() -> nil(),
               toList node(t1, n, t2) -> append(toList t1, cons(n, toList t2)),
                    append(nil(), l2) -> l2,
              append(cons(n, l1), l2) -> cons(n, append(l1, l2)),
                                  a() -> c(),
                                  a() -> d()}
       Open
      
      SCC (1):
       Strict:
        {append#(cons(n, l1), l2) -> append#(l1, l2)}
       Weak:
       {               lessE(l, t, n) -> if(le(length l, n), le(length toList t, n), l, t, n),
                   lessElements(l, t) -> lessE(l, t, 0()),
               if(true(), b, l, t, n) -> l,
         if(false(), true(), l, t, n) -> t,
        if(false(), false(), l, t, n) -> lessE(l, t, s n),
                           le(0(), m) -> true(),
                         le(s n, 0()) -> false(),
                         le(s n, s m) -> le(n, m),
                         length nil() -> 0(),
                    length cons(n, l) -> s length l,
                        toList leaf() -> nil(),
               toList node(t1, n, t2) -> append(toList t1, cons(n, toList t2)),
                    append(nil(), l2) -> l2,
              append(cons(n, l1), l2) -> cons(n, append(l1, l2)),
                                  a() -> c(),
                                  a() -> d()}
       Open