MAYBE

Problem:
 le(0(),y,z) -> greater(y,z)
 le(s(x),0(),z) -> false()
 le(s(x),s(y),0()) -> false()
 le(s(x),s(y),s(z)) -> le(x,y,z)
 greater(x,0()) -> first()
 greater(0(),s(y)) -> second()
 greater(s(x),s(y)) -> greater(x,y)
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 triple(x) -> if(le(x,x,double(x)),x,0(),0())
 if(false(),x,y,z) -> true()
 if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
 if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)

Proof:
 DP Processor:
  DPs:
   le#(0(),y,z) -> greater#(y,z)
   le#(s(x),s(y),s(z)) -> le#(x,y,z)
   greater#(s(x),s(y)) -> greater#(x,y)
   double#(s(x)) -> double#(x)
   triple#(x) -> double#(x)
   triple#(x) -> le#(x,x,double(x))
   triple#(x) -> if#(le(x,x,double(x)),x,0(),0())
   if#(first(),x,y,z) -> le#(s(x),y,s(z))
   if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z))
   if#(second(),x,y,z) -> le#(s(x),s(y),z)
   if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z)
  TRS:
   le(0(),y,z) -> greater(y,z)
   le(s(x),0(),z) -> false()
   le(s(x),s(y),0()) -> false()
   le(s(x),s(y),s(z)) -> le(x,y,z)
   greater(x,0()) -> first()
   greater(0(),s(y)) -> second()
   greater(s(x),s(y)) -> greater(x,y)
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   triple(x) -> if(le(x,x,double(x)),x,0(),0())
   if(false(),x,y,z) -> true()
   if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
   if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)
  TDG Processor:
   DPs:
    le#(0(),y,z) -> greater#(y,z)
    le#(s(x),s(y),s(z)) -> le#(x,y,z)
    greater#(s(x),s(y)) -> greater#(x,y)
    double#(s(x)) -> double#(x)
    triple#(x) -> double#(x)
    triple#(x) -> le#(x,x,double(x))
    triple#(x) -> if#(le(x,x,double(x)),x,0(),0())
    if#(first(),x,y,z) -> le#(s(x),y,s(z))
    if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z))
    if#(second(),x,y,z) -> le#(s(x),s(y),z)
    if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z)
   TRS:
    le(0(),y,z) -> greater(y,z)
    le(s(x),0(),z) -> false()
    le(s(x),s(y),0()) -> false()
    le(s(x),s(y),s(z)) -> le(x,y,z)
    greater(x,0()) -> first()
    greater(0(),s(y)) -> second()
    greater(s(x),s(y)) -> greater(x,y)
    double(0()) -> 0()
    double(s(x)) -> s(s(double(x)))
    triple(x) -> if(le(x,x,double(x)),x,0(),0())
    if(false(),x,y,z) -> true()
    if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
    if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)
   graph:
    if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z) ->
    if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z)
    if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z) ->
    if#(second(),x,y,z) -> le#(s(x),s(y),z)
    if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z) ->
    if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z))
    if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z) ->
    if#(first(),x,y,z) -> le#(s(x),y,s(z))
    if#(second(),x,y,z) -> le#(s(x),s(y),z) ->
    le#(s(x),s(y),s(z)) -> le#(x,y,z)
    if#(second(),x,y,z) -> le#(s(x),s(y),z) ->
    le#(0(),y,z) -> greater#(y,z)
    if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z)) ->
    if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z)
    if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z)) ->
    if#(second(),x,y,z) -> le#(s(x),s(y),z)
    if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z)) ->
    if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z))
    if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z)) ->
    if#(first(),x,y,z) -> le#(s(x),y,s(z))
    if#(first(),x,y,z) -> le#(s(x),y,s(z)) ->
    le#(s(x),s(y),s(z)) -> le#(x,y,z)
    if#(first(),x,y,z) -> le#(s(x),y,s(z)) ->
    le#(0(),y,z) -> greater#(y,z)
    triple#(x) -> if#(le(x,x,double(x)),x,0(),0()) ->
    if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z)
    triple#(x) -> if#(le(x,x,double(x)),x,0(),0()) ->
    if#(second(),x,y,z) -> le#(s(x),s(y),z)
    triple#(x) -> if#(le(x,x,double(x)),x,0(),0()) ->
    if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z))
    triple#(x) -> if#(le(x,x,double(x)),x,0(),0()) ->
    if#(first(),x,y,z) -> le#(s(x),y,s(z))
    triple#(x) -> double#(x) -> double#(s(x)) -> double#(x)
    triple#(x) -> le#(x,x,double(x)) ->
    le#(s(x),s(y),s(z)) -> le#(x,y,z)
    triple#(x) -> le#(x,x,double(x)) -> le#(0(),y,z) -> greater#(y,z)
    double#(s(x)) -> double#(x) -> double#(s(x)) -> double#(x)
    greater#(s(x),s(y)) -> greater#(x,y) ->
    greater#(s(x),s(y)) -> greater#(x,y)
    le#(s(x),s(y),s(z)) -> le#(x,y,z) ->
    le#(s(x),s(y),s(z)) -> le#(x,y,z)
    le#(s(x),s(y),s(z)) -> le#(x,y,z) -> le#(0(),y,z) -> greater#(y,z)
    le#(0(),y,z) -> greater#(y,z) -> greater#(s(x),s(y)) -> greater#(x,y)
   SCC Processor:
    #sccs: 4
    #rules: 5
    #arcs: 24/121
    DPs:
     double#(s(x)) -> double#(x)
    TRS:
     le(0(),y,z) -> greater(y,z)
     le(s(x),0(),z) -> false()
     le(s(x),s(y),0()) -> false()
     le(s(x),s(y),s(z)) -> le(x,y,z)
     greater(x,0()) -> first()
     greater(0(),s(y)) -> second()
     greater(s(x),s(y)) -> greater(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     triple(x) -> if(le(x,x,double(x)),x,0(),0())
     if(false(),x,y,z) -> true()
     if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
     if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)
    Subterm Criterion Processor:
     simple projection:
      pi(double#) = 0
     problem:
      DPs:
       
      TRS:
       le(0(),y,z) -> greater(y,z)
       le(s(x),0(),z) -> false()
       le(s(x),s(y),0()) -> false()
       le(s(x),s(y),s(z)) -> le(x,y,z)
       greater(x,0()) -> first()
       greater(0(),s(y)) -> second()
       greater(s(x),s(y)) -> greater(x,y)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       triple(x) -> if(le(x,x,double(x)),x,0(),0())
       if(false(),x,y,z) -> true()
       if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
       if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)
     Qed
    
    DPs:
     if#(second(),x,y,z) -> if#(le(s(x),s(y),z),s(x),s(y),z)
     if#(first(),x,y,z) -> if#(le(s(x),y,s(z)),s(x),y,s(z))
    TRS:
     le(0(),y,z) -> greater(y,z)
     le(s(x),0(),z) -> false()
     le(s(x),s(y),0()) -> false()
     le(s(x),s(y),s(z)) -> le(x,y,z)
     greater(x,0()) -> first()
     greater(0(),s(y)) -> second()
     greater(s(x),s(y)) -> greater(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     triple(x) -> if(le(x,x,double(x)),x,0(),0())
     if(false(),x,y,z) -> true()
     if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
     if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)
    Open
    
    DPs:
     le#(s(x),s(y),s(z)) -> le#(x,y,z)
    TRS:
     le(0(),y,z) -> greater(y,z)
     le(s(x),0(),z) -> false()
     le(s(x),s(y),0()) -> false()
     le(s(x),s(y),s(z)) -> le(x,y,z)
     greater(x,0()) -> first()
     greater(0(),s(y)) -> second()
     greater(s(x),s(y)) -> greater(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     triple(x) -> if(le(x,x,double(x)),x,0(),0())
     if(false(),x,y,z) -> true()
     if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
     if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 2
     problem:
      DPs:
       
      TRS:
       le(0(),y,z) -> greater(y,z)
       le(s(x),0(),z) -> false()
       le(s(x),s(y),0()) -> false()
       le(s(x),s(y),s(z)) -> le(x,y,z)
       greater(x,0()) -> first()
       greater(0(),s(y)) -> second()
       greater(s(x),s(y)) -> greater(x,y)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       triple(x) -> if(le(x,x,double(x)),x,0(),0())
       if(false(),x,y,z) -> true()
       if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
       if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)
     Qed
    
    DPs:
     greater#(s(x),s(y)) -> greater#(x,y)
    TRS:
     le(0(),y,z) -> greater(y,z)
     le(s(x),0(),z) -> false()
     le(s(x),s(y),0()) -> false()
     le(s(x),s(y),s(z)) -> le(x,y,z)
     greater(x,0()) -> first()
     greater(0(),s(y)) -> second()
     greater(s(x),s(y)) -> greater(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     triple(x) -> if(le(x,x,double(x)),x,0(),0())
     if(false(),x,y,z) -> true()
     if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
     if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)
    Subterm Criterion Processor:
     simple projection:
      pi(greater#) = 1
     problem:
      DPs:
       
      TRS:
       le(0(),y,z) -> greater(y,z)
       le(s(x),0(),z) -> false()
       le(s(x),s(y),0()) -> false()
       le(s(x),s(y),s(z)) -> le(x,y,z)
       greater(x,0()) -> first()
       greater(0(),s(y)) -> second()
       greater(s(x),s(y)) -> greater(x,y)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       triple(x) -> if(le(x,x,double(x)),x,0(),0())
       if(false(),x,y,z) -> true()
       if(first(),x,y,z) -> if(le(s(x),y,s(z)),s(x),y,s(z))
       if(second(),x,y,z) -> if(le(s(x),s(y),z),s(x),s(y),z)
     Qed