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)))
    Usable Rule Processor:
     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:
      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))
      test(x_0,y) -> True()
      test(x_0,y) -> False()
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       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))
       test(x_0,y) -> True()
       test(x_0,y) -> False()
      interpretation:
       [match_5#](x0, x1, x2, x3) = x0 + x1 + x3 + 0,
       
       [match_4#](x0, x1) = x0 + x1 + 4,
       
       [quick#](x0) = x0 + 4,
       
       [match_3](x0, x1, x2, x3, x4, x5, x6) = 1x0 + 1x1 + 4x2 + 4x6 + 0,
       
       [match_2](x0, x1, x2, x3, x4) = 4x0 + x1 + 1x4 + 0,
       
       [Pair](x0, x1) = x0 + x1 + 4,
       
       [match_1](x0, x1, x2) = x1 + x2,
       
       [part](x0, x1) = x1 + 2,
       
       [Cons](x0, x1) = 4x0 + 1x1 + 3,
       
       [Nil] = 4,
       
       [False] = 0,
       
       [True] = 0,
       
       [test](x0, x1) = x1 + 1
      orientation:
       match_5#(a,l',l_5,Pair(l1,l2)) = a + l' + l1 + l2 + 4 >= l2 + 4 = quick#(l2)
       
       quick#(l_5) = l_5 + 4 >= l_5 + 4 = match_4#(l_5,l_5)
       
       match_4#(l_5,Cons(a,l')) = 4a + 1l' + l_5 + 4 >= a + l' + 2 = match_5#(a,l',l_5,part(a,l'))
       
       match_5#(a,l',l_5,Pair(l1,l2)) = a + l' + l1 + l2 + 4 >= l1 + 4 = quick#(l1)
       
       part(a_4,l_3) = l_3 + 2 >= l_3 = match_1(a_4,l_3,l_3)
       
       match_1(a_4,l_3,Nil()) = l_3 + 4 >= 4 = Pair(Nil(),Nil())
       
       match_1(a_4,l_3,Cons(x,l')) = 1l' + l_3 + 4x + 3 >= 1l' + 4x + 3 = match_2(x,l',a_4,l_3,part(a_4,l'))
       
       match_2(x,l',a_4,l_3,Pair(l1,l2)) = l' + 1l1 + 1l2 + 4x + 5 >= 1l1 + 1l2 + 4x + 5 = 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()) = 1l1 + 1l2 + 4x + 4 >= 1l1 + l2 + 4x + 4 = Pair(Cons(x,l1),l2)
       
       match_3(l1,l2,x,l',a_4,l_3,True()) = 1l1 + 1l2 + 4x + 4 >= l1 + 1l2 + 4x + 4 = Pair(l1,Cons(x,l2))
       
       test(x_0,y) = y + 1 >= 0 = True()
       
       test(x_0,y) = y + 1 >= 0 = False()
      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:
        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))
        test(x_0,y) -> True()
        test(x_0,y) -> False()
      Restore Modifier:
       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