MAYBE
Time: 0.029735
TRS:
 { cond(true(), x, y) -> s 0(),
  cond(false(), x, y) -> double log(x, square s s y),
         le(s u, s v) -> le(u, v),
         le(s u, 0()) -> false(),
           le(0(), v) -> true(),
        log(x, s s y) -> cond(le(x, s s y), x, y),
           double s x -> s s double x,
           double 0() -> 0(),
           square s x -> s plus(square x, double x),
           square 0() -> 0(),
         plus(n, s m) -> s plus(n, m),
         plus(n, 0()) -> n}
 DP:
  DP:
   {cond#(false(), x, y) -> log#(x, square s s y),
    cond#(false(), x, y) -> double# log(x, square s s y),
    cond#(false(), x, y) -> square# s s y,
           le#(s u, s v) -> le#(u, v),
          log#(x, s s y) -> cond#(le(x, s s y), x, y),
          log#(x, s s y) -> le#(x, s s y),
             double# s x -> double# x,
             square# s x -> double# x,
             square# s x -> square# x,
             square# s x -> plus#(square x, double x),
           plus#(n, s m) -> plus#(n, m)}
  TRS:
  { cond(true(), x, y) -> s 0(),
   cond(false(), x, y) -> double log(x, square s s y),
          le(s u, s v) -> le(u, v),
          le(s u, 0()) -> false(),
            le(0(), v) -> true(),
         log(x, s s y) -> cond(le(x, s s y), x, y),
            double s x -> s s double x,
            double 0() -> 0(),
            square s x -> s plus(square x, double x),
            square 0() -> 0(),
          plus(n, s m) -> s plus(n, m),
          plus(n, 0()) -> n}
  EDG:
   {(square# s x -> double# x, double# s x -> double# x)
    (square# s x -> plus#(square x, double x), plus#(n, s m) -> plus#(n, m))
    (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> square# s s y)
    (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> double# log(x, square s s y))
    (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> log#(x, square s s y))
    (log#(x, s s y) -> le#(x, s s y), le#(s u, s v) -> le#(u, v))
    (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
    (le#(s u, s v) -> le#(u, v), le#(s u, s v) -> le#(u, v))
    (cond#(false(), x, y) -> double# log(x, square s s y), double# s x -> double# x)
    (cond#(false(), x, y) -> log#(x, square s s y), log#(x, s s y) -> cond#(le(x, s s y), x, y))
    (cond#(false(), x, y) -> log#(x, square s s y), log#(x, s s y) -> le#(x, s s y))
    (cond#(false(), x, y) -> square# s s y, square# s x -> double# x)
    (cond#(false(), x, y) -> square# s s y, square# s x -> square# x)
    (cond#(false(), x, y) -> square# s s y, square# s x -> plus#(square x, double x))
    (square# s x -> square# x, square# s x -> double# x)
    (square# s x -> square# x, square# s x -> square# x)
    (square# s x -> square# x, square# s x -> plus#(square x, double x))
    (double# s x -> double# x, double# s x -> double# x)}
   EDG:
    {(square# s x -> double# x, double# s x -> double# x)
     (square# s x -> plus#(square x, double x), plus#(n, s m) -> plus#(n, m))
     (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> square# s s y)
     (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> double# log(x, square s s y))
     (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> log#(x, square s s y))
     (log#(x, s s y) -> le#(x, s s y), le#(s u, s v) -> le#(u, v))
     (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
     (le#(s u, s v) -> le#(u, v), le#(s u, s v) -> le#(u, v))
     (cond#(false(), x, y) -> double# log(x, square s s y), double# s x -> double# x)
     (cond#(false(), x, y) -> log#(x, square s s y), log#(x, s s y) -> cond#(le(x, s s y), x, y))
     (cond#(false(), x, y) -> log#(x, square s s y), log#(x, s s y) -> le#(x, s s y))
     (cond#(false(), x, y) -> square# s s y, square# s x -> double# x)
     (cond#(false(), x, y) -> square# s s y, square# s x -> square# x)
     (cond#(false(), x, y) -> square# s s y, square# s x -> plus#(square x, double x))
     (square# s x -> square# x, square# s x -> double# x)
     (square# s x -> square# x, square# s x -> square# x)
     (square# s x -> square# x, square# s x -> plus#(square x, double x))
     (double# s x -> double# x, double# s x -> double# x)}
    EDG:
     {(square# s x -> double# x, double# s x -> double# x)
      (square# s x -> plus#(square x, double x), plus#(n, s m) -> plus#(n, m))
      (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> square# s s y)
      (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> double# log(x, square s s y))
      (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> log#(x, square s s y))
      (log#(x, s s y) -> le#(x, s s y), le#(s u, s v) -> le#(u, v))
      (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
      (le#(s u, s v) -> le#(u, v), le#(s u, s v) -> le#(u, v))
      (cond#(false(), x, y) -> double# log(x, square s s y), double# s x -> double# x)
      (cond#(false(), x, y) -> log#(x, square s s y), log#(x, s s y) -> cond#(le(x, s s y), x, y))
      (cond#(false(), x, y) -> log#(x, square s s y), log#(x, s s y) -> le#(x, s s y))
      (cond#(false(), x, y) -> square# s s y, square# s x -> double# x)
      (cond#(false(), x, y) -> square# s s y, square# s x -> square# x)
      (cond#(false(), x, y) -> square# s s y, square# s x -> plus#(square x, double x))
      (square# s x -> square# x, square# s x -> double# x)
      (square# s x -> square# x, square# s x -> square# x)
      (square# s x -> square# x, square# s x -> plus#(square x, double x))
      (double# s x -> double# x, double# s x -> double# x)}
     EDG:
      {(square# s x -> double# x, double# s x -> double# x)
       (square# s x -> plus#(square x, double x), plus#(n, s m) -> plus#(n, m))
       (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> square# s s y)
       (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> double# log(x, square s s y))
       (log#(x, s s y) -> cond#(le(x, s s y), x, y), cond#(false(), x, y) -> log#(x, square s s y))
       (log#(x, s s y) -> le#(x, s s y), le#(s u, s v) -> le#(u, v))
       (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
       (le#(s u, s v) -> le#(u, v), le#(s u, s v) -> le#(u, v))
       (cond#(false(), x, y) -> double# log(x, square s s y), double# s x -> double# x)
       (cond#(false(), x, y) -> log#(x, square s s y), log#(x, s s y) -> cond#(le(x, s s y), x, y))
       (cond#(false(), x, y) -> log#(x, square s s y), log#(x, s s y) -> le#(x, s s y))
       (cond#(false(), x, y) -> square# s s y, square# s x -> double# x)
       (cond#(false(), x, y) -> square# s s y, square# s x -> square# x)
       (cond#(false(), x, y) -> square# s s y, square# s x -> plus#(square x, double x))
       (square# s x -> square# x, square# s x -> double# x)
       (square# s x -> square# x, square# s x -> square# x)
       (square# s x -> square# x, square# s x -> plus#(square x, double x))
       (double# s x -> double# x, double# s x -> double# x)}
      STATUS:
       arrows: 0.851240
       SCCS (5):
        Scc:
         {cond#(false(), x, y) -> log#(x, square s s y),
                log#(x, s s y) -> cond#(le(x, s s y), x, y)}
        Scc:
         {le#(s u, s v) -> le#(u, v)}
        Scc:
         {square# s x -> square# x}
        Scc:
         {plus#(n, s m) -> plus#(n, m)}
        Scc:
         {double# s x -> double# x}
        
        SCC (2):
         Strict:
          {cond#(false(), x, y) -> log#(x, square s s y),
                 log#(x, s s y) -> cond#(le(x, s s y), x, y)}
         Weak:
         { cond(true(), x, y) -> s 0(),
          cond(false(), x, y) -> double log(x, square s s y),
                 le(s u, s v) -> le(u, v),
                 le(s u, 0()) -> false(),
                   le(0(), v) -> true(),
                log(x, s s y) -> cond(le(x, s s y), x, y),
                   double s x -> s s double x,
                   double 0() -> 0(),
                   square s x -> s plus(square x, double x),
                   square 0() -> 0(),
                 plus(n, s m) -> s plus(n, m),
                 plus(n, 0()) -> n}
         Open
        
        
        SCC (1):
         Strict:
          {le#(s u, s v) -> le#(u, v)}
         Weak:
         { cond(true(), x, y) -> s 0(),
          cond(false(), x, y) -> double log(x, square s s y),
                 le(s u, s v) -> le(u, v),
                 le(s u, 0()) -> false(),
                   le(0(), v) -> true(),
                log(x, s s y) -> cond(le(x, s s y), x, y),
                   double s x -> s s double x,
                   double 0() -> 0(),
                   square s x -> s plus(square x, double x),
                   square 0() -> 0(),
                 plus(n, s m) -> s plus(n, m),
                 plus(n, 0()) -> n}
         Open
        
        SCC (1):
         Strict:
          {square# s x -> square# x}
         Weak:
         { cond(true(), x, y) -> s 0(),
          cond(false(), x, y) -> double log(x, square s s y),
                 le(s u, s v) -> le(u, v),
                 le(s u, 0()) -> false(),
                   le(0(), v) -> true(),
                log(x, s s y) -> cond(le(x, s s y), x, y),
                   double s x -> s s double x,
                   double 0() -> 0(),
                   square s x -> s plus(square x, double x),
                   square 0() -> 0(),
                 plus(n, s m) -> s plus(n, m),
                 plus(n, 0()) -> n}
         Open
        
        SCC (1):
         Strict:
          {plus#(n, s m) -> plus#(n, m)}
         Weak:
         { cond(true(), x, y) -> s 0(),
          cond(false(), x, y) -> double log(x, square s s y),
                 le(s u, s v) -> le(u, v),
                 le(s u, 0()) -> false(),
                   le(0(), v) -> true(),
                log(x, s s y) -> cond(le(x, s s y), x, y),
                   double s x -> s s double x,
                   double 0() -> 0(),
                   square s x -> s plus(square x, double x),
                   square 0() -> 0(),
                 plus(n, s m) -> s plus(n, m),
                 plus(n, 0()) -> n}
         Open
        
        SCC (1):
         Strict:
          {double# s x -> double# x}
         Weak:
         { cond(true(), x, y) -> s 0(),
          cond(false(), x, y) -> double log(x, square s s y),
                 le(s u, s v) -> le(u, v),
                 le(s u, 0()) -> false(),
                   le(0(), v) -> true(),
                log(x, s s y) -> cond(le(x, s s y), x, y),
                   double s x -> s s double x,
                   double 0() -> 0(),
                   square s x -> s plus(square x, double x),
                   square 0() -> 0(),
                 plus(n, s m) -> s plus(n, m),
                 plus(n, 0()) -> n}
         Open