YES

Problem:
 min(0(),y) -> 0()
 min(x,0()) -> 0()
 min(s(x),s(y)) -> s(min(x,y))
 max(0(),y) -> y
 max(x,0()) -> x
 max(s(x),s(y)) -> s(max(x,y))
 +(0(),y) -> y
 +(s(x),y) -> s(+(x,y))
 -(x,0()) -> x
 -(s(x),s(y)) -> -(x,y)
 *(x,0()) -> 0()
 *(x,s(y)) -> +(x,*(x,y))
 p(s(x)) -> x
 f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))

Proof:
 DP Processor:
  DPs:
   min#(s(x),s(y)) -> min#(x,y)
   max#(s(x),s(y)) -> max#(x,y)
   +#(s(x),y) -> +#(x,y)
   -#(s(x),s(y)) -> -#(x,y)
   *#(x,s(y)) -> *#(x,y)
   *#(x,s(y)) -> +#(x,*(x,y))
   f#(s(x),s(y)) -> *#(s(x),s(y))
   f#(s(x),s(y)) -> max#(s(x),s(y))
   f#(s(x),s(y)) -> min#(s(x),s(y))
   f#(s(x),s(y)) -> -#(min(s(x),s(y)),max(s(x),s(y)))
   f#(s(x),s(y)) -> f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
  TRS:
   min(0(),y) -> 0()
   min(x,0()) -> 0()
   min(s(x),s(y)) -> s(min(x,y))
   max(0(),y) -> y
   max(x,0()) -> x
   max(s(x),s(y)) -> s(max(x,y))
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   -(x,0()) -> x
   -(s(x),s(y)) -> -(x,y)
   *(x,0()) -> 0()
   *(x,s(y)) -> +(x,*(x,y))
   p(s(x)) -> x
   f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
  TDG Processor:
   DPs:
    min#(s(x),s(y)) -> min#(x,y)
    max#(s(x),s(y)) -> max#(x,y)
    +#(s(x),y) -> +#(x,y)
    -#(s(x),s(y)) -> -#(x,y)
    *#(x,s(y)) -> *#(x,y)
    *#(x,s(y)) -> +#(x,*(x,y))
    f#(s(x),s(y)) -> *#(s(x),s(y))
    f#(s(x),s(y)) -> max#(s(x),s(y))
    f#(s(x),s(y)) -> min#(s(x),s(y))
    f#(s(x),s(y)) -> -#(min(s(x),s(y)),max(s(x),s(y)))
    f#(s(x),s(y)) -> f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
   TRS:
    min(0(),y) -> 0()
    min(x,0()) -> 0()
    min(s(x),s(y)) -> s(min(x,y))
    max(0(),y) -> y
    max(x,0()) -> x
    max(s(x),s(y)) -> s(max(x,y))
    +(0(),y) -> y
    +(s(x),y) -> s(+(x,y))
    -(x,0()) -> x
    -(s(x),s(y)) -> -(x,y)
    *(x,0()) -> 0()
    *(x,s(y)) -> +(x,*(x,y))
    p(s(x)) -> x
    f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
   graph:
    f#(s(x),s(y)) -> f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ->
    f#(s(x),s(y)) -> f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
    f#(s(x),s(y)) -> f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ->
    f#(s(x),s(y)) -> -#(min(s(x),s(y)),max(s(x),s(y)))
    f#(s(x),s(y)) -> f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ->
    f#(s(x),s(y)) -> min#(s(x),s(y))
    f#(s(x),s(y)) -> f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ->
    f#(s(x),s(y)) -> max#(s(x),s(y))
    f#(s(x),s(y)) -> f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y))) ->
    f#(s(x),s(y)) -> *#(s(x),s(y))
    f#(s(x),s(y)) -> *#(s(x),s(y)) -> *#(x,s(y)) -> +#(x,*(x,y))
    f#(s(x),s(y)) -> *#(s(x),s(y)) ->
    *#(x,s(y)) -> *#(x,y)
    f#(s(x),s(y)) -> -#(min(s(x),s(y)),max(s(x),s(y))) ->
    -#(s(x),s(y)) -> -#(x,y)
    f#(s(x),s(y)) -> max#(s(x),s(y)) ->
    max#(s(x),s(y)) -> max#(x,y)
    f#(s(x),s(y)) -> min#(s(x),s(y)) -> min#(s(x),s(y)) -> min#(x,y)
    *#(x,s(y)) -> *#(x,y) -> *#(x,s(y)) -> +#(x,*(x,y))
    *#(x,s(y)) -> *#(x,y) -> *#(x,s(y)) -> *#(x,y)
    *#(x,s(y)) -> +#(x,*(x,y)) -> +#(s(x),y) -> +#(x,y)
    -#(s(x),s(y)) -> -#(x,y) -> -#(s(x),s(y)) -> -#(x,y)
    +#(s(x),y) -> +#(x,y) -> +#(s(x),y) -> +#(x,y)
    max#(s(x),s(y)) -> max#(x,y) -> max#(s(x),s(y)) -> max#(x,y)
    min#(s(x),s(y)) -> min#(x,y) -> min#(s(x),s(y)) -> min#(x,y)
   SCC Processor:
    #sccs: 6
    #rules: 6
    #arcs: 17/121
    DPs:
     f#(s(x),s(y)) -> f#(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
    TRS:
     min(0(),y) -> 0()
     min(x,0()) -> 0()
     min(s(x),s(y)) -> s(min(x,y))
     max(0(),y) -> y
     max(x,0()) -> x
     max(s(x),s(y)) -> s(max(x,y))
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     *(x,0()) -> 0()
     *(x,s(y)) -> +(x,*(x,y))
     p(s(x)) -> x
     f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
    Extended Uncurrying Processor:
     application symbol: +
     symbol table:
      f# ==> f{0,#}/2
      f ==> f0/2
      p ==> p0/1
      * ==> *0/2
      - ==> -0/2
      max ==> max0/2
      s ==> s0/1 s1/2
      min ==> min0/2
      0 ==> 00/0 01/1
      
     uncurry-rules:
      +(00(),x16) -> 01(x16)
      +(s0(x18),x19) -> s1(x18,x19)
     eta-rules:
      
     problem:
      DPs:
       f{0,#}(s0(x),s0(y)) -> f{0,#}(-0(min0(s0(x),s0(y)),max0(s0(x),s0(y))),*0(s0(x),s0(y)))
      TRS:
       min0(00(),y) -> 00()
       min0(x,00()) -> 00()
       min0(s0(x),s0(y)) -> s0(min0(x,y))
       max0(00(),y) -> y
       max0(x,00()) -> x
       max0(s0(x),s0(y)) -> s0(max0(x,y))
       01(y) -> y
       s1(x,y) -> s0(+(x,y))
       -0(x,00()) -> x
       -0(s0(x),s0(y)) -> -0(x,y)
       *0(x,00()) -> 00()
       *0(x,s0(y)) -> +(x,*0(x,y))
       p0(s0(x)) -> x
       f0(s0(x),s0(y)) -> f0(-0(min0(s0(x),s0(y)),max0(s0(x),s0(y))),*0(s0(x),s0(y)))
       +(00(),x16) -> 01(x16)
       +(s0(x18),x19) -> s1(x18,x19)
     Extended Uncurrying Processor:
      application symbol: f{0,#}
      symbol table:
       f0 ==> f{0,0}/2
       p0 ==> p{0,0}/1
       *0 ==> *{0,0}/2
       -0 ==> -{0,0}/2 -0_f{0,#}_1#/3
       max0 ==> max{0,0}/2
       s1 ==> s{1,0}/2
       s0 ==> s{0,0}/1 s0_f{0,#}_1#/2
       min0 ==> min{0,0}/2
       01 ==> 0{1,0}/1
       00 ==> 0{0,0}/0
       + ==> +0/2
       
      uncurry-rules:
       f{0,#}(-0(x47,x48),x49) -> -0_f{0,#}_1#(x47,x48,x49)
       f{0,#}(s0(x45),x46) -> s0_f{0,#}_1#(x45,x46)
      eta-rules:
       f{0,#}(-0(x,00()),x50) -> f{0,#}(x,x50)
       f{0,#}(-0(s0(x),s0(y)),x51) -> f{0,#}(-0(x,y),x51)
      problem:
       DPs:
        f{0,#}(-{0,0}(x47,x48),x49) -> -0_f{0,#}_1#(x47,x48,x49)
        f{0,#}(s{0,0}(x45),x46) -> s0_f{0,#}_1#(x45,x46)
        -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
        -0_f{0,#}_1#(s{0,0}(x),s{0,0}(y),x51) -> -0_f{0,#}_1#(x,y,x51)
        s0_f{0,#}_1#(x,s{0,0}(y)) ->
        -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                     *{0,0}(s{0,0}(x),s{0,0}(y)))
       TRS:
        min{0,0}(0{0,0}(),y) -> 0{0,0}()
        min{0,0}(x,0{0,0}()) -> 0{0,0}()
        min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
        max{0,0}(0{0,0}(),y) -> y
        max{0,0}(x,0{0,0}()) -> x
        max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
        0{1,0}(y) -> y
        s{1,0}(x,y) -> s{0,0}(+0(x,y))
        -{0,0}(x,0{0,0}()) -> x
        -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
        *{0,0}(x,0{0,0}()) -> 0{0,0}()
        *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
        p{0,0}(s{0,0}(x)) -> x
        f{0,0}(s{0,0}(x),s{0,0}(y)) ->
        f{0,0}(-{0,0}(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y))),
               *{0,0}(s{0,0}(x),s{0,0}(y)))
        +0(0{0,0}(),x16) -> 0{1,0}(x16)
        +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
      Usable Rule Processor:
       DPs:
        f{0,#}(-{0,0}(x47,x48),x49) -> -0_f{0,#}_1#(x47,x48,x49)
        f{0,#}(s{0,0}(x45),x46) -> s0_f{0,#}_1#(x45,x46)
        -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
        -0_f{0,#}_1#(s{0,0}(x),s{0,0}(y),x51) -> -0_f{0,#}_1#(x,y,x51)
        s0_f{0,#}_1#(x,s{0,0}(y)) ->
        -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                     *{0,0}(s{0,0}(x),s{0,0}(y)))
       TRS:
        *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
        +0(0{0,0}(),x16) -> 0{1,0}(x16)
        +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
        *{0,0}(x,0{0,0}()) -> 0{0,0}()
        0{1,0}(y) -> y
        s{1,0}(x,y) -> s{0,0}(+0(x,y))
        max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
        max{0,0}(0{0,0}(),y) -> y
        max{0,0}(x,0{0,0}()) -> x
        min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
        min{0,0}(0{0,0}(),y) -> 0{0,0}()
        min{0,0}(x,0{0,0}()) -> 0{0,0}()
       Arctic Interpretation Processor:
        dimension: 1
        usable rules:
         min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
         min{0,0}(0{0,0}(),y) -> 0{0,0}()
         min{0,0}(x,0{0,0}()) -> 0{0,0}()
        interpretation:
         [*{0,0}](x0, x1) = x0 + -5x1 + 1,
         
         [-0_f{0,#}_1#](x0, x1, x2) = x0 + 0,
         
         [-{0,0}](x0, x1) = 2x0 + 2x1 + 2,
         
         [max{0,0}](x0, x1) = 1x0 + 5x1 + -5,
         
         [s{1,0}](x0, x1) = x0 + x1 + 0,
         
         [s0_f{0,#}_1#](x0, x1) = x0 + 1,
         
         [s{0,0}](x0) = x0 + 1,
         
         [min{0,0}](x0, x1) = x0 + 0,
         
         [0{1,0}](x0) = -12x0 + 2,
         
         [0{0,0}] = 0,
         
         [+0](x0, x1) = x0 + x1 + 0,
         
         [f{0,#}](x0, x1) = x0 + 0
        orientation:
         f{0,#}(-{0,0}(x47,x48),x49) = 2x47 + 2x48 + 2 >= x47 + 0 = -0_f{0,#}_1#(x47,x48,x49)
         
         f{0,#}(s{0,0}(x45),x46) = x45 + 1 >= x45 + 1 = s0_f{0,#}_1#(x45,x46)
         
         -0_f{0,#}_1#(x,0{0,0}(),x50) = x + 0 >= x + 0 = f{0,#}(x,x50)
         
         -0_f{0,#}_1#(s{0,0}(x),s{0,0}(y),x51) = x + 1 >= x + 0 = -0_f{0,#}_1#(x,y,x51)
         
         s0_f{0,#}_1#(x,s{0,0}(y)) = x + 1 >= x + 1 = -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
             *{0,0}(s{0,0}(x),s{0,0}(y)))
         
         *{0,0}(x,s{0,0}(y)) = x + -5y + 1 >= x + -5y + 1 = +0(x,*{0,0}(x,y))
         
         +0(0{0,0}(),x16) = x16 + 0 >= -12x16 + 2 = 0{1,0}(x16)
         
         +0(s{0,0}(x18),x19) = x18 + x19 + 1 >= x18 + x19 + 0 = s{1,0}(x18,x19)
         
         *{0,0}(x,0{0,0}()) = x + 1 >= 0 = 0{0,0}()
         
         0{1,0}(y) = -12y + 2 >= y = y
         
         s{1,0}(x,y) = x + y + 0 >= x + y + 1 = s{0,0}(+0(x,y))
         
         max{0,0}(s{0,0}(x),s{0,0}(y)) = 1x + 5y + 6 >= 1x + 5y + 1 = s{0,0}(max{0,0}(x,y))
         
         max{0,0}(0{0,0}(),y) = 5y + 1 >= y = y
         
         max{0,0}(x,0{0,0}()) = 1x + 5 >= x = x
         
         min{0,0}(s{0,0}(x),s{0,0}(y)) = x + 1 >= x + 1 = s{0,0}(min{0,0}(x,y))
         
         min{0,0}(0{0,0}(),y) = 0 >= 0 = 0{0,0}()
         
         min{0,0}(x,0{0,0}()) = x + 0 >= 0 = 0{0,0}()
        problem:
         DPs:
          f{0,#}(s{0,0}(x45),x46) -> s0_f{0,#}_1#(x45,x46)
          -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
          -0_f{0,#}_1#(s{0,0}(x),s{0,0}(y),x51) -> -0_f{0,#}_1#(x,y,x51)
          s0_f{0,#}_1#(x,s{0,0}(y)) ->
          -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                       *{0,0}(s{0,0}(x),s{0,0}(y)))
         TRS:
          *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
          +0(0{0,0}(),x16) -> 0{1,0}(x16)
          +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
          *{0,0}(x,0{0,0}()) -> 0{0,0}()
          0{1,0}(y) -> y
          s{1,0}(x,y) -> s{0,0}(+0(x,y))
          max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
          max{0,0}(0{0,0}(),y) -> y
          max{0,0}(x,0{0,0}()) -> x
          min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
          min{0,0}(0{0,0}(),y) -> 0{0,0}()
          min{0,0}(x,0{0,0}()) -> 0{0,0}()
        Restore Modifier:
         DPs:
          f{0,#}(s{0,0}(x45),x46) -> s0_f{0,#}_1#(x45,x46)
          -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
          -0_f{0,#}_1#(s{0,0}(x),s{0,0}(y),x51) -> -0_f{0,#}_1#(x,y,x51)
          s0_f{0,#}_1#(x,s{0,0}(y)) ->
          -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                       *{0,0}(s{0,0}(x),s{0,0}(y)))
         TRS:
          min{0,0}(0{0,0}(),y) -> 0{0,0}()
          min{0,0}(x,0{0,0}()) -> 0{0,0}()
          min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
          max{0,0}(0{0,0}(),y) -> y
          max{0,0}(x,0{0,0}()) -> x
          max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
          0{1,0}(y) -> y
          s{1,0}(x,y) -> s{0,0}(+0(x,y))
          -{0,0}(x,0{0,0}()) -> x
          -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
          *{0,0}(x,0{0,0}()) -> 0{0,0}()
          *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
          p{0,0}(s{0,0}(x)) -> x
          f{0,0}(s{0,0}(x),s{0,0}(y)) ->
          f{0,0}(-{0,0}(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y))),
                 *{0,0}(s{0,0}(x),s{0,0}(y)))
          +0(0{0,0}(),x16) -> 0{1,0}(x16)
          +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
         Usable Rule Processor:
          DPs:
           f{0,#}(s{0,0}(x45),x46) -> s0_f{0,#}_1#(x45,x46)
           -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
           -0_f{0,#}_1#(s{0,0}(x),s{0,0}(y),x51) -> -0_f{0,#}_1#(x,y,x51)
           s0_f{0,#}_1#(x,s{0,0}(y)) ->
           -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                        *{0,0}(s{0,0}(x),s{0,0}(y)))
          TRS:
           *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
           +0(0{0,0}(),x16) -> 0{1,0}(x16)
           +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
           *{0,0}(x,0{0,0}()) -> 0{0,0}()
           0{1,0}(y) -> y
           s{1,0}(x,y) -> s{0,0}(+0(x,y))
           max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
           max{0,0}(0{0,0}(),y) -> y
           max{0,0}(x,0{0,0}()) -> x
           min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
           min{0,0}(0{0,0}(),y) -> 0{0,0}()
           min{0,0}(x,0{0,0}()) -> 0{0,0}()
          Matrix Interpretation Processor: dim=1
           
           usable rules:
            max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
            max{0,0}(0{0,0}(),y) -> y
            max{0,0}(x,0{0,0}()) -> x
            min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
            min{0,0}(0{0,0}(),y) -> 0{0,0}()
            min{0,0}(x,0{0,0}()) -> 0{0,0}()
           interpretation:
            [*{0,0}](x0, x1) = 7/2x0 + 2x1 + 2,
            
            [-0_f{0,#}_1#](x0, x1, x2) = 1/2x0 + 1,
            
            [max{0,0}](x0, x1) = 2x0 + 5/2x1,
            
            [s{1,0}](x0, x1) = 0,
            
            [s0_f{0,#}_1#](x0, x1) = x0 + 5/2,
            
            [s{0,0}](x0) = 2x0 + 3,
            
            [min{0,0}](x0, x1) = x0,
            
            [0{1,0}](x0) = 0,
            
            [0{0,0}] = 0,
            
            [+0](x0, x1) = 2x0 + 7/2,
            
            [f{0,#}](x0, x1) = 1/2x0 + 1
           orientation:
            f{0,#}(s{0,0}(x45),x46) = x45 + 5/2 >= x45 + 5/2 = s0_f{0,#}_1#(x45,x46)
            
            -0_f{0,#}_1#(x,0{0,0}(),x50) = 1/2x + 1 >= 1/2x + 1 = f{0,#}(x,x50)
            
            -0_f{0,#}_1#(s{0,0}(x),s{0,0}(y),x51) = x + 5/2 >= 1/2x + 1 = -0_f{0,#}_1#(x,y,x51)
            
            s0_f{0,#}_1#(x,s{0,0}(y)) = x + 5/2 >= x + 5/2 = -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
             *{0,0}(s{0,0}(x),s{0,0}(y)))
            
            *{0,0}(x,s{0,0}(y)) = 7/2x + 4y + 8 >= 2x + 7/2 = +0(x,*{0,0}(x,y))
            
            +0(0{0,0}(),x16) = 7/2 >= 0 = 0{1,0}(x16)
            
            +0(s{0,0}(x18),x19) = 4x18 + 19/2 >= 0 = s{1,0}(x18,x19)
            
            *{0,0}(x,0{0,0}()) = 7/2x + 2 >= 0 = 0{0,0}()
            
            0{1,0}(y) = 0 >= y = y
            
            s{1,0}(x,y) = 0 >= 4x + 10 = s{0,0}(+0(x,y))
            
            max{0,0}(s{0,0}(x),s{0,0}(y)) = 4x + 5y + 27/2 >= 4x + 5y + 3 = s{0,0}(max{0,0}(x,y))
            
            max{0,0}(0{0,0}(),y) = 5/2y >= y = y
            
            max{0,0}(x,0{0,0}()) = 2x >= x = x
            
            min{0,0}(s{0,0}(x),s{0,0}(y)) = 2x + 3 >= 2x + 3 = s{0,0}(min{0,0}(x,y))
            
            min{0,0}(0{0,0}(),y) = 0 >= 0 = 0{0,0}()
            
            min{0,0}(x,0{0,0}()) = x >= 0 = 0{0,0}()
           problem:
            DPs:
             f{0,#}(s{0,0}(x45),x46) -> s0_f{0,#}_1#(x45,x46)
             -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
             s0_f{0,#}_1#(x,s{0,0}(y)) ->
             -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                          *{0,0}(s{0,0}(x),s{0,0}(y)))
            TRS:
             *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
             +0(0{0,0}(),x16) -> 0{1,0}(x16)
             +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
             *{0,0}(x,0{0,0}()) -> 0{0,0}()
             0{1,0}(y) -> y
             s{1,0}(x,y) -> s{0,0}(+0(x,y))
             max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
             max{0,0}(0{0,0}(),y) -> y
             max{0,0}(x,0{0,0}()) -> x
             min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
             min{0,0}(0{0,0}(),y) -> 0{0,0}()
             min{0,0}(x,0{0,0}()) -> 0{0,0}()
           Restore Modifier:
            DPs:
             f{0,#}(s{0,0}(x45),x46) -> s0_f{0,#}_1#(x45,x46)
             -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
             s0_f{0,#}_1#(x,s{0,0}(y)) ->
             -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                          *{0,0}(s{0,0}(x),s{0,0}(y)))
            TRS:
             min{0,0}(0{0,0}(),y) -> 0{0,0}()
             min{0,0}(x,0{0,0}()) -> 0{0,0}()
             min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
             max{0,0}(0{0,0}(),y) -> y
             max{0,0}(x,0{0,0}()) -> x
             max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
             0{1,0}(y) -> y
             s{1,0}(x,y) -> s{0,0}(+0(x,y))
             -{0,0}(x,0{0,0}()) -> x
             -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
             *{0,0}(x,0{0,0}()) -> 0{0,0}()
             *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
             p{0,0}(s{0,0}(x)) -> x
             f{0,0}(s{0,0}(x),s{0,0}(y)) ->
             f{0,0}(-{0,0}(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y))),
                    *{0,0}(s{0,0}(x),s{0,0}(y)))
             +0(0{0,0}(),x16) -> 0{1,0}(x16)
             +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
            Usable Rule Processor:
             DPs:
              f{0,#}(s{0,0}(x45),x46) -> s0_f{0,#}_1#(x45,x46)
              -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
              s0_f{0,#}_1#(x,s{0,0}(y)) ->
              -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                           *{0,0}(s{0,0}(x),s{0,0}(y)))
             TRS:
              *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
              +0(0{0,0}(),x16) -> 0{1,0}(x16)
              +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
              *{0,0}(x,0{0,0}()) -> 0{0,0}()
              0{1,0}(y) -> y
              s{1,0}(x,y) -> s{0,0}(+0(x,y))
              max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
              max{0,0}(0{0,0}(),y) -> y
              max{0,0}(x,0{0,0}()) -> x
              min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
              min{0,0}(0{0,0}(),y) -> 0{0,0}()
              min{0,0}(x,0{0,0}()) -> 0{0,0}()
             Arctic Interpretation Processor:
              dimension: 1
              usable rules:
               *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
               +0(0{0,0}(),x16) -> 0{1,0}(x16)
               +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
               *{0,0}(x,0{0,0}()) -> 0{0,0}()
               0{1,0}(y) -> y
               s{1,0}(x,y) -> s{0,0}(+0(x,y))
               max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
               max{0,0}(0{0,0}(),y) -> y
               max{0,0}(x,0{0,0}()) -> x
              interpretation:
               [*{0,0}](x0, x1) = 3x0 + 3,
               
               [-0_f{0,#}_1#](x0, x1, x2) = 3x1 + x2,
               
               [max{0,0}](x0, x1) = x0 + 1x1 + 0,
               
               [s{1,0}](x0, x1) = 0,
               
               [s0_f{0,#}_1#](x0, x1) = 4,
               
               [s{0,0}](x0) = 0,
               
               [min{0,0}](x0, x1) = 2x1 + 0,
               
               [0{1,0}](x0) = x0,
               
               [0{0,0}] = 2,
               
               [+0](x0, x1) = x1 + 0,
               
               [f{0,#}](x0, x1) = x1 + 5
              orientation:
               f{0,#}(s{0,0}(x45),x46) = x46 + 5 >= 4 = s0_f{0,#}_1#(x45,x46)
               
               -0_f{0,#}_1#(x,0{0,0}(),x50) = x50 + 5 >= x50 + 5 = f{0,#}(x,x50)
               
               s0_f{0,#}_1#(x,s{0,0}(y)) = 4 >= 4 = -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
             *{0,0}(s{0,0}(x),s{0,0}(y)))
               
               *{0,0}(x,s{0,0}(y)) = 3x + 3 >= 3x + 3 = +0(x,*{0,0}(x,y))
               
               +0(0{0,0}(),x16) = x16 + 0 >= x16 = 0{1,0}(x16)
               
               +0(s{0,0}(x18),x19) = x19 + 0 >= 0 = s{1,0}(x18,x19)
               
               *{0,0}(x,0{0,0}()) = 3x + 3 >= 2 = 0{0,0}()
               
               0{1,0}(y) = y >= y = y
               
               s{1,0}(x,y) = 0 >= 0 = s{0,0}(+0(x,y))
               
               max{0,0}(s{0,0}(x),s{0,0}(y)) = 1 >= 0 = s{0,0}(max{0,0}(x,y))
               
               max{0,0}(0{0,0}(),y) = 1y + 2 >= y = y
               
               max{0,0}(x,0{0,0}()) = x + 3 >= x = x
               
               min{0,0}(s{0,0}(x),s{0,0}(y)) = 2 >= 0 = s{0,0}(min{0,0}(x,y))
               
               min{0,0}(0{0,0}(),y) = 2y + 0 >= 2 = 0{0,0}()
               
               min{0,0}(x,0{0,0}()) = 4 >= 2 = 0{0,0}()
              problem:
               DPs:
                -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
                s0_f{0,#}_1#(x,s{0,0}(y)) ->
                -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                             *{0,0}(s{0,0}(x),s{0,0}(y)))
               TRS:
                *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
                +0(0{0,0}(),x16) -> 0{1,0}(x16)
                +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
                *{0,0}(x,0{0,0}()) -> 0{0,0}()
                0{1,0}(y) -> y
                s{1,0}(x,y) -> s{0,0}(+0(x,y))
                max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
                max{0,0}(0{0,0}(),y) -> y
                max{0,0}(x,0{0,0}()) -> x
                min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
                min{0,0}(0{0,0}(),y) -> 0{0,0}()
                min{0,0}(x,0{0,0}()) -> 0{0,0}()
              Restore Modifier:
               DPs:
                -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
                s0_f{0,#}_1#(x,s{0,0}(y)) ->
                -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                             *{0,0}(s{0,0}(x),s{0,0}(y)))
               TRS:
                min{0,0}(0{0,0}(),y) -> 0{0,0}()
                min{0,0}(x,0{0,0}()) -> 0{0,0}()
                min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
                max{0,0}(0{0,0}(),y) -> y
                max{0,0}(x,0{0,0}()) -> x
                max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
                0{1,0}(y) -> y
                s{1,0}(x,y) -> s{0,0}(+0(x,y))
                -{0,0}(x,0{0,0}()) -> x
                -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
                *{0,0}(x,0{0,0}()) -> 0{0,0}()
                *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
                p{0,0}(s{0,0}(x)) -> x
                f{0,0}(s{0,0}(x),s{0,0}(y)) ->
                f{0,0}(-{0,0}(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y))),
                       *{0,0}(s{0,0}(x),s{0,0}(y)))
                +0(0{0,0}(),x16) -> 0{1,0}(x16)
                +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
               Usable Rule Processor:
                DPs:
                 -0_f{0,#}_1#(x,0{0,0}(),x50) -> f{0,#}(x,x50)
                 s0_f{0,#}_1#(x,s{0,0}(y)) ->
                 -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                              *{0,0}(s{0,0}(x),s{0,0}(y)))
                TRS:
                 *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
                 +0(0{0,0}(),x16) -> 0{1,0}(x16)
                 +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
                 *{0,0}(x,0{0,0}()) -> 0{0,0}()
                 0{1,0}(y) -> y
                 s{1,0}(x,y) -> s{0,0}(+0(x,y))
                 max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
                 max{0,0}(0{0,0}(),y) -> y
                 max{0,0}(x,0{0,0}()) -> x
                 min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
                 min{0,0}(0{0,0}(),y) -> 0{0,0}()
                 min{0,0}(x,0{0,0}()) -> 0{0,0}()
                Arctic Interpretation Processor:
                 dimension: 1
                 usable rules:
                  *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
                  +0(0{0,0}(),x16) -> 0{1,0}(x16)
                  +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
                  *{0,0}(x,0{0,0}()) -> 0{0,0}()
                  0{1,0}(y) -> y
                  s{1,0}(x,y) -> s{0,0}(+0(x,y))
                  max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
                  max{0,0}(0{0,0}(),y) -> y
                  max{0,0}(x,0{0,0}()) -> x
                 interpretation:
                  [*{0,0}](x0, x1) = 4x0 + x1 + 2,
                  
                  [-0_f{0,#}_1#](x0, x1, x2) = 1x1 + x2 + 4,
                  
                  [max{0,0}](x0, x1) = 4x0 + 3x1 + 2,
                  
                  [s{1,0}](x0, x1) = x1 + 2,
                  
                  [s0_f{0,#}_1#](x0, x1) = 5x0 + 4x1 + 5,
                  
                  [s{0,0}](x0) = x0 + 0,
                  
                  [min{0,0}](x0, x1) = x0,
                  
                  [0{1,0}](x0) = x0 + 1,
                  
                  [0{0,0}] = 2,
                  
                  [+0](x0, x1) = x1 + 2,
                  
                  [f{0,#}](x0, x1) = 0
                 orientation:
                  -0_f{0,#}_1#(x,0{0,0}(),x50) = x50 + 4 >= 0 = f{0,#}(x,x50)
                  
                  s0_f{0,#}_1#(x,s{0,0}(y)) = 5x + 4y + 5 >= 5x + 4y + 5 = -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
             *{0,0}(s{0,0}(x),s{0,0}(y)))
                  
                  *{0,0}(x,s{0,0}(y)) = 4x + y + 2 >= 4x + y + 2 = +0(x,*{0,0}(x,y))
                  
                  +0(0{0,0}(),x16) = x16 + 2 >= x16 + 1 = 0{1,0}(x16)
                  
                  +0(s{0,0}(x18),x19) = x19 + 2 >= x19 + 2 = s{1,0}(x18,x19)
                  
                  *{0,0}(x,0{0,0}()) = 4x + 2 >= 2 = 0{0,0}()
                  
                  0{1,0}(y) = y + 1 >= y = y
                  
                  s{1,0}(x,y) = y + 2 >= y + 2 = s{0,0}(+0(x,y))
                  
                  max{0,0}(s{0,0}(x),s{0,0}(y)) = 4x + 3y + 4 >= 4x + 3y + 2 = s{0,0}(max{0,0}(x,y))
                  
                  max{0,0}(0{0,0}(),y) = 3y + 6 >= y = y
                  
                  max{0,0}(x,0{0,0}()) = 4x + 5 >= x = x
                  
                  min{0,0}(s{0,0}(x),s{0,0}(y)) = x + 0 >= x + 0 = s{0,0}(min{0,0}(x,y))
                  
                  min{0,0}(0{0,0}(),y) = 2 >= 2 = 0{0,0}()
                  
                  min{0,0}(x,0{0,0}()) = x >= 2 = 0{0,0}()
                 problem:
                  DPs:
                   s0_f{0,#}_1#(x,s{0,0}(y)) ->
                   -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                                *{0,0}(s{0,0}(x),s{0,0}(y)))
                  TRS:
                   *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
                   +0(0{0,0}(),x16) -> 0{1,0}(x16)
                   +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
                   *{0,0}(x,0{0,0}()) -> 0{0,0}()
                   0{1,0}(y) -> y
                   s{1,0}(x,y) -> s{0,0}(+0(x,y))
                   max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
                   max{0,0}(0{0,0}(),y) -> y
                   max{0,0}(x,0{0,0}()) -> x
                   min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
                   min{0,0}(0{0,0}(),y) -> 0{0,0}()
                   min{0,0}(x,0{0,0}()) -> 0{0,0}()
                 Restore Modifier:
                  DPs:
                   s0_f{0,#}_1#(x,s{0,0}(y)) ->
                   -0_f{0,#}_1#(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y)),
                                *{0,0}(s{0,0}(x),s{0,0}(y)))
                  TRS:
                   min{0,0}(0{0,0}(),y) -> 0{0,0}()
                   min{0,0}(x,0{0,0}()) -> 0{0,0}()
                   min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
                   max{0,0}(0{0,0}(),y) -> y
                   max{0,0}(x,0{0,0}()) -> x
                   max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
                   0{1,0}(y) -> y
                   s{1,0}(x,y) -> s{0,0}(+0(x,y))
                   -{0,0}(x,0{0,0}()) -> x
                   -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
                   *{0,0}(x,0{0,0}()) -> 0{0,0}()
                   *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
                   p{0,0}(s{0,0}(x)) -> x
                   f{0,0}(s{0,0}(x),s{0,0}(y)) ->
                   f{0,0}(-{0,0}(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y))),
                          *{0,0}(s{0,0}(x),s{0,0}(y)))
                   +0(0{0,0}(),x16) -> 0{1,0}(x16)
                   +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
                  Bounds Processor:
                   bound: 1
                   enrichment: top-dp
                   automaton:
                    final states: {2}
                    transitions:
                     -{0,0,0}(1,1) -> 1*
                     p{0,0,0}(1) -> 1*
                     f{0,0,0}(1,1) -> 1*
                     -0_f{0,#}_1{#,1}(13,10,7) -> 2*
                     min{0,0,1}(12,11) -> 13*
                     min{0,0,1}(1,1) -> 24*
                     s{0,0,1}(30) -> 28,7
                     s{0,0,1}(25) -> 25,10
                     s{0,0,1}(24) -> 24,13
                     s{0,0,1}(1) -> 12,11,9,8,6,5
                     max{0,0,1}(9,8) -> 10*
                     max{0,0,1}(1,1) -> 25*
                     *{0,0,1}(6,1) -> 28*
                     *{0,0,1}(6,5) -> 7*
                     +{0,1}(6,28) -> 28,7
                     +{0,1}(1,28) -> 30*
                     s{1,0,1}(1,28) -> 30,28,7
                     0{0,0,1}() -> 28,24
                     0{1,0,1}(28) -> 30*
                     s0_f{0,#}_1{#,0}(1,1) -> 2*
                     s{0,0,0}(1) -> 1*
                     -0_f{0,#}_1{#,0}(1,1,1) -> 1*
                     min{0,0,0}(1,1) -> 1*
                     max{0,0,0}(1,1) -> 1*
                     *{0,0,0}(1,1) -> 1*
                     0{0,0,0}() -> 1*
                     0{1,0,0}(1) -> 1*
                     s{1,0,0}(1,1) -> 1*
                     +{0,0}(1,1) -> 1*
                     1 -> 25*
                     28 -> 30*
                   problem:
                    DPs:
                     
                    TRS:
                     min{0,0}(0{0,0}(),y) -> 0{0,0}()
                     min{0,0}(x,0{0,0}()) -> 0{0,0}()
                     min{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(min{0,0}(x,y))
                     max{0,0}(0{0,0}(),y) -> y
                     max{0,0}(x,0{0,0}()) -> x
                     max{0,0}(s{0,0}(x),s{0,0}(y)) -> s{0,0}(max{0,0}(x,y))
                     0{1,0}(y) -> y
                     s{1,0}(x,y) -> s{0,0}(+0(x,y))
                     -{0,0}(x,0{0,0}()) -> x
                     -{0,0}(s{0,0}(x),s{0,0}(y)) -> -{0,0}(x,y)
                     *{0,0}(x,0{0,0}()) -> 0{0,0}()
                     *{0,0}(x,s{0,0}(y)) -> +0(x,*{0,0}(x,y))
                     p{0,0}(s{0,0}(x)) -> x
                     f{0,0}(s{0,0}(x),s{0,0}(y)) ->
                     f{0,0}(-{0,0}(min{0,0}(s{0,0}(x),s{0,0}(y)),max{0,0}(s{0,0}(x),s{0,0}(y))),
                            *{0,0}(s{0,0}(x),s{0,0}(y)))
                     +0(0{0,0}(),x16) -> 0{1,0}(x16)
                     +0(s{0,0}(x18),x19) -> s{1,0}(x18,x19)
                   Qed
    
    DPs:
     -#(s(x),s(y)) -> -#(x,y)
    TRS:
     min(0(),y) -> 0()
     min(x,0()) -> 0()
     min(s(x),s(y)) -> s(min(x,y))
     max(0(),y) -> y
     max(x,0()) -> x
     max(s(x),s(y)) -> s(max(x,y))
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     *(x,0()) -> 0()
     *(x,s(y)) -> +(x,*(x,y))
     p(s(x)) -> x
     f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(-#) = 1
     problem:
      DPs:
       
      TRS:
       min(0(),y) -> 0()
       min(x,0()) -> 0()
       min(s(x),s(y)) -> s(min(x,y))
       max(0(),y) -> y
       max(x,0()) -> x
       max(s(x),s(y)) -> s(max(x,y))
       +(0(),y) -> y
       +(s(x),y) -> s(+(x,y))
       -(x,0()) -> x
       -(s(x),s(y)) -> -(x,y)
       *(x,0()) -> 0()
       *(x,s(y)) -> +(x,*(x,y))
       p(s(x)) -> x
       f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
     Qed
    
    DPs:
     min#(s(x),s(y)) -> min#(x,y)
    TRS:
     min(0(),y) -> 0()
     min(x,0()) -> 0()
     min(s(x),s(y)) -> s(min(x,y))
     max(0(),y) -> y
     max(x,0()) -> x
     max(s(x),s(y)) -> s(max(x,y))
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     *(x,0()) -> 0()
     *(x,s(y)) -> +(x,*(x,y))
     p(s(x)) -> x
     f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(min#) = 1
     problem:
      DPs:
       
      TRS:
       min(0(),y) -> 0()
       min(x,0()) -> 0()
       min(s(x),s(y)) -> s(min(x,y))
       max(0(),y) -> y
       max(x,0()) -> x
       max(s(x),s(y)) -> s(max(x,y))
       +(0(),y) -> y
       +(s(x),y) -> s(+(x,y))
       -(x,0()) -> x
       -(s(x),s(y)) -> -(x,y)
       *(x,0()) -> 0()
       *(x,s(y)) -> +(x,*(x,y))
       p(s(x)) -> x
       f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
     Qed
    
    DPs:
     max#(s(x),s(y)) -> max#(x,y)
    TRS:
     min(0(),y) -> 0()
     min(x,0()) -> 0()
     min(s(x),s(y)) -> s(min(x,y))
     max(0(),y) -> y
     max(x,0()) -> x
     max(s(x),s(y)) -> s(max(x,y))
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     *(x,0()) -> 0()
     *(x,s(y)) -> +(x,*(x,y))
     p(s(x)) -> x
     f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(max#) = 1
     problem:
      DPs:
       
      TRS:
       min(0(),y) -> 0()
       min(x,0()) -> 0()
       min(s(x),s(y)) -> s(min(x,y))
       max(0(),y) -> y
       max(x,0()) -> x
       max(s(x),s(y)) -> s(max(x,y))
       +(0(),y) -> y
       +(s(x),y) -> s(+(x,y))
       -(x,0()) -> x
       -(s(x),s(y)) -> -(x,y)
       *(x,0()) -> 0()
       *(x,s(y)) -> +(x,*(x,y))
       p(s(x)) -> x
       f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
     Qed
    
    DPs:
     *#(x,s(y)) -> *#(x,y)
    TRS:
     min(0(),y) -> 0()
     min(x,0()) -> 0()
     min(s(x),s(y)) -> s(min(x,y))
     max(0(),y) -> y
     max(x,0()) -> x
     max(s(x),s(y)) -> s(max(x,y))
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     *(x,0()) -> 0()
     *(x,s(y)) -> +(x,*(x,y))
     p(s(x)) -> x
     f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(*#) = 1
     problem:
      DPs:
       
      TRS:
       min(0(),y) -> 0()
       min(x,0()) -> 0()
       min(s(x),s(y)) -> s(min(x,y))
       max(0(),y) -> y
       max(x,0()) -> x
       max(s(x),s(y)) -> s(max(x,y))
       +(0(),y) -> y
       +(s(x),y) -> s(+(x,y))
       -(x,0()) -> x
       -(s(x),s(y)) -> -(x,y)
       *(x,0()) -> 0()
       *(x,s(y)) -> +(x,*(x,y))
       p(s(x)) -> x
       f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
     Qed
    
    DPs:
     +#(s(x),y) -> +#(x,y)
    TRS:
     min(0(),y) -> 0()
     min(x,0()) -> 0()
     min(s(x),s(y)) -> s(min(x,y))
     max(0(),y) -> y
     max(x,0()) -> x
     max(s(x),s(y)) -> s(max(x,y))
     +(0(),y) -> y
     +(s(x),y) -> s(+(x,y))
     -(x,0()) -> x
     -(s(x),s(y)) -> -(x,y)
     *(x,0()) -> 0()
     *(x,s(y)) -> +(x,*(x,y))
     p(s(x)) -> x
     f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
    Subterm Criterion Processor:
     simple projection:
      pi(+#) = 0
     problem:
      DPs:
       
      TRS:
       min(0(),y) -> 0()
       min(x,0()) -> 0()
       min(s(x),s(y)) -> s(min(x,y))
       max(0(),y) -> y
       max(x,0()) -> x
       max(s(x),s(y)) -> s(max(x,y))
       +(0(),y) -> y
       +(s(x),y) -> s(+(x,y))
       -(x,0()) -> x
       -(s(x),s(y)) -> -(x,y)
       *(x,0()) -> 0()
       *(x,s(y)) -> +(x,*(x,y))
       p(s(x)) -> x
       f(s(x),s(y)) -> f(-(min(s(x),s(y)),max(s(x),s(y))),*(s(x),s(y)))
     Qed