MAYBE

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)))
  EDG 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)) -> 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)) -> append#(quick(l1),Cons(a,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')) -> 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'))
    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))
    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')) -> 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')) -> match_2#(x,l',a_4,l_3,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)))
    Open
    
    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)))
    Open
    
    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)))
    Open