MAYBE
Time: 0.006248
TRS:
 {        le(s x, s y) -> le(x, y),
          le(s x, 0()) -> false(),
            le(0(), y) -> true(),
            double s x -> s s double x,
            double 0() -> 0(),
               log s x -> loop(s x, s 0(), 0()),
               log 0() -> logError(),
       loop(x, s y, z) -> if(le(x, s y), x, s y, z),
  if(false(), x, y, z) -> loop(x, double y, s z),
   if(true(), x, y, z) -> z}
 DP:
  DP:
   {        le#(s x, s y) -> le#(x, y),
              double# s x -> double# x,
                 log# s x -> loop#(s x, s 0(), 0()),
         loop#(x, s y, z) -> le#(x, s y),
         loop#(x, s y, z) -> if#(le(x, s y), x, s y, z),
    if#(false(), x, y, z) -> double# y,
    if#(false(), x, y, z) -> loop#(x, double y, s z)}
  TRS:
  {        le(s x, s y) -> le(x, y),
           le(s x, 0()) -> false(),
             le(0(), y) -> true(),
             double s x -> s s double x,
             double 0() -> 0(),
                log s x -> loop(s x, s 0(), 0()),
                log 0() -> logError(),
        loop(x, s y, z) -> if(le(x, s y), x, s y, z),
   if(false(), x, y, z) -> loop(x, double y, s z),
    if(true(), x, y, z) -> z}
  EDG:
   {(if#(false(), x, y, z) -> double# y, double# s x -> double# x)
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (if#(false(), x, y, z) -> loop#(x, double y, s z), loop#(x, s y, z) -> if#(le(x, s y), x, s y, z))
    (if#(false(), x, y, z) -> loop#(x, double y, s z), loop#(x, s y, z) -> le#(x, s y))
    (loop#(x, s y, z) -> if#(le(x, s y), x, s y, z), if#(false(), x, y, z) -> double# y)
    (loop#(x, s y, z) -> if#(le(x, s y), x, s y, z), if#(false(), x, y, z) -> loop#(x, double y, s z))
    (log# s x -> loop#(s x, s 0(), 0()), loop#(x, s y, z) -> le#(x, s y))
    (log# s x -> loop#(s x, s 0(), 0()), loop#(x, s y, z) -> if#(le(x, s y), x, s y, z))
    (double# s x -> double# x, double# s x -> double# x)
    (loop#(x, s y, z) -> le#(x, s y), le#(s x, s y) -> le#(x, y))}
   STATUS:
    arrows: 0.795918
    SCCS (3):
     Scc:
      {     loop#(x, s y, z) -> if#(le(x, s y), x, s y, z),
       if#(false(), x, y, z) -> loop#(x, double y, s z)}
     Scc:
      {double# s x -> double# x}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     
     
     SCC (2):
      Strict:
       {     loop#(x, s y, z) -> if#(le(x, s y), x, s y, z),
        if#(false(), x, y, z) -> loop#(x, double y, s z)}
      Weak:
      {        le(s x, s y) -> le(x, y),
               le(s x, 0()) -> false(),
                 le(0(), y) -> true(),
                 double s x -> s s double x,
                 double 0() -> 0(),
                    log s x -> loop(s x, s 0(), 0()),
                    log 0() -> logError(),
            loop(x, s y, z) -> if(le(x, s y), x, s y, z),
       if(false(), x, y, z) -> loop(x, double y, s z),
        if(true(), x, y, z) -> z}
      Open
     
     SCC (1):
      Strict:
       {double# s x -> double# x}
      Weak:
      {        le(s x, s y) -> le(x, y),
               le(s x, 0()) -> false(),
                 le(0(), y) -> true(),
                 double s x -> s s double x,
                 double 0() -> 0(),
                    log s x -> loop(s x, s 0(), 0()),
                    log 0() -> logError(),
            loop(x, s y, z) -> if(le(x, s y), x, s y, z),
       if(false(), x, y, z) -> loop(x, double y, s z),
        if(true(), x, y, z) -> z}
      Open
     
     SCC (1):
      Strict:
       {le#(s x, s y) -> le#(x, y)}
      Weak:
      {        le(s x, s y) -> le(x, y),
               le(s x, 0()) -> false(),
                 le(0(), y) -> true(),
                 double s x -> s s double x,
                 double 0() -> 0(),
                    log s x -> loop(s x, s 0(), 0()),
                    log 0() -> logError(),
            loop(x, s y, z) -> if(le(x, s y), x, s y, z),
       if(false(), x, y, z) -> loop(x, double y, s z),
        if(true(), x, y, z) -> z}
      Open