YES
TRS:
 {                             test(x_0, y) -> True(),
                               test(x_0, y) -> False(),
                 match_0(l1_2, l2_1, Nil()) -> l2_1,
            match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                         append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                   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')),
                             part(a_4, l_3) -> match_1(a_4, l_3, l_3),
     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, True()) -> Pair(l1, Cons(x, l2)),
  match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                        match_4(l_5, Nil()) -> Nil(),
                  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_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))}
 DP:
  Strict:
   {       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),
            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')),
                            part#(a_4, l_3) -> match_1#(a_4, l_3, l_3),
    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)),
                 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')),
                                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))),
         match_5#(a, l', l_5, Pair(l1, l2)) -> quick#(l1),
         match_5#(a, l', l_5, Pair(l1, l2)) -> quick#(l2)}
  Weak:
  {                             test(x_0, y) -> True(),
                                test(x_0, y) -> False(),
                  match_0(l1_2, l2_1, Nil()) -> l2_1,
             match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                          append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                    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')),
                              part(a_4, l_3) -> match_1(a_4, l_3, l_3),
      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, True()) -> Pair(l1, Cons(x, l2)),
   match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                         match_4(l_5, Nil()) -> Nil(),
                   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_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))}
  EDG:
   {(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))
    (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)) -> quick#(l2), quick#(l_5) -> match_4#(l_5, l_5))
    (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_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))
    (match_4#(l_5, Cons(a, l')) -> part#(a, l'), part#(a_4, l_3) -> match_1#(a_4, l_3, l_3))
    (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_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')) -> 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)))
    (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))
    (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))
    (quick#(l_5) -> match_4#(l_5, l_5), match_4#(l_5, Cons(a, l')) -> part#(a, l'))
    (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')))}
   SCCS:
    Scc:
     {        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_5#(a, l', l_5, Pair(l1, l2)) -> quick#(l1),
      match_5#(a, l', l_5, Pair(l1, l2)) -> quick#(l2)}
    Scc:
     {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)}
    Scc:
     {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)}
    SCC:
     Strict:
      {        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_5#(a, l', l_5, Pair(l1, l2)) -> quick#(l1),
       match_5#(a, l', l_5, Pair(l1, l2)) -> quick#(l2)}
     Weak:
     {                             test(x_0, y) -> True(),
                                   test(x_0, y) -> False(),
                     match_0(l1_2, l2_1, Nil()) -> l2_1,
                match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                             append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                       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')),
                                 part(a_4, l_3) -> match_1(a_4, l_3, l_3),
         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, True()) -> Pair(l1, Cons(x, l2)),
      match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                            match_4(l_5, Nil()) -> Nil(),
                      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_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))}
     POLY:
      Argument Filtering:
       pi(match_5#) = 3, pi(match_5) = [], pi(quick#) = 0, pi(quick) = [], pi(match_4#) = 1, pi(match_4) = [], pi(match_3) = [0,1,6], pi(match_2) = [4], pi(Pair) = [0,1], pi(part) = [1], pi(match_1) = [2], pi(Cons) = [1], pi(Nil) = [], pi(append) = [], pi(match_0) = [], pi(False) = [], pi(test) = [], pi(True) = []
      Usable Rules:
       {}
      Interpretation:
       [Pair](x0, x1) = x0 + x1 + 1,
       [part](x0) = x0 + 1,
       [Cons](x0) = x0 + 1
      Strict:
       {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)}
      Weak:
       {                             test(x_0, y) -> True(),
                                     test(x_0, y) -> False(),
                       match_0(l1_2, l2_1, Nil()) -> l2_1,
                  match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                               append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                         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')),
                                   part(a_4, l_3) -> match_1(a_4, l_3, l_3),
           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, True()) -> Pair(l1, Cons(x, l2)),
        match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                              match_4(l_5, Nil()) -> Nil(),
                        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_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))}
      EDG:
       {(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')))}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {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)}
     Weak:
     {                             test(x_0, y) -> True(),
                                   test(x_0, y) -> False(),
                     match_0(l1_2, l2_1, Nil()) -> l2_1,
                match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                             append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                       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')),
                                 part(a_4, l_3) -> match_1(a_4, l_3, l_3),
         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, True()) -> Pair(l1, Cons(x, l2)),
      match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                            match_4(l_5, Nil()) -> Nil(),
                      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_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))}
     SPSC:
      Simple Projection:
       pi(part#) = 1, pi(match_1#) = 2
      Strict:
       {part#(a_4, l_3) -> match_1#(a_4, l_3, l_3)}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {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)}
     Weak:
     {                             test(x_0, y) -> True(),
                                   test(x_0, y) -> False(),
                     match_0(l1_2, l2_1, Nil()) -> l2_1,
                match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1)),
                             append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2),
                       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')),
                                 part(a_4, l_3) -> match_1(a_4, l_3, l_3),
         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, True()) -> Pair(l1, Cons(x, l2)),
      match_3(l1, l2, x, l', a_4, l_3, False()) -> Pair(Cons(x, l1), l2),
                            match_4(l_5, Nil()) -> Nil(),
                      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_5(a, l', l_5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))}
     SPSC:
      Simple Projection:
       pi(append#) = 0, pi(match_0#) = 2
      Strict:
       {append#(l1_2, l2_1) -> match_0#(l1_2, l2_1, l1_2)}
      EDG:
       {}
       SCCS:
        
        Qed