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)))
  TDG 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)))
   graph:
    match_5#(a,l',l_5,Pair(l1,l2)) -> quick#(l2) ->
    quick#(l_5) -> match_4#(l_5,l_5)
    match_5#(a,l',l_5,Pair(l1,l2)) -> quick#(l1) ->
    quick#(l_5) -> match_4#(l_5,l_5)
    match_5#(a,l',l_5,Pair(l1,l2)) -> append#(quick(l1),Cons(a,quick(l2))) ->
    append#(l1_2,l2_1) -> match_0#(l1_2,l2_1,l1_2)
    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)))
    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#(l1)
    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_4#(l_5,Cons(a,l')) -> part#(a,l') ->
    part#(a_4,l_3) -> match_1#(a_4,l_3,l_3)
    quick#(l_5) -> match_4#(l_5,l_5) ->
    match_4#(l_5,Cons(a,l')) -> match_5#(a,l',l_5,part(a,l'))
    quick#(l_5) -> match_4#(l_5,l_5) ->
    match_4#(l_5,Cons(a,l')) -> part#(a,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)) -> match_3#(l1,l2,x,l',a_4,l_3,test(a_4,x))
    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_1#(a_4,l_3,Cons(x,l')) -> part#(a_4,l') ->
    part#(a_4,l_3) -> match_1#(a_4,l_3,l_3)
    part#(a_4,l_3) -> match_1#(a_4,l_3,l_3) ->
    match_1#(a_4,l_3,Cons(x,l')) -> match_2#(x,l',a_4,l_3,part(a_4,l'))
    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_0#(l1_2,l2_1,Cons(x,l)) -> append#(l,l2_1) ->
    append#(l1_2,l2_1) -> match_0#(l1_2,l2_1,l1_2)
    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)
   SCC Processor:
    #sccs: 3
    #rules: 8
    #arcs: 16/169
    DPs:
     match_5#(a,l',l_5,Pair(l1,l2)) -> quick#(l2)
     quick#(l_5) -> match_4#(l_5,l_5)
     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#(l1)
    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
     
     interpretation:
      [match_5#](x0, x1, x2, x3) = x3,
      
      [match_4#](x0, x1) = 7/2x1,
      
      [quick#](x0) = 7/2x0,
      
      [match_5](x0, x1, x2, x3) = x3 + 3,
      
      [match_4](x0, x1) = 7/2x1,
      
      [quick](x0) = 7/2x0,
      
      [match_3](x0, x1, x2, x3, x4, x5, x6) = 7/2x0 + 7/2x1 + 1/2x6 + 3,
      
      [match_2](x0, x1, x2, x3, x4) = x4 + 7/2,
      
      [Pair](x0, x1) = 7/2x0 + 7/2x1,
      
      [match_1](x0, x1, x2) = 7/2x2,
      
      [part](x0, x1) = 7/2x1,
      
      [Cons](x0, x1) = x1 + 1,
      
      [Nil] = 0,
      
      [match_0](x0, x1, x2) = x1 + x2 + 2,
      
      [append](x0, x1) = x0 + x1 + 2,
      
      [False] = 1,
      
      [True] = 1,
      
      [test](x0, x1) = 1
     orientation:
      match_5#(a,l',l_5,Pair(l1,l2)) = 7/2l1 + 7/2l2 >= 7/2l2 = quick#(l2)
      
      quick#(l_5) = 7/2l_5 >= 7/2l_5 = match_4#(l_5,l_5)
      
      match_4#(l_5,Cons(a,l')) = 7/2l' + 7/2 >= 7/2l' = match_5#(a,l',l_5,part(a,l'))
      
      match_5#(a,l',l_5,Pair(l1,l2)) = 7/2l1 + 7/2l2 >= 7/2l1 = quick#(l1)
      
      test(x_0,y) = 1 >= 1 = True()
      
      test(x_0,y) = 1 >= 1 = False()
      
      append(l1_2,l2_1) = l1_2 + l2_1 + 2 >= l1_2 + l2_1 + 2 = match_0(l1_2,l2_1,l1_2)
      
      match_0(l1_2,l2_1,Nil()) = l2_1 + 2 >= l2_1 = l2_1
      
      match_0(l1_2,l2_1,Cons(x,l)) = l + l2_1 + 3 >= l + l2_1 + 3 = Cons(x,append(l,l2_1))
      
      part(a_4,l_3) = 7/2l_3 >= 7/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')) = 7/2l' + 7/2 >= 7/2l' + 7/2 = match_2(x,l',a_4,l_3,part(a_4,l'))
      
      match_2(x,l',a_4,l_3,Pair(l1,l2)) = 7/2l1 + 7/2l2 + 7/2 >= 7/2l1 + 7/2l2 + 7/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()) = 7/2l1 + 7/2l2 + 7/2 >= 7/2l1 + 7/2l2 + 7/2 = Pair(Cons(x,l1),l2)
      
      match_3(l1,l2,x,l',a_4,l_3,True()) = 7/2l1 + 7/2l2 + 7/2 >= 7/2l1 + 7/2l2 + 7/2 = Pair(l1,Cons(x,l2))
      
      quick(l_5) = 7/2l_5 >= 7/2l_5 = match_4(l_5,l_5)
      
      match_4(l_5,Nil()) = 0 >= 0 = Nil()
      
      match_4(l_5,Cons(a,l')) = 7/2l' + 7/2 >= 7/2l' + 3 = match_5(a,l',l_5,part(a,l'))
      
      match_5(a,l',l_5,Pair(l1,l2)) = 7/2l1 + 7/2l2 + 3 >= 7/2l1 + 7/2l2 + 3 = append(quick(l1),Cons(a,quick(l2)))
     problem:
      DPs:
       match_5#(a,l',l_5,Pair(l1,l2)) -> quick#(l2)
       quick#(l_5) -> match_4#(l_5,l_5)
       match_5#(a,l',l_5,Pair(l1,l2)) -> quick#(l1)
      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)))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 5/9
      
    
    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)
    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)))
    Subterm Criterion Processor:
     simple projection:
      pi(append#) = 0
      pi(match_0#) = 2
     problem:
      DPs:
       append#(l1_2,l2_1) -> match_0#(l1_2,l2_1,l1_2)
      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)))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 2/1
      
    
    DPs:
     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')
    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)))
    Subterm Criterion Processor:
     simple projection:
      pi(part#) = 1
      pi(match_1#) = 2
     problem:
      DPs:
       part#(a_4,l_3) -> match_1#(a_4,l_3,l_3)
      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)))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 2/1