MAYBE

Problem:
 log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
 cond(true(),x,y) -> s(0())
 cond(false(),x,y) -> double(log(x,square(s(s(y)))))
 le(0(),v) -> true()
 le(s(u),0()) -> false()
 le(s(u),s(v)) -> le(u,v)
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 square(0()) -> 0()
 square(s(x)) -> s(plus(square(x),double(x)))
 plus(n,0()) -> n
 plus(n,s(m)) -> s(plus(n,m))

Proof:
 DP Processor:
  DPs:
   log#(x,s(s(y))) -> le#(x,s(s(y)))
   log#(x,s(s(y))) -> cond#(le(x,s(s(y))),x,y)
   cond#(false(),x,y) -> square#(s(s(y)))
   cond#(false(),x,y) -> log#(x,square(s(s(y))))
   cond#(false(),x,y) -> double#(log(x,square(s(s(y)))))
   le#(s(u),s(v)) -> le#(u,v)
   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:
   log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
   cond(true(),x,y) -> s(0())
   cond(false(),x,y) -> double(log(x,square(s(s(y)))))
   le(0(),v) -> true()
   le(s(u),0()) -> false()
   le(s(u),s(v)) -> le(u,v)
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   square(0()) -> 0()
   square(s(x)) -> s(plus(square(x),double(x)))
   plus(n,0()) -> n
   plus(n,s(m)) -> s(plus(n,m))
  TDG Processor:
   DPs:
    log#(x,s(s(y))) -> le#(x,s(s(y)))
    log#(x,s(s(y))) -> cond#(le(x,s(s(y))),x,y)
    cond#(false(),x,y) -> square#(s(s(y)))
    cond#(false(),x,y) -> log#(x,square(s(s(y))))
    cond#(false(),x,y) -> double#(log(x,square(s(s(y)))))
    le#(s(u),s(v)) -> le#(u,v)
    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:
    log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
    cond(true(),x,y) -> s(0())
    cond(false(),x,y) -> double(log(x,square(s(s(y)))))
    le(0(),v) -> true()
    le(s(u),0()) -> false()
    le(s(u),s(v)) -> le(u,v)
    double(0()) -> 0()
    double(s(x)) -> s(s(double(x)))
    square(0()) -> 0()
    square(s(x)) -> s(plus(square(x),double(x)))
    plus(n,0()) -> n
    plus(n,s(m)) -> s(plus(n,m))
   graph:
    plus#(n,s(m)) -> plus#(n,m) -> plus#(n,s(m)) -> plus#(n,m)
    double#(s(x)) -> double#(x) ->
    double#(s(x)) -> double#(x)
    square#(s(x)) -> plus#(square(x),double(x)) ->
    plus#(n,s(m)) -> plus#(n,m)
    square#(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) -> double#(log(x,square(s(s(y))))) ->
    double#(s(x)) -> double#(x)
    cond#(false(),x,y) -> square#(s(s(y))) ->
    square#(s(x)) -> plus#(square(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)) -> 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)))
    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) -> 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))) -> cond#(le(x,s(s(y))),x,y) ->
    cond#(false(),x,y) -> square#(s(s(y)))
    log#(x,s(s(y))) -> le#(x,s(s(y))) -> le#(s(u),s(v)) -> le#(u,v)
   SCC Processor:
    #sccs: 5
    #rules: 6
    #arcs: 18/121
    DPs:
     cond#(false(),x,y) -> log#(x,square(s(s(y))))
     log#(x,s(s(y))) -> cond#(le(x,s(s(y))),x,y)
    TRS:
     log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
     cond(true(),x,y) -> s(0())
     cond(false(),x,y) -> double(log(x,square(s(s(y)))))
     le(0(),v) -> true()
     le(s(u),0()) -> false()
     le(s(u),s(v)) -> le(u,v)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     square(0()) -> 0()
     square(s(x)) -> s(plus(square(x),double(x)))
     plus(n,0()) -> n
     plus(n,s(m)) -> s(plus(n,m))
    Open
    
    DPs:
     le#(s(u),s(v)) -> le#(u,v)
    TRS:
     log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
     cond(true(),x,y) -> s(0())
     cond(false(),x,y) -> double(log(x,square(s(s(y)))))
     le(0(),v) -> true()
     le(s(u),0()) -> false()
     le(s(u),s(v)) -> le(u,v)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     square(0()) -> 0()
     square(s(x)) -> s(plus(square(x),double(x)))
     plus(n,0()) -> n
     plus(n,s(m)) -> s(plus(n,m))
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      TRS:
       log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
       cond(true(),x,y) -> s(0())
       cond(false(),x,y) -> double(log(x,square(s(s(y)))))
       le(0(),v) -> true()
       le(s(u),0()) -> false()
       le(s(u),s(v)) -> le(u,v)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       square(0()) -> 0()
       square(s(x)) -> s(plus(square(x),double(x)))
       plus(n,0()) -> n
       plus(n,s(m)) -> s(plus(n,m))
     Qed
    
    DPs:
     square#(s(x)) -> square#(x)
    TRS:
     log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
     cond(true(),x,y) -> s(0())
     cond(false(),x,y) -> double(log(x,square(s(s(y)))))
     le(0(),v) -> true()
     le(s(u),0()) -> false()
     le(s(u),s(v)) -> le(u,v)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     square(0()) -> 0()
     square(s(x)) -> s(plus(square(x),double(x)))
     plus(n,0()) -> n
     plus(n,s(m)) -> s(plus(n,m))
    Subterm Criterion Processor:
     simple projection:
      pi(square#) = 0
     problem:
      DPs:
       
      TRS:
       log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
       cond(true(),x,y) -> s(0())
       cond(false(),x,y) -> double(log(x,square(s(s(y)))))
       le(0(),v) -> true()
       le(s(u),0()) -> false()
       le(s(u),s(v)) -> le(u,v)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       square(0()) -> 0()
       square(s(x)) -> s(plus(square(x),double(x)))
       plus(n,0()) -> n
       plus(n,s(m)) -> s(plus(n,m))
     Qed
    
    DPs:
     double#(s(x)) -> double#(x)
    TRS:
     log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
     cond(true(),x,y) -> s(0())
     cond(false(),x,y) -> double(log(x,square(s(s(y)))))
     le(0(),v) -> true()
     le(s(u),0()) -> false()
     le(s(u),s(v)) -> le(u,v)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     square(0()) -> 0()
     square(s(x)) -> s(plus(square(x),double(x)))
     plus(n,0()) -> n
     plus(n,s(m)) -> s(plus(n,m))
    Subterm Criterion Processor:
     simple projection:
      pi(double#) = 0
     problem:
      DPs:
       
      TRS:
       log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
       cond(true(),x,y) -> s(0())
       cond(false(),x,y) -> double(log(x,square(s(s(y)))))
       le(0(),v) -> true()
       le(s(u),0()) -> false()
       le(s(u),s(v)) -> le(u,v)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       square(0()) -> 0()
       square(s(x)) -> s(plus(square(x),double(x)))
       plus(n,0()) -> n
       plus(n,s(m)) -> s(plus(n,m))
     Qed
    
    DPs:
     plus#(n,s(m)) -> plus#(n,m)
    TRS:
     log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
     cond(true(),x,y) -> s(0())
     cond(false(),x,y) -> double(log(x,square(s(s(y)))))
     le(0(),v) -> true()
     le(s(u),0()) -> false()
     le(s(u),s(v)) -> le(u,v)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     square(0()) -> 0()
     square(s(x)) -> s(plus(square(x),double(x)))
     plus(n,0()) -> n
     plus(n,s(m)) -> s(plus(n,m))
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 1
     problem:
      DPs:
       
      TRS:
       log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
       cond(true(),x,y) -> s(0())
       cond(false(),x,y) -> double(log(x,square(s(s(y)))))
       le(0(),v) -> true()
       le(s(u),0()) -> false()
       le(s(u),s(v)) -> le(u,v)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       square(0()) -> 0()
       square(s(x)) -> s(plus(square(x),double(x)))
       plus(n,0()) -> n
       plus(n,s(m)) -> s(plus(n,m))
     Qed