YES
Time: 0.842

Problem:
 Equations:
  minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5))
  minAC(x3,x4) -> minAC(x4,x3)
  maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5))
  maxAC(x3,x4) -> maxAC(x4,x3)
  minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5)
  minAC(x4,x3) -> minAC(x3,x4)
  maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5)
  maxAC(x4,x3) -> maxAC(x3,x4)
 TRS:
  plus(x,0()) -> x
  plus(x,s(y)) -> s(plus(x,y))
  minAC(0(),y) -> 0()
  minAC(s(x),s(y)) -> s(minAC(x,y))
  maxAC(0(),y) -> y
  maxAC(s(x),s(y)) -> s(maxAC(x,y))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [1 0]     [3]
   [s](x0) = [2 0]x0 + [1],
   
                    [1 4]     [5  0 ]     [0]
   [plus](x0, x1) = [9 8]x0 + [2  12]x1 + [8],
   
         [5]
   [0] = [1],
   
                               [3]
   [maxAC](x0, x1) = x0 + x1 + [8],
   
                               [6 ]
   [minAC](x0, x1) = x0 + x1 + [13]
  orientation:
                 [1 4]    [25]         
   plus(x,0()) = [9 8]x + [30] >= x = x
   
                  [1 4]    [5  0 ]    [15]    [1 4]    [5  0 ]    [3]               
   plus(x,s(y)) = [9 8]x + [26 0 ]y + [26] >= [2 8]x + [10 0 ]y + [1] = s(plus(x,y))
   
                      [11]    [5]      
   minAC(0(),y) = y + [14] >= [1] = 0()
   
                      [1 0]    [1 0]    [12]    [1 0]    [1 0]    [9 ]                
   minAC(s(x),s(y)) = [2 0]x + [2 0]y + [15] >= [2 0]x + [2 0]y + [13] = s(minAC(x,y))
   
                      [8]         
   maxAC(0(),y) = y + [9] >= y = y
   
                      [1 0]    [1 0]    [9 ]    [1 0]    [1 0]    [6]                
   maxAC(s(x),s(y)) = [2 0]x + [2 0]y + [10] >= [2 0]x + [2 0]y + [7] = s(maxAC(x,y))
  problem:
   Equations:
    minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5))
    minAC(x3,x4) -> minAC(x4,x3)
    maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5))
    maxAC(x3,x4) -> maxAC(x4,x3)
    minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5)
    minAC(x4,x3) -> minAC(x3,x4)
    maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5)
    maxAC(x4,x3) -> maxAC(x3,x4)
   TRS:
    
  Qed