MAYBE
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:
  Strict:
   {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)}
  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}
  EDG:
   {(square#(s(x)) -> plus#(square(x), double(x)), plus#(n, s(m)) -> plus#(n, m))
    (double#(s(x)) -> double#(x), double#(s(x)) -> double#(x))
    (square#(s(x)) -> square#(x), square#(s(x)) -> plus#(square(x), double(x)))
    (square#(s(x)) -> square#(x), square#(s(x)) -> square#(x))
    (square#(s(x)) -> square#(x), square#(s(x)) -> double#(x))
    (cond#(false(), x, y) -> log#(x, square(s(s(y)))), log#(x, s(s(y))) -> le#(x, s(s(y))))
    (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) -> double#(log(x, square(s(s(y))))), double#(s(x)) -> double#(x))
    (plus#(n, s(m)) -> plus#(n, m), plus#(n, s(m)) -> plus#(n, m))
    (log#(x, s(s(y))) -> le#(x, s(s(y))), le#(s(u), s(v)) -> le#(u, v))
    (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)) -> double#(x), double#(s(x)) -> double#(x))
    (le#(s(u), s(v)) -> le#(u, v), le#(s(u), s(v)) -> le#(u, v))
    (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))) -> 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) -> square#(s(s(y))))}
   SCCS:
    Scc:
     {plus#(n, s(m)) -> plus#(n, m)}
    Scc:
     {square#(s(x)) -> square#(x)}
    Scc:
     {double#(s(x)) -> double#(x)}
    Scc:
     {le#(s(u), s(v)) -> le#(u, v)}
    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:
     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}
     SPSC:
      Simple Projection:
       pi(plus#) = 1
      Strict:
       {}
      Qed
    SCC:
     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}
     SPSC:
      Simple Projection:
       pi(square#) = 0
      Strict:
       {}
      Qed
    SCC:
     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}
     SPSC:
      Simple Projection:
       pi(double#) = 0
      Strict:
       {}
      Qed
    SCC:
     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}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     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}
     Fail