YES

Problem:
 test(x_0,y) -> True()
 test(x_0,y) -> False()
 append(l1_2,l2_1) -> match_0(l1_2,l2_1,l1_2)
 match_0(l1_2,l2_1,Nil()) -> l2_1
 match_0(l1_2,l2_1,Cons(x,l)) -> Cons(x,append(l,l2_1))
 part(a_4,l_3) -> match_1(a_4,l_3,l_3)
 match_1(a_4,l_3,Nil()) -> Pair(Nil(),Nil())
 match_1(a_4,l_3,Cons(x,l')) -> match_2(x,l',a_4,l_3,part(a_4,l'))
 match_2(x,l',a_4,l_3,Pair(l1,l2)) -> match_3(l1,l2,x,l',a_4,l_3,test(a_4,x))
 match_3(l1,l2,x,l',a_4,l_3,False()) -> Pair(Cons(x,l1),l2)
 match_3(l1,l2,x,l',a_4,l_3,True()) -> Pair(l1,Cons(x,l2))
 quick(l_5) -> match_4(l_5,l_5)
 match_4(l_5,Nil()) -> Nil()
 match_4(l_5,Cons(a,l')) -> match_5(a,l',l_5,part(a,l'))
 match_5(a,l',l_5,Pair(l1,l2)) -> append(quick(l1),Cons(a,quick(l2)))

Proof:
 DP Processor:
  DPs:
   append#(l1_2,l2_1) -> match_0#(l1_2,l2_1,l1_2)
   match_0#(l1_2,l2_1,Cons(x,l)) -> append#(l,l2_1)
   part#(a_4,l_3) -> match_1#(a_4,l_3,l_3)
   match_1#(a_4,l_3,Cons(x,l')) -> part#(a_4,l')
   match_1#(a_4,l_3,Cons(x,l')) -> match_2#(x,l',a_4,l_3,part(a_4,l'))
   match_2#(x,l',a_4,l_3,Pair(l1,l2)) -> test#(a_4,x)
   match_2#(x,l',a_4,l_3,Pair(l1,l2)) -> match_3#(l1,l2,x,l',a_4,l_3,test(a_4,x))
   quick#(l_5) -> match_4#(l_5,l_5)
   match_4#(l_5,Cons(a,l')) -> part#(a,l')
   match_4#(l_5,Cons(a,l')) -> match_5#(a,l',l_5,part(a,l'))
   match_5#(a,l',l_5,Pair(l1,l2)) -> quick#(l2)
   match_5#(a,l',l_5,Pair(l1,l2)) -> quick#(l1)
   match_5#(a,l',l_5,Pair(l1,l2)) -> append#(quick(l1),Cons(a,quick(l2)))
  TRS:
   test(x_0,y) -> True()
   test(x_0,y) -> False()
   append(l1_2,l2_1) -> match_0(l1_2,l2_1,l1_2)
   match_0(l1_2,l2_1,Nil()) -> l2_1
   match_0(l1_2,l2_1,Cons(x,l)) -> Cons(x,append(l,l2_1))
   part(a_4,l_3) -> match_1(a_4,l_3,l_3)
   match_1(a_4,l_3,Nil()) -> Pair(Nil(),Nil())
   match_1(a_4,l_3,Cons(x,l')) -> match_2(x,l',a_4,l_3,part(a_4,l'))
   match_2(x,l',a_4,l_3,Pair(l1,l2)) -> match_3(l1,l2,x,l',a_4,l_3,test(a_4,x))
   match_3(l1,l2,x,l',a_4,l_3,False()) -> Pair(Cons(x,l1),l2)
   match_3(l1,l2,x,l',a_4,l_3,True()) -> Pair(l1,Cons(x,l2))
   quick(l_5) -> match_4(l_5,l_5)
   match_4(l_5,Nil()) -> Nil()
   match_4(l_5,Cons(a,l')) -> match_5(a,l',l_5,part(a,l'))
   match_5(a,l',l_5,Pair(l1,l2)) -> append(quick(l1),Cons(a,quick(l2)))
  Matrix Interpretation Processor: dim=1
   
   usable rules:
    append(l1_2,l2_1) -> match_0(l1_2,l2_1,l1_2)
    match_0(l1_2,l2_1,Nil()) -> l2_1
    match_0(l1_2,l2_1,Cons(x,l)) -> Cons(x,append(l,l2_1))
    part(a_4,l_3) -> match_1(a_4,l_3,l_3)
    match_1(a_4,l_3,Nil()) -> Pair(Nil(),Nil())
    match_1(a_4,l_3,Cons(x,l')) -> match_2(x,l',a_4,l_3,part(a_4,l'))
    match_2(x,l',a_4,l_3,Pair(l1,l2)) -> match_3(l1,l2,x,l',a_4,l_3,test(a_4,x))
    match_3(l1,l2,x,l',a_4,l_3,False()) -> Pair(Cons(x,l1),l2)
    match_3(l1,l2,x,l',a_4,l_3,True()) -> Pair(l1,Cons(x,l2))
    quick(l_5) -> match_4(l_5,l_5)
    match_4(l_5,Nil()) -> Nil()
    match_4(l_5,Cons(a,l')) -> match_5(a,l',l_5,part(a,l'))
    match_5(a,l',l_5,Pair(l1,l2)) -> append(quick(l1),Cons(a,quick(l2)))
   interpretation:
    [match_5#](x0, x1, x2, x3) = 3x3 + 2,
    
    [match_4#](x0, x1) = 3/2x1 + 1,
    
    [quick#](x0) = 3/2x0 + 3/2,
    
    [match_3#](x0, x1, x2, x3, x4, x5, x6) = 0,
    
    [match_2#](x0, x1, x2, x3, x4) = 1/2,
    
    [match_1#](x0, x1, x2) = x2,
    
    [part#](x0, x1) = x1 + 1/2,
    
    [match_0#](x0, x1, x2) = x2 + 1/2,
    
    [append#](x0, x1) = x0 + 1,
    
    [test#](x0, x1) = 0,
    
    [match_5](x0, x1, x2, x3) = 3x3 + 3/2,
    
    [match_4](x0, x1) = 3/2x1,
    
    [quick](x0) = 3/2x0,
    
    [match_3](x0, x1, x2, x3, x4, x5, x6) = 1/2x0 + 1/2x1 + 1/2,
    
    [match_2](x0, x1, x2, x3, x4) = x4 + 1/2,
    
    [Pair](x0, x1) = 1/2x0 + 1/2x1,
    
    [match_1](x0, x1, x2) = 1/2x2,
    
    [part](x0, x1) = 1/2x1,
    
    [Cons](x0, x1) = x1 + 1,
    
    [Nil] = 0,
    
    [match_0](x0, x1, x2) = x1 + x2,
    
    [append](x0, x1) = x0 + x1,
    
    [False] = 0,
    
    [True] = 0,
    
    [test](x0, x1) = 0
   orientation:
    append#(l1_2,l2_1) = l1_2 + 1 >= l1_2 + 1/2 = match_0#(l1_2,l2_1,l1_2)
    
    match_0#(l1_2,l2_1,Cons(x,l)) = l + 3/2 >= l + 1 = append#(l,l2_1)
    
    part#(a_4,l_3) = l_3 + 1/2 >= l_3 = match_1#(a_4,l_3,l_3)
    
    match_1#(a_4,l_3,Cons(x,l')) = l' + 1 >= l' + 1/2 = part#(a_4,l')
    
    match_1#(a_4,l_3,Cons(x,l')) = l' + 1 >= 1/2 = match_2#(x,l',a_4,l_3,part(a_4,l'))
    
    match_2#(x,l',a_4,l_3,Pair(l1,l2)) = 1/2 >= 0 = test#(a_4,x)
    
    match_2#(x,l',a_4,l_3,Pair(l1,l2)) = 1/2 >= 0 = match_3#(l1,l2,x,l',a_4,l_3,test(a_4,x))
    
    quick#(l_5) = 3/2l_5 + 3/2 >= 3/2l_5 + 1 = match_4#(l_5,l_5)
    
    match_4#(l_5,Cons(a,l')) = 3/2l' + 5/2 >= l' + 1/2 = part#(a,l')
    
    match_4#(l_5,Cons(a,l')) = 3/2l' + 5/2 >= 3/2l' + 2 = match_5#(a,l',l_5,part(a,l'))
    
    match_5#(a,l',l_5,Pair(l1,l2)) = 3/2l1 + 3/2l2 + 2 >= 3/2l2 + 3/2 = quick#(l2)
    
    match_5#(a,l',l_5,Pair(l1,l2)) = 3/2l1 + 3/2l2 + 2 >= 3/2l1 + 3/2 = quick#(l1)
    
    match_5#(a,l',l_5,Pair(l1,l2)) = 3/2l1 + 3/2l2 + 2 >= 3/2l1 + 1 = append#(quick(l1),Cons(a,quick(l2)))
    
    test(x_0,y) = 0 >= 0 = True()
    
    test(x_0,y) = 0 >= 0 = False()
    
    append(l1_2,l2_1) = l1_2 + l2_1 >= l1_2 + l2_1 = match_0(l1_2,l2_1,l1_2)
    
    match_0(l1_2,l2_1,Nil()) = l2_1 >= l2_1 = l2_1
    
    match_0(l1_2,l2_1,Cons(x,l)) = l + l2_1 + 1 >= l + l2_1 + 1 = Cons(x,append(l,l2_1))
    
    part(a_4,l_3) = 1/2l_3 >= 1/2l_3 = match_1(a_4,l_3,l_3)
    
    match_1(a_4,l_3,Nil()) = 0 >= 0 = Pair(Nil(),Nil())
    
    match_1(a_4,l_3,Cons(x,l')) = 1/2l' + 1/2 >= 1/2l' + 1/2 = match_2(x,l',a_4,l_3,part(a_4,l'))
    
    match_2(x,l',a_4,l_3,Pair(l1,l2)) = 1/2l1 + 1/2l2 + 1/2 >= 1/2l1 + 1/2l2 + 1/2 = match_3(l1,l2,x,l',a_4,l_3,test(a_4,x))
    
    match_3(l1,l2,x,l',a_4,l_3,False()) = 1/2l1 + 1/2l2 + 1/2 >= 1/2l1 + 1/2l2 + 1/2 = Pair(Cons(x,l1),l2)
    
    match_3(l1,l2,x,l',a_4,l_3,True()) = 1/2l1 + 1/2l2 + 1/2 >= 1/2l1 + 1/2l2 + 1/2 = Pair(l1,Cons(x,l2))
    
    quick(l_5) = 3/2l_5 >= 3/2l_5 = match_4(l_5,l_5)
    
    match_4(l_5,Nil()) = 0 >= 0 = Nil()
    
    match_4(l_5,Cons(a,l')) = 3/2l' + 3/2 >= 3/2l' + 3/2 = match_5(a,l',l_5,part(a,l'))
    
    match_5(a,l',l_5,Pair(l1,l2)) = 3/2l1 + 3/2l2 + 3/2 >= 3/2l1 + 3/2l2 + 1 = append(quick(l1),Cons(a,quick(l2)))
   problem:
    DPs:
     
    TRS:
     test(x_0,y) -> True()
     test(x_0,y) -> False()
     append(l1_2,l2_1) -> match_0(l1_2,l2_1,l1_2)
     match_0(l1_2,l2_1,Nil()) -> l2_1
     match_0(l1_2,l2_1,Cons(x,l)) -> Cons(x,append(l,l2_1))
     part(a_4,l_3) -> match_1(a_4,l_3,l_3)
     match_1(a_4,l_3,Nil()) -> Pair(Nil(),Nil())
     match_1(a_4,l_3,Cons(x,l')) -> match_2(x,l',a_4,l_3,part(a_4,l'))
     match_2(x,l',a_4,l_3,Pair(l1,l2)) -> match_3(l1,l2,x,l',a_4,l_3,test(a_4,x))
     match_3(l1,l2,x,l',a_4,l_3,False()) -> Pair(Cons(x,l1),l2)
     match_3(l1,l2,x,l',a_4,l_3,True()) -> Pair(l1,Cons(x,l2))
     quick(l_5) -> match_4(l_5,l_5)
     match_4(l_5,Nil()) -> Nil()
     match_4(l_5,Cons(a,l')) -> match_5(a,l',l_5,part(a,l'))
     match_5(a,l',l_5,Pair(l1,l2)) -> append(quick(l1),Cons(a,quick(l2)))
   Qed