YES
Time: 0.316

Problem:
 Equations:
  
 TRS:
  le(0(),y) -> true()
  le(s(x),0()) -> false()
  le(s(x),s(y)) -> le(x,y)
  minus(x,0()) -> x
  minus(s(x),s(y)) -> 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),s(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(x,0()) -> x
   minus(s(x),s(y)) -> 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),s(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(x,0()) -> x
    minus(s(x),s(y)) -> 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: 5
    #arcs: 13/64
    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(x,0()) -> x
     minus(s(x),s(y)) -> 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(x,0()) -> x
      minus(s(x),s(y)) -> 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(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
      S:
       
      AC-KBO Processor:
       argument filtering:
        pi(0) = []
        pi(le) = 0
        pi(true) = []
        pi(s) = [0]
        pi(false) = []
        pi(minus) = [0]
        pi(gcd{C,#}) = [0,1]
        pi(if_gcd#) = [1,2]
       precedence:
        minus > gcd{C,#} > if_gcd# ~ false ~ s ~ true ~ le ~ 0
        weight function:
         [if_gcd#](x0, x1, x2) = x1 + x2,
         
         [gcd{C,#}](x0, x1) = x0 + x1,
         
         [minus](x0, x1) = 2x0,
         
         [false] = 4,
         
         [s](x0) = 2x0 + 1,
         
         [true] = 4,
         
         [le](x0, x1) = x0,
         
         [0] = 1
         usable rules:
          minus(x,0()) -> x
          minus(s(x),s(y)) -> minus(x,y)
         problem:
          Equations#:
           
          DPs:
           
          Equations:
           
          TRS:
           minus(x,0()) -> x
           minus(s(x),s(y)) -> minus(x,y)
           le(0(),y) -> true()
           le(s(x),0()) -> false()
           le(s(x),s(y)) -> le(x,y)
          S:
           
         Qed
     
     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(x,0()) -> x
      minus(s(x),s(y)) -> 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(x,0()) -> x
       minus(s(x),s(y)) -> 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#) = 0
        precedence:
         s > le#
         weight function:
          [le#](x0, x1) = x0,
          
          [s](x0) = 4x0
          usable rules:
           
          problem:
           Equations#:
            
           DPs:
            
           Equations:
            
           TRS:
            
           S:
            
          Qed
      
      Equations#:
       
      DPs:
       minus#(s(x),s(y)) -> minus#(x,y)
      Equations:
       
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       minus(x,0()) -> x
       minus(s(x),s(y)) -> 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),s(y)) -> minus#(x,y)
       Equations:
        
       TRS:
        le(0(),y) -> true()
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
        minus(x,0()) -> x
        minus(s(x),s(y)) -> 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),s(y)) -> minus#(x,y)
        Equations:
         
        TRS:
         
        S:
         
        AC-KBO Processor:
         argument filtering:
          pi(s) = [0]
          pi(minus#) = 0
         precedence:
          s > minus#
          weight function:
           [minus#](x0, x1) = x0,
           
           [s](x0) = 4x0
           usable rules:
            
           problem:
            Equations#:
             
            DPs:
             
            Equations:
             
            TRS:
             
            S:
             
           Qed