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)
   EDG 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#(first(),x,y,z) -> le#(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) -> 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#(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) ->
     le#(s(x),s(y),s(z)) -> le#(x,y,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) -> 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#(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#(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)) ->
     le#(s(x),s(y),s(z)) -> le#(x,y,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) -> 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#(second(),x,y,z) -> le#(s(x),s(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) -> double#(x) -> double#(s(x)) -> double#(x)
     triple#(x) -> le#(x,x,double(x)) ->
     le#(0(),y,z) -> greater#(y,z)
     triple#(x) -> le#(x,x,double(x)) ->
     le#(s(x),s(y),s(z)) -> le#(x,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#(0(),y,z) -> greater#(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) -> greater#(s(x),s(y)) -> greater#(x,y)
    SCC Processor:
     #sccs: 4
     #rules: 5
     #arcs: 22/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)
     LPO Processor:
      argument filtering:
       pi(0) = []
       pi(le) = []
       pi(greater) = []
       pi(s) = [0]
       pi(false) = []
       pi(first) = []
       pi(second) = []
       pi(double) = [0]
       pi(triple) = []
       pi(if) = []
       pi(true) = []
       pi(double#) = 0
      precedence:
       triple ~ le > if ~ greater > double > double# ~ true ~ second ~ first ~ false ~ s ~ 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)
     LPO Processor:
      argument filtering:
       pi(0) = []
       pi(le) = [1,2]
       pi(greater) = 1
       pi(s) = [0]
       pi(false) = []
       pi(first) = []
       pi(second) = []
       pi(double) = [0]
       pi(triple) = []
       pi(if) = []
       pi(true) = []
       pi(le#) = [2]
      precedence:
       double ~ 0 > triple > if ~ s > le# ~ true ~ second ~ first ~ false ~ greater ~ le
      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)
     LPO Processor:
      argument filtering:
       pi(0) = []
       pi(le) = []
       pi(greater) = []
       pi(s) = [0]
       pi(false) = []
       pi(first) = []
       pi(second) = []
       pi(double) = [0]
       pi(triple) = []
       pi(if) = []
       pi(true) = []
       pi(greater#) = [1]
      precedence:
       double > triple > if ~ le > s ~ greater > greater# ~ true ~ second ~ first ~ false ~ 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