YES(?,O(n^2))

Problem:
 +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
 *(*(x,y),z) -> *(x,*(y,z))

Proof:
 Complexity Transformation Processor:
  strict:
   +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
   *(*(x,y),z) -> *(x,*(y,z))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [+](x0, x1) = x0 + x1,
     
     [a] = 0,
     
     [*](x0, x1) = x0 + x1 + 1
    orientation:
     +(*(x,y),*(a(),y)) = x + 2y + 2 >= x + y + 1 = *(+(x,a()),y)
     
     *(*(x,y),z) = x + y + z + 2 >= x + y + z + 2 = *(x,*(y,z))
    problem:
     strict:
      *(*(x,y),z) -> *(x,*(y,z))
     weak:
      +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
    Matrix Interpretation Processor:
     dimension: 2
     max_matrix:
      [1 1]
      [0 1]
      interpretation:
                     [1 1]          [0]
       [+](x0, x1) = [0 0]x0 + x1 + [1],
       
             [1]
       [a] = [1],
       
                     [1 1]          [0]
       [*](x0, x1) = [0 1]x0 + x1 + [1]
      orientation:
                     [1 2]    [1 1]        [1]    [1 1]    [1 1]        [0]              
       *(*(x,y),z) = [0 1]x + [0 1]y + z + [2] >= [0 1]x + [0 1]y + z + [2] = *(x,*(y,z))
       
                            [1 2]    [2 1]    [3]    [1 1]        [3]                
       +(*(x,y),*(a(),y)) = [0 0]x + [0 1]y + [3] >= [0 0]x + y + [3] = *(+(x,a()),y)
      problem:
       strict:
        
       weak:
        *(*(x,y),z) -> *(x,*(y,z))
        +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
      Qed