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:
 RT 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:
   
  Bounds Processor:
   bound: 0
   enrichment: match-rt
   automaton:
    final states: {6,7}
    transitions:
     merge0(6,6) -> 6*
     merge0(7,7) -> 6*
     merge0(6,7) -> 6*
     merge0(7,6) -> 6*
     nil0() -> 7*
     ++0(6,6) -> 6*
     ++0(7,7) -> 6*
     ++0(6,7) -> 6*
     ++0(7,6) -> 6*
     u0() -> 6*
     v0() -> 6*
     7 -> 6*
   problem:
    strict:
     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:
     merge(x,nil()) -> x
   Bounds Processor:
    bound: 0
    enrichment: match-rt
    automaton:
     final states: {6,7}
     transitions:
      merge0(6,6) -> 6*
      merge0(7,7) -> 6*
      merge0(6,7) -> 6*
      merge0(7,6) -> 6*
      nil0() -> 7*
      ++0(6,6) -> 6*
      ++0(7,7) -> 6*
      ++0(6,7) -> 6*
      ++0(7,6) -> 6*
      u0() -> 6*
      v0() -> 6*
      7 -> 6*
    problem:
     strict:
      merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
      merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
     weak:
      merge(nil(),y) -> y
      merge(x,nil()) -> x
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
            [11]
      [v] = [0 ],
      
            [0]
      [u] = [1],
      
                          [1 0]     [0]
      [++](x0, x1) = x0 + [0 0]x1 + [1],
      
                             [1 2]  
      [merge](x0, x1) = x0 + [0 1]x1,
      
              [0]
      [nil] = [0]
     orientation:
                                       [1 0]    [15]        [1 0]    [15]                             
      merge(++(x,y),++(u(),v())) = x + [0 0]y + [3 ] >= x + [0 0]y + [1 ] = ++(x,merge(y,++(u(),v())))
      
                                       [1 0]    [15]    [1 0]    [1 0]    [11]                             
      merge(++(x,y),++(u(),v())) = x + [0 0]y + [3 ] >= [0 0]x + [0 0]y + [2 ] = ++(u(),merge(++(x,y),v()))
      
                       [1 2]          
      merge(nil(),y) = [0 1]y >= y = y
      
                                 
      merge(x,nil()) = x >= x = x
     problem:
      strict:
       merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
      weak:
       merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
       merge(nil(),y) -> y
       merge(x,nil()) -> x
     Matrix Interpretation Processor:
      dimension: 2
      interpretation:
             [0]
       [v] = [8],
       
             [0]
       [u] = [1],
       
                      [1 4]          [5]
       [++](x0, x1) = [0 0]x0 + x1 + [3],
       
                         [1 4]          [5]
       [merge](x0, x1) = [0 1]x0 + x1 + [8],
       
               [0]
       [nil] = [0]
      orientation:
                                    [1 4]    [1 4]    [31]    [1 4]    [1 4]    [19]                             
       merge(++(x,y),++(u(),v())) = [0 0]x + [0 1]y + [22] >= [0 0]x + [0 1]y + [22] = ++(x,merge(y,++(u(),v())))
       
                                    [1 4]    [1 4]    [31]    [1 4]    [1 4]    [31]                             
       merge(++(x,y),++(u(),v())) = [0 0]x + [0 1]y + [22] >= [0 0]x + [0 1]y + [22] = ++(u(),merge(++(x,y),v()))
       
                            [5]         
       merge(nil(),y) = y + [8] >= y = y
       
                        [1 4]    [5]         
       merge(x,nil()) = [0 1]x + [8] >= x = x
      problem:
       strict:
        
       weak:
        merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
        merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
        merge(nil(),y) -> y
        merge(x,nil()) -> x
      Qed