YES(?,O(n^2))

Problem:
 merge(x,nil()) -> x
 merge(nil(),y) -> y
 merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
 merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))

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