YES
Time: 0.270

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