YES
Time: 0.807

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) = 1
        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:
        gcd{C,#} > minus > if_gcd# ~ if_minus ~ false ~ s ~ true ~ le ~ 0
        weight function:
         [if_gcd#](x0, x1, x2) = 6x1 + 6x2 + 1,
         
         [gcd{C,#}](x0, x1) = 6x0 + 6x1 + 4,
         
         [if_minus](x0, x1, x2) = 2x1 + 4,
         
         [minus](x0, x1) = 2x0 + 4,
         
         [false] = 2,
         
         [s](x0) = 2x0 + 6,
         
         [true] = 4,
         
         [le](x0, x1) = x1,
         
         [0] = 4
         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) = 0
         pi(true) = []
         pi(s) = [0]
         pi(false) = []
         pi(minus#) = 0
         pi(if_minus#) = 1
        precedence:
         s > if_minus# ~ minus# ~ false ~ true ~ le ~ 0
         weight function:
          [if_minus#](x0, x1, x2) = x1,
          
          [minus#](x0, x1) = x0,
          
          [false] = 4,
          
          [s](x0) = x0,
          
          [true] = 4,
          
          [le](x0, x1) = x0,
          
          [0] = 1
          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#) = 0
         precedence:
          s > le#
          weight function:
           [le#](x0, x1) = x0,
           
           [s](x0) = 4x0
           usable rules:
            
           problem:
            Equations#:
             
            DPs:
             
            Equations:
             
            TRS:
             
            S:
             
           Qed