YES
Time: 0.550

Problem:
 Equations:
  
 TRS:
  le(0(),y) -> true()
  le(s(x),0()) -> false()
  le(s(x),s(y)) -> le(x,y)
  minus(0(),y) -> 0()
  minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
  if_minus(true(),s(x),y) -> 0()
  if_minus(false(),s(x),y) -> s(minus(x,y))
  gcdC(0(),y) -> y
  gcdC(s(x),0()) -> s(x)
  gcdC(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
  if_gcd(true(),s(x),s(y)) -> gcdC(minus(x,y),s(y))
  if_gcd(false(),s(x),s(y)) -> gcdC(minus(y,x),s(x))

Proof:
 DP Processor:
  Equations#:
   
  DPs:
   le#(s(x),s(y)) -> le#(x,y)
   minus#(s(x),y) -> le#(s(x),y)
   minus#(s(x),y) -> if_minus#(le(s(x),y),s(x),y)
   if_minus#(false(),s(x),y) -> minus#(x,y)
   gcd{C,#}(s(x),s(y)) -> le#(y,x)
   gcd{C,#}(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
   if_gcd#(true(),s(x),s(y)) -> minus#(x,y)
   if_gcd#(true(),s(x),s(y)) -> gcd{C,#}(minus(x,y),s(y))
   if_gcd#(false(),s(x),s(y)) -> minus#(y,x)
   if_gcd#(false(),s(x),s(y)) -> gcd{C,#}(minus(y,x),s(x))
  Equations:
   
  TRS:
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   minus(0(),y) -> 0()
   minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
   if_minus(true(),s(x),y) -> 0()
   if_minus(false(),s(x),y) -> s(minus(x,y))
   gcdC(0(),y) -> y
   gcdC(s(x),0()) -> s(x)
   gcdC(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
   if_gcd(true(),s(x),s(y)) -> gcdC(minus(x,y),s(y))
   if_gcd(false(),s(x),s(y)) -> gcdC(minus(y,x),s(x))
  S:
   
  AC-EDG Processor:
   Equations#:
    
   DPs:
    le#(s(x),s(y)) -> le#(x,y)
    minus#(s(x),y) -> le#(s(x),y)
    minus#(s(x),y) -> if_minus#(le(s(x),y),s(x),y)
    if_minus#(false(),s(x),y) -> minus#(x,y)
    gcd{C,#}(s(x),s(y)) -> le#(y,x)
    gcd{C,#}(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
    if_gcd#(true(),s(x),s(y)) -> minus#(x,y)
    if_gcd#(true(),s(x),s(y)) -> gcd{C,#}(minus(x,y),s(y))
    if_gcd#(false(),s(x),s(y)) -> minus#(y,x)
    if_gcd#(false(),s(x),s(y)) -> gcd{C,#}(minus(y,x),s(x))
   Equations:
    
   TRS:
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    minus(0(),y) -> 0()
    minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
    if_minus(true(),s(x),y) -> 0()
    if_minus(false(),s(x),y) -> s(minus(x,y))
    gcdC(0(),y) -> y
    gcdC(s(x),0()) -> s(x)
    gcdC(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
    if_gcd(true(),s(x),s(y)) -> gcdC(minus(x,y),s(y))
    if_gcd(false(),s(x),s(y)) -> gcdC(minus(y,x),s(x))
   S:
    
   SCC Processor:
    #sccs: 3
    #rules: 6
    #arcs: 18/100
    Equations#:
     
    DPs:
     if_gcd#(false(),s(x),s(y)) -> gcd{C,#}(minus(y,x),s(x))
     gcd{C,#}(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
     if_gcd#(true(),s(x),s(y)) -> gcd{C,#}(minus(x,y),s(y))
    Equations:
     
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     minus(0(),y) -> 0()
     minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
     if_minus(true(),s(x),y) -> 0()
     if_minus(false(),s(x),y) -> s(minus(x,y))
     gcdC(0(),y) -> y
     gcdC(s(x),0()) -> s(x)
     gcdC(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
     if_gcd(true(),s(x),s(y)) -> gcdC(minus(x,y),s(y))
     if_gcd(false(),s(x),s(y)) -> gcdC(minus(y,x),s(x))
    S:
     
    AC-DP unlabeling:
     Equations#:
      
     DPs:
      if_gcd#(false(),s(x),s(y)) -> gcd{C,#}(minus(y,x),s(x))
      gcd{C,#}(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
      if_gcd#(true(),s(x),s(y)) -> gcd{C,#}(minus(x,y),s(y))
     Equations:
      
     TRS:
      le(0(),y) -> true()
      le(s(x),0()) -> false()
      le(s(x),s(y)) -> le(x,y)
      minus(0(),y) -> 0()
      minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
      if_minus(true(),s(x),y) -> 0()
      if_minus(false(),s(x),y) -> s(minus(x,y))
      gcdC(0(),y) -> y
      gcdC(s(x),0()) -> s(x)
      gcdC(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
      if_gcd(true(),s(x),s(y)) -> gcdC(minus(x,y),s(y))
      if_gcd(false(),s(x),s(y)) -> gcdC(minus(y,x),s(x))
     S:
      
     Usable Rule Processor:
      Equations#:
       
      DPs:
       if_gcd#(false(),s(x),s(y)) -> gcd{C,#}(minus(y,x),s(x))
       gcd{C,#}(s(x),s(y)) -> if_gcd#(le(y,x),s(x),s(y))
       if_gcd#(true(),s(x),s(y)) -> gcd{C,#}(minus(x,y),s(y))
      Equations:
       
      TRS:
       minus(0(),y) -> 0()
       minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
       if_minus(true(),s(x),y) -> 0()
       if_minus(false(),s(x),y) -> s(minus(x,y))
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       le(0(),y) -> true()
      S:
       
      AC-KBO Processor:
       argument filtering:
        pi(0) = []
        pi(le) = []
        pi(true) = []
        pi(s) = [0]
        pi(false) = []
        pi(minus) = 0
        pi(if_minus) = 1
        pi(gcd{C,#}) = [0,1]
        pi(if_gcd#) = [1,2]
       precedence:
        if_gcd# > gcd{C,#} ~ if_minus ~ minus ~ false ~ s ~ true ~ le ~ 0
        weight function:
         w0 = 1
         w(false) = 2
         w(gcd{C,#}) = w(s) = w(true) = w(le) = w(0) = 1
         w(if_gcd#) = w(if_minus) = w(minus) = 0
         usable rules:
          minus(0(),y) -> 0()
          minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
          if_minus(true(),s(x),y) -> 0()
          if_minus(false(),s(x),y) -> s(minus(x,y))
         problem:
          Equations#:
           
          DPs:
           
          Equations:
           
          TRS:
           minus(0(),y) -> 0()
           minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
           if_minus(true(),s(x),y) -> 0()
           if_minus(false(),s(x),y) -> s(minus(x,y))
           le(s(x),0()) -> false()
           le(s(x),s(y)) -> le(x,y)
           le(0(),y) -> true()
          S:
           
         Qed
     
     Equations#:
      
     DPs:
      minus#(s(x),y) -> if_minus#(le(s(x),y),s(x),y)
      if_minus#(false(),s(x),y) -> minus#(x,y)
     Equations:
      
     TRS:
      le(0(),y) -> true()
      le(s(x),0()) -> false()
      le(s(x),s(y)) -> le(x,y)
      minus(0(),y) -> 0()
      minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
      if_minus(true(),s(x),y) -> 0()
      if_minus(false(),s(x),y) -> s(minus(x,y))
      gcdC(0(),y) -> y
      gcdC(s(x),0()) -> s(x)
      gcdC(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
      if_gcd(true(),s(x),s(y)) -> gcdC(minus(x,y),s(y))
      if_gcd(false(),s(x),s(y)) -> gcdC(minus(y,x),s(x))
     S:
      
     AC-DP unlabeling:
      Equations#:
       
      DPs:
       minus#(s(x),y) -> if_minus#(le(s(x),y),s(x),y)
       if_minus#(false(),s(x),y) -> minus#(x,y)
      Equations:
       
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       minus(0(),y) -> 0()
       minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
       if_minus(true(),s(x),y) -> 0()
       if_minus(false(),s(x),y) -> s(minus(x,y))
       gcdC(0(),y) -> y
       gcdC(s(x),0()) -> s(x)
       gcdC(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
       if_gcd(true(),s(x),s(y)) -> gcdC(minus(x,y),s(y))
       if_gcd(false(),s(x),s(y)) -> gcdC(minus(y,x),s(x))
      S:
       
      Usable Rule Processor:
       Equations#:
        
       DPs:
        minus#(s(x),y) -> if_minus#(le(s(x),y),s(x),y)
        if_minus#(false(),s(x),y) -> minus#(x,y)
       Equations:
        
       TRS:
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
        le(0(),y) -> true()
       S:
        
       AC-KBO Processor:
        argument filtering:
         pi(0) = []
         pi(le) = []
         pi(true) = []
         pi(s) = [0]
         pi(false) = []
         pi(minus#) = 0
         pi(if_minus#) = 1
        precedence:
         if_minus# ~ minus# ~ false ~ s ~ true ~ le ~ 0
         weight function:
          w0 = 4
          w(if_minus#) = w(false) = w(true) = w(le) = w(0) = 4
          w(minus#) = 3
          w(s) = 0
          usable rules:
           
          problem:
           Equations#:
            
           DPs:
            minus#(s(x),y) -> if_minus#(le(s(x),y),s(x),y)
           Equations:
            
           TRS:
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            le(0(),y) -> true()
           S:
            
          Restore Modifier:
           Equations#:
            
           DPs:
            minus#(s(x),y) -> if_minus#(le(s(x),y),s(x),y)
           Equations:
            
           TRS:
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            le(0(),y) -> true()
           S:
            
           SCC Processor:
            #sccs: 0
            #rules: 0
            #arcs: 2/1
            
      
      Equations#:
       
      DPs:
       le#(s(x),s(y)) -> le#(x,y)
      Equations:
       
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       minus(0(),y) -> 0()
       minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
       if_minus(true(),s(x),y) -> 0()
       if_minus(false(),s(x),y) -> s(minus(x,y))
       gcdC(0(),y) -> y
       gcdC(s(x),0()) -> s(x)
       gcdC(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
       if_gcd(true(),s(x),s(y)) -> gcdC(minus(x,y),s(y))
       if_gcd(false(),s(x),s(y)) -> gcdC(minus(y,x),s(x))
      S:
       
      AC-DP unlabeling:
       Equations#:
        
       DPs:
        le#(s(x),s(y)) -> le#(x,y)
       Equations:
        
       TRS:
        le(0(),y) -> true()
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
        minus(0(),y) -> 0()
        minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
        if_minus(true(),s(x),y) -> 0()
        if_minus(false(),s(x),y) -> s(minus(x,y))
        gcdC(0(),y) -> y
        gcdC(s(x),0()) -> s(x)
        gcdC(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y))
        if_gcd(true(),s(x),s(y)) -> gcdC(minus(x,y),s(y))
        if_gcd(false(),s(x),s(y)) -> gcdC(minus(y,x),s(x))
       S:
        
       Usable Rule Processor:
        Equations#:
         
        DPs:
         le#(s(x),s(y)) -> le#(x,y)
        Equations:
         
        TRS:
         
        S:
         
        AC-KBO Processor:
         argument filtering:
          pi(s) = [0]
          pi(le#) = 1
         precedence:
          le# ~ s
          weight function:
           w0 = 1
           w(le#) = 7
           w(s) = 1
           usable rules:
            
           problem:
            Equations#:
             
            DPs:
             
            Equations:
             
            TRS:
             
            S:
             
           Qed