YES

Problem:
 leq(0(),y) -> true()
 leq(s(x),0()) -> false()
 leq(s(x),s(y)) -> leq(x,y)
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 -(x,0()) -> x
 -(s(x),s(y)) -> -(x,y)
 mod(0(),y) -> 0()
 mod(s(x),0()) -> 0()
 mod(s(x),s(y)) -> if(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))

Proof:
 DP Processor:
  DPs:
   leq#(s(x),s(y)) -> leq#(x,y)
   -#(s(x),s(y)) -> -#(x,y)
   mod#(s(x),s(y)) -> -#(s(x),s(y))
   mod#(s(x),s(y)) -> mod#(-(s(x),s(y)),s(y))
   mod#(s(x),s(y)) -> leq#(y,x)
   mod#(s(x),s(y)) -> if#(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
  TRS:
   leq(0(),y) -> true()
   leq(s(x),0()) -> false()
   leq(s(x),s(y)) -> leq(x,y)
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   -(x,0()) -> x
   -(s(x),s(y)) -> -(x,y)
   mod(0(),y) -> 0()
   mod(s(x),0()) -> 0()
   mod(s(x),s(y)) -> if(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
  TDG Processor:
   DPs:
    leq#(s(x),s(y)) -> leq#(x,y)
    -#(s(x),s(y)) -> -#(x,y)
    mod#(s(x),s(y)) -> -#(s(x),s(y))
    mod#(s(x),s(y)) -> mod#(-(s(x),s(y)),s(y))
    mod#(s(x),s(y)) -> leq#(y,x)
    mod#(s(x),s(y)) -> if#(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
   TRS:
    leq(0(),y) -> true()
    leq(s(x),0()) -> false()
    leq(s(x),s(y)) -> leq(x,y)
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    -(x,0()) -> x
    -(s(x),s(y)) -> -(x,y)
    mod(0(),y) -> 0()
    mod(s(x),0()) -> 0()
    mod(s(x),s(y)) -> if(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
   graph:
    mod#(s(x),s(y)) -> mod#(-(s(x),s(y)),s(y)) ->
    mod#(s(x),s(y)) -> if#(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
    mod#(s(x),s(y)) -> mod#(-(s(x),s(y)),s(y)) ->
    mod#(s(x),s(y)) -> leq#(y,x)
    mod#(s(x),s(y)) -> mod#(-(s(x),s(y)),s(y)) ->
    mod#(s(x),s(y)) -> mod#(-(s(x),s(y)),s(y))
    mod#(s(x),s(y)) -> mod#(-(s(x),s(y)),s(y)) ->
    mod#(s(x),s(y)) -> -#(s(x),s(y))
    mod#(s(x),s(y)) -> -#(s(x),s(y)) -> -#(s(x),s(y)) -> -#(x,y)
    mod#(s(x),s(y)) -> leq#(y,x) -> leq#(s(x),s(y)) -> leq#(x,y)
    -#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y)
    leq#(s(x),s(y)) -> leq#(x,y) -> leq#(s(x),s(y)) -> leq#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 3
    #arcs: 8/36
    DPs:
     mod#(s(x),s(y)) -> mod#(-(s(x),s(y)),s(y))
    TRS:
     leq(0(),y) -> true()
     leq(s(x),0()) -> false()
     leq(s(x),s(y)) -> leq(x,y)
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     mod(0(),y) -> 0()
     mod(s(x),0()) -> 0()
     mod(s(x),s(y)) -> if(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
    Extended Uncurrying Processor:
     application symbol: leq
     symbol table:
      mod# ==> mod{0,#}/2
      mod ==> mod0/2
      - ==> -0/2
      if ==> if0/3
      false ==> false0/0
      s ==> s0/1 s1/2
      true ==> true0/0
      0 ==> 00/0 01/1
      
     uncurry-rules:
      leq(00(),x7) -> 01(x7)
      leq(s0(x10),x11) -> s1(x10,x11)
     eta-rules:
      
     problem:
      DPs:
       mod{0,#}(s0(x),s0(y)) -> mod{0,#}(-0(s0(x),s0(y)),s0(y))
      TRS:
       01(y) -> true0()
       s1(x,00()) -> false0()
       s1(x,s0(y)) -> leq(x,y)
       if0(true0(),x,y) -> x
       if0(false0(),x,y) -> y
       -0(x,00()) -> x
       -0(s0(x),s0(y)) -> -0(x,y)
       mod0(00(),y) -> 00()
       mod0(s0(x),00()) -> 00()
       mod0(s0(x),s0(y)) -> if0(leq(y,x),mod0(-0(s0(x),s0(y)),s0(y)),s0(x))
       leq(00(),x7) -> 01(x7)
       leq(s0(x10),x11) -> s1(x10,x11)
     Extended Uncurrying Processor:
      application symbol: mod{0,#}
      symbol table:
       mod0 ==> mod{0,0}/2
       -0 ==> -{0,0}/2 -0_mod{0,#}_1#/3
       if0 ==> if{0,0}/3
       false0 ==> false{0,0}/0
       s1 ==> s{1,0}/2
       s0 ==> s{0,0}/1 s0_mod{0,#}_1#/2
       true0 ==> true{0,0}/0
       01 ==> 0{1,0}/1
       00 ==> 0{0,0}/0
       leq ==> leq0/2
       
      uncurry-rules:
       mod{0,#}(-0(x32,x33),x34) -> -0_mod{0,#}_1#(x32,x33,x34)
       mod{0,#}(s0(x30),x31) -> s0_mod{0,#}_1#(x30,x31)
      eta-rules:
       mod{0,#}(-0(x,00()),x35) -> mod{0,#}(x,x35)
       mod{0,#}(-0(s0(x),s0(y)),x36) -> mod{0,#}(-0(x,y),x36)
      problem:
       DPs:
        mod{0,#}(-{0,0}(x32,x33),x34) -> -0_mod{0,#}_1#(x32,x33,x34)
        mod{0,#}(s{0,0}(x30),x31) -> s0_mod{0,#}_1#(x30,x31)
        -0_mod{0,#}_1#(x,0{0,0}(),x35) -> mod{0,#}(x,x35)
        -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),x36) -> -0_mod{0,#}_1#(x,y,x36)
        s0_mod{0,#}_1#(x,s{0,0}(y)) -> -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),s{0,0}(y))
       TRS:
        0{1,0}(y) -> true{0,0}()
        s{1,0}(x,0{0,0}()) -> false{0,0}()
        s{1,0}(x,s{0,0}(y)) -> leq0(x,y)
        if{0,0}(true{0,0}(),x,y) -> x
        if{0,0}(false{0,0}(),x,y) -> y
        -{0,0}(x,0{0,0}()) -> x
        -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
        mod{0,0}(0{0,0}(),y) -> 0{0,0}()
        mod{0,0}(s{0,0}(x),0{0,0}()) -> 0{0,0}()
        mod{0,0}(s{0,0}(x),s{0,0}(y)) ->
        if{0,0}(leq0(y,x),mod{0,0}(-{0,0}(s{0,0}(x),s{0,0}(y)),s{0,0}(y)),s{0,0}(x))
        leq0(0{0,0}(),x7) -> 0{1,0}(x7)
        leq0(s{0,0}(x10),x11) -> s{1,0}(x10,x11)
      Usable Rule Processor:
       DPs:
        mod{0,#}(-{0,0}(x32,x33),x34) -> -0_mod{0,#}_1#(x32,x33,x34)
        mod{0,#}(s{0,0}(x30),x31) -> s0_mod{0,#}_1#(x30,x31)
        -0_mod{0,#}_1#(x,0{0,0}(),x35) -> mod{0,#}(x,x35)
        -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),x36) -> -0_mod{0,#}_1#(x,y,x36)
        s0_mod{0,#}_1#(x,s{0,0}(y)) -> -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),s{0,0}(y))
       TRS:
        
       Arctic Interpretation Processor:
        dimension: 1
        usable rules:
         
        interpretation:
         [-0_mod{0,#}_1#](x0, x1, x2) = -8x0 + 0,
         
         [-{0,0}](x0, x1) = 1x0 + 9,
         
         [s0_mod{0,#}_1#](x0, x1) = x0 + 0,
         
         [s{0,0}](x0) = 8x0,
         
         [0{0,0}] = 0,
         
         [mod{0,#}](x0, x1) = -8x0 + 0
        orientation:
         mod{0,#}(-{0,0}(x32,x33),x34) = -7x32 + 1 >= -8x32 + 0 = -0_mod{0,#}_1#(x32,x33,x34)
         
         mod{0,#}(s{0,0}(x30),x31) = x30 + 0 >= x30 + 0 = s0_mod{0,#}_1#(x30,x31)
         
         -0_mod{0,#}_1#(x,0{0,0}(),x35) = -8x + 0 >= -8x + 0 = mod{0,#}(x,x35)
         
         -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),x36) = x + 0 >= -8x + 0 = -0_mod{0,#}_1#(x,y,x36)
         
         s0_mod{0,#}_1#(x,s{0,0}(y)) = x + 0 >= x + 0 = -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),s{0,0}(y))
        problem:
         DPs:
          mod{0,#}(s{0,0}(x30),x31) -> s0_mod{0,#}_1#(x30,x31)
          -0_mod{0,#}_1#(x,0{0,0}(),x35) -> mod{0,#}(x,x35)
          -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),x36) -> -0_mod{0,#}_1#(x,y,x36)
          s0_mod{0,#}_1#(x,s{0,0}(y)) -> -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),s{0,0}(y))
         TRS:
          
        Restore Modifier:
         DPs:
          mod{0,#}(s{0,0}(x30),x31) -> s0_mod{0,#}_1#(x30,x31)
          -0_mod{0,#}_1#(x,0{0,0}(),x35) -> mod{0,#}(x,x35)
          -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),x36) -> -0_mod{0,#}_1#(x,y,x36)
          s0_mod{0,#}_1#(x,s{0,0}(y)) -> -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),s{0,0}(y))
         TRS:
          0{1,0}(y) -> true{0,0}()
          s{1,0}(x,0{0,0}()) -> false{0,0}()
          s{1,0}(x,s{0,0}(y)) -> leq0(x,y)
          if{0,0}(true{0,0}(),x,y) -> x
          if{0,0}(false{0,0}(),x,y) -> y
          -{0,0}(x,0{0,0}()) -> x
          -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
          mod{0,0}(0{0,0}(),y) -> 0{0,0}()
          mod{0,0}(s{0,0}(x),0{0,0}()) -> 0{0,0}()
          mod{0,0}(s{0,0}(x),s{0,0}(y)) ->
          if{0,0}(leq0(y,x),mod{0,0}(-{0,0}(s{0,0}(x),s{0,0}(y)),s{0,0}(y)),s{0,0}(x))
          leq0(0{0,0}(),x7) -> 0{1,0}(x7)
          leq0(s{0,0}(x10),x11) -> s{1,0}(x10,x11)
         Usable Rule Processor:
          DPs:
           mod{0,#}(s{0,0}(x30),x31) -> s0_mod{0,#}_1#(x30,x31)
           -0_mod{0,#}_1#(x,0{0,0}(),x35) -> mod{0,#}(x,x35)
           -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),x36) -> -0_mod{0,#}_1#(x,y,x36)
           s0_mod{0,#}_1#(x,s{0,0}(y)) -> -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),s{0,0}(y))
          TRS:
           
          Matrix Interpretation Processor: dim=4
           
           usable rules:
            
           interpretation:
            [-0_mod{0,#}_1#](x0, x1, x2) = [0 1 1 0]x0,
            
            [s0_mod{0,#}_1#](x0, x1) = [1 1 1 1]x0 + [1],
            
                           [0 0 0 0]     [0]
                           [1 1 0 1]     [0]
            [s{0,0}](x0) = [0 0 1 0]x0 + [1]
                           [0 0 0 0]     [0],
            
                       [0]
                       [0]
            [0{0,0}] = [0]
                       [0],
            
            [mod{0,#}](x0, x1) = [0 1 1 0]x0
           orientation:
            mod{0,#}(s{0,0}(x30),x31) = [1 1 1 1]x30 + [1] >= [1 1 1 1]x30 + [1] = s0_mod{0,#}_1#(x30,x31)
            
            -0_mod{0,#}_1#(x,0{0,0}(),x35) = [0 1 1 0]x >= [0 1 1 0]x = mod{0,#}(x,x35)
            
            -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),x36) = [1 1 1 1]x + [1] >= [0 1 1 0]x = -0_mod{0,#}_1#(x,y,x36)
            
            s0_mod{0,#}_1#(x,s{0,0}(y)) = [1 1 1 1]x + [1] >= [1 1 1 1]x + [1] = -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),s{0,0}(y))
           problem:
            DPs:
             mod{0,#}(s{0,0}(x30),x31) -> s0_mod{0,#}_1#(x30,x31)
             -0_mod{0,#}_1#(x,0{0,0}(),x35) -> mod{0,#}(x,x35)
             s0_mod{0,#}_1#(x,s{0,0}(y)) -> -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),s{0,0}(y))
            TRS:
             
           Restore Modifier:
            DPs:
             mod{0,#}(s{0,0}(x30),x31) -> s0_mod{0,#}_1#(x30,x31)
             -0_mod{0,#}_1#(x,0{0,0}(),x35) -> mod{0,#}(x,x35)
             s0_mod{0,#}_1#(x,s{0,0}(y)) -> -0_mod{0,#}_1#(s{0,0}(x),s{0,0}(y),s{0,0}(y))
            TRS:
             0{1,0}(y) -> true{0,0}()
             s{1,0}(x,0{0,0}()) -> false{0,0}()
             s{1,0}(x,s{0,0}(y)) -> leq0(x,y)
             if{0,0}(true{0,0}(),x,y) -> x
             if{0,0}(false{0,0}(),x,y) -> y
             -{0,0}(x,0{0,0}()) -> x
             -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
             mod{0,0}(0{0,0}(),y) -> 0{0,0}()
             mod{0,0}(s{0,0}(x),0{0,0}()) -> 0{0,0}()
             mod{0,0}(s{0,0}(x),s{0,0}(y)) ->
             if{0,0}(leq0(y,x),mod{0,0}(-{0,0}(s{0,0}(x),s{0,0}(y)),s{0,0}(y)),s{0,0}(x))
             leq0(0{0,0}(),x7) -> 0{1,0}(x7)
             leq0(s{0,0}(x10),x11) -> s{1,0}(x10,x11)
            Bounds Processor:
             bound: 3
             enrichment: top-dp
             automaton:
              final states: {8,7,6}
              transitions:
               s0_mod{0,#}_1{#,1}(5,5) -> 6*
               -0_mod{0,#}_1{#,2}(20,19,18) -> 6*
               s{0,0,2}(5) -> 20,19,18
               s0_mod{0,#}_1{#,2}(5,5) -> 7*
               -0_mod{0,#}_1{#,3}(23,22,21) -> 7*
               s{0,0,3}(5) -> 23,22,21
               mod{0,#,0}(5,5) -> 6*
               s{0,0,0}(5) -> 5*
               s0_mod{0,#}_1{#,0}(5,5) -> 8*
               -0_mod{0,#}_1{#,0}(5,5,5) -> 7*
               0{0,0,0}() -> 5*
               0{1,0,0}(5) -> 5*
               true{0,0,0}() -> 5*
               s{1,0,0}(5,5) -> 5*
               false{0,0,0}() -> 5*
               leq{0,0}(5,5) -> 5*
               if{0,0,0}(5,5,5) -> 5*
               -{0,0,0}(5,5) -> 5*
               mod{0,0,0}(5,5) -> 5*
               -0_mod{0,#}_1{#,1}(14,13,12) -> 8*
               s{0,0,1}(5) -> 14,13,12
               mod{0,#,1}(5,5) -> 7*
             problem:
              DPs:
               
              TRS:
               0{1,0}(y) -> true{0,0}()
               s{1,0}(x,0{0,0}()) -> false{0,0}()
               s{1,0}(x,s{0,0}(y)) -> leq0(x,y)
               if{0,0}(true{0,0}(),x,y) -> x
               if{0,0}(false{0,0}(),x,y) -> y
               -{0,0}(x,0{0,0}()) -> x
               -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
               mod{0,0}(0{0,0}(),y) -> 0{0,0}()
               mod{0,0}(s{0,0}(x),0{0,0}()) -> 0{0,0}()
               mod{0,0}(s{0,0}(x),s{0,0}(y)) ->
               if{0,0}(leq0(y,x),mod{0,0}(-{0,0}(s{0,0}(x),s{0,0}(y)),s{0,0}(y)),s{0,0}(x))
               leq0(0{0,0}(),x7) -> 0{1,0}(x7)
               leq0(s{0,0}(x10),x11) -> s{1,0}(x10,x11)
             Qed
    
    DPs:
     leq#(s(x),s(y)) -> leq#(x,y)
    TRS:
     leq(0(),y) -> true()
     leq(s(x),0()) -> false()
     leq(s(x),s(y)) -> leq(x,y)
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     mod(0(),y) -> 0()
     mod(s(x),0()) -> 0()
     mod(s(x),s(y)) -> if(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
    Subterm Criterion Processor:
     simple projection:
      pi(leq#) = 1
     problem:
      DPs:
       
      TRS:
       leq(0(),y) -> true()
       leq(s(x),0()) -> false()
       leq(s(x),s(y)) -> leq(x,y)
       if(true(),x,y) -> x
       if(false(),x,y) -> y
       -(x,0()) -> x
       -(s(x),s(y)) -> -(x,y)
       mod(0(),y) -> 0()
       mod(s(x),0()) -> 0()
       mod(s(x),s(y)) -> if(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
     Qed
    
    DPs:
     -#(s(x),s(y)) -> -#(x,y)
    TRS:
     leq(0(),y) -> true()
     leq(s(x),0()) -> false()
     leq(s(x),s(y)) -> leq(x,y)
     if(true(),x,y) -> x
     if(false(),x,y) -> y
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     mod(0(),y) -> 0()
     mod(s(x),0()) -> 0()
     mod(s(x),s(y)) -> if(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
    Subterm Criterion Processor:
     simple projection:
      pi(-#) = 1
     problem:
      DPs:
       
      TRS:
       leq(0(),y) -> true()
       leq(s(x),0()) -> false()
       leq(s(x),s(y)) -> leq(x,y)
       if(true(),x,y) -> x
       if(false(),x,y) -> y
       -(x,0()) -> x
       -(s(x),s(y)) -> -(x,y)
       mod(0(),y) -> 0()
       mod(s(x),0()) -> 0()
       mod(s(x),s(y)) -> if(leq(y,x),mod(-(s(x),s(y)),s(y)),s(x))
     Qed