- : unit = ()
h : heuristic = <heuristic>
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)

TRS termination of:
[1] test(x_0,y) -> True
[2] test(x_0,y) -> False
[3] append(l1_2,l2_1) -> match_0(l1_2,l2_1,l1_2)
[4] match_0(l1_2,l2_1,Nil) -> l2_1
[5] match_0(l1_2,l2_1,Cons(x,l)) -> Cons(x,append(l,l2_1))
[6] part(a_4,l_3) -> match_1(a_4,l_3,l_3)
[7] match_1(a_4,l_3,Nil) -> Pair(Nil,Nil)
[8] match_1(a_4,l_3,Cons(x,l')) -> match_2(x,l',a_4,l_3,part(a_4,l'))
[9] 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))
[10] match_3(l1,l2,x,l',a_4,l_3,False) -> Pair(Cons(x,l1),l2)
[11] match_3(l1,l2,x,l',a_4,l_3,True) -> Pair(l1,Cons(x,l2))
[12] quick(l_5) -> match_4(l_5,l_5)
[13] match_4(l_5,Nil) -> Nil
[14] match_4(l_5,Cons(a,l')) -> match_5(a,l',l_5,part(a,l'))
[15] match_5(a,l',l_5,Pair(l1,l2)) -> append(quick(l1),Cons(a,quick(l2)))


Sub problem: 
guided: 

DP termination of:
<Marked_append(l1_2,l2_1) , Marked_match_0(l1_2,l2_1,l1_2)>
<Marked_match_0(l1_2,l2_1,Cons(x,l)) , Marked_append(l,l2_1)>
<Marked_part(a_4,l_3) , Marked_match_1(a_4,l_3,l_3)>
<Marked_match_1(a_4,l_3,Cons(x,l')) , Marked_match_2(x,l',a_4,l_3,part(a_4,l'))>
<Marked_match_1(a_4,l_3,Cons(x,l')) , Marked_part(a_4,l')>
<Marked_match_2(x,l',a_4,l_3,Pair(l1,l2)) , Marked_match_3(l1,l2,x,l',
                                             a_4,l_3,test(a_4,x))>
<Marked_match_2(x,l',a_4,l_3,Pair(l1,l2)) , Marked_test(a_4,x)>
<Marked_quick(l_5) , Marked_match_4(l_5,l_5)>
<Marked_match_4(l_5,Cons(a,l')) , Marked_match_5(a,l',l_5,part(a,l'))>
<Marked_match_4(l_5,Cons(a,l')) , Marked_part(a,l')>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_append(quick(l1),
                                         Cons(a,quick(l2)))>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l1)>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l2)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 3 components:

{  <Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l2)> 
      --> <Marked_quick(l_5) , Marked_match_4(l_5,l_5)>
  <Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l1)> 
     --> <Marked_quick(l_5) , Marked_match_4(l_5,l_5)>
  <Marked_match_4(l_5,Cons(a,l')) , Marked_match_5(a,l',l_5,part(a,l'))> 
     --> <Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l2)>
  <Marked_match_4(l_5,Cons(a,l')) , Marked_match_5(a,l',l_5,part(a,l'))> 
     --> <Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l1)>
  <Marked_quick(l_5) , Marked_match_4(l_5,l_5)> 
     --> <Marked_match_4(l_5,Cons(a,l')) , Marked_match_5(a,l',l_5,part(a,l'))>
}

{  <Marked_match_0(l1_2,l2_1,Cons(x,l)) , Marked_append(l,l2_1)> 
      --> <Marked_append(l1_2,l2_1) , Marked_match_0(l1_2,l2_1,l1_2)>
  <Marked_append(l1_2,l2_1) , Marked_match_0(l1_2,l2_1,l1_2)> 
     --> <Marked_match_0(l1_2,l2_1,Cons(x,l)) , Marked_append(l,l2_1)>
}

{  <Marked_match_1(a_4,l_3,Cons(x,l')) , Marked_part(a_4,l')> 
      --> <Marked_part(a_4,l_3) , Marked_match_1(a_4,l_3,l_3)>
  <Marked_part(a_4,l_3) , Marked_match_1(a_4,l_3,l_3)> 
     --> <Marked_match_1(a_4,l_3,Cons(x,l')) , Marked_part(a_4,l')>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  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))) ;
  Marked_match_5(a,l',l_5,Pair(l1,l2)) >= Marked_quick(l2) ;
  Marked_match_5(a,l',l_5,Pair(l1,l2)) >= Marked_quick(l1) ;
  Marked_quick(l_5) >= Marked_match_4(l_5,l_5) ;
  Marked_match_4(l_5,Cons(a,l')) >= Marked_match_5(a,l',l_5,part(a,l')) ;
 }
 + Disjunctions:{ 
{
  Marked_match_5(a,l',l_5,Pair(l1,l2)) > Marked_quick(l2) ;
 }
{
  Marked_match_5(a,l',l_5,Pair(l1,l2)) > Marked_quick(l1) ;
 }
{
  Marked_quick(l_5) > Marked_match_4(l_5,l_5) ;
 }
{
  Marked_match_4(l_5,Cons(a,l')) > Marked_match_5(a,l',l_5,part(a,l')) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: test(x_0,y) >= True
constraint: test(x_0,y) >= False
constraint: match_0(l1_2,l2_1,Nil) >= l2_1
constraint: match_0(l1_2,l2_1,Cons(x,l)) >= Cons(x,append(l,l2_1))
constraint: append(l1_2,l2_1) >= match_0(l1_2,l2_1,l1_2)
constraint: match_1(a_4,l_3,Nil) >= Pair(Nil,Nil)
constraint: match_1(a_4,l_3,Cons(x,l')) >= match_2(x,l',a_4,l_3,part(a_4,l'))
constraint: part(a_4,l_3) >= match_1(a_4,l_3,l_3)
constraint: 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))
constraint: match_3(l1,l2,x,l',a_4,l_3,True) >= Pair(l1,Cons(x,l2))
constraint: match_3(l1,l2,x,l',a_4,l_3,False) >= Pair(Cons(x,l1),l2)
constraint: match_4(l_5,Nil) >= Nil
constraint: match_4(l_5,Cons(a,l')) >= match_5(a,l',l_5,part(a,l'))
constraint: quick(l_5) >= match_4(l_5,l_5)
constraint: match_5(a,l',l_5,Pair(l1,l2)) >= append(quick(l1),
                                              Cons(a,quick(l2)))
constraint: Marked_match_5(a,l',l_5,Pair(l1,l2)) >= Marked_quick(l2)
constraint: Marked_match_5(a,l',l_5,Pair(l1,l2)) >= Marked_quick(l1)
constraint: Marked_quick(l_5) >= Marked_match_4(l_5,l_5)
constraint: Marked_match_4(l_5,Cons(a,l')) >= Marked_match_5(a,l',l_5,
                                               part(a,l'))
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  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))) ;
  Marked_append(l1_2,l2_1) >= Marked_match_0(l1_2,l2_1,l1_2) ;
  Marked_match_0(l1_2,l2_1,Cons(x,l)) >= Marked_append(l,l2_1) ;
 }
 + Disjunctions:{ 
{
  Marked_append(l1_2,l2_1) > Marked_match_0(l1_2,l2_1,l1_2) ;
 }
{
  Marked_match_0(l1_2,l2_1,Cons(x,l)) > Marked_append(l,l2_1) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: test(x_0,y) >= True
constraint: test(x_0,y) >= False
constraint: match_0(l1_2,l2_1,Nil) >= l2_1
constraint: match_0(l1_2,l2_1,Cons(x,l)) >= Cons(x,append(l,l2_1))
constraint: append(l1_2,l2_1) >= match_0(l1_2,l2_1,l1_2)
constraint: match_1(a_4,l_3,Nil) >= Pair(Nil,Nil)
constraint: match_1(a_4,l_3,Cons(x,l')) >= match_2(x,l',a_4,l_3,part(a_4,l'))
constraint: part(a_4,l_3) >= match_1(a_4,l_3,l_3)
constraint: 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))
constraint: match_3(l1,l2,x,l',a_4,l_3,True) >= Pair(l1,Cons(x,l2))
constraint: match_3(l1,l2,x,l',a_4,l_3,False) >= Pair(Cons(x,l1),l2)
constraint: match_4(l_5,Nil) >= Nil
constraint: match_4(l_5,Cons(a,l')) >= match_5(a,l',l_5,part(a,l'))
constraint: quick(l_5) >= match_4(l_5,l_5)
constraint: match_5(a,l',l_5,Pair(l1,l2)) >= append(quick(l1),
                                              Cons(a,quick(l2)))
constraint: Marked_append(l1_2,l2_1) >= Marked_match_0(l1_2,l2_1,l1_2)
constraint: Marked_match_0(l1_2,l2_1,Cons(x,l)) >= Marked_append(l,l2_1)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  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))) ;
  Marked_part(a_4,l_3) >= Marked_match_1(a_4,l_3,l_3) ;
  Marked_match_1(a_4,l_3,Cons(x,l')) >= Marked_part(a_4,l') ;
 }
 + Disjunctions:{ 
{
  Marked_part(a_4,l_3) > Marked_match_1(a_4,l_3,l_3) ;
 }
{
  Marked_match_1(a_4,l_3,Cons(x,l')) > Marked_part(a_4,l') ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: test(x_0,y) >= True
constraint: test(x_0,y) >= False
constraint: match_0(l1_2,l2_1,Nil) >= l2_1
constraint: match_0(l1_2,l2_1,Cons(x,l)) >= Cons(x,append(l,l2_1))
constraint: append(l1_2,l2_1) >= match_0(l1_2,l2_1,l1_2)
constraint: match_1(a_4,l_3,Nil) >= Pair(Nil,Nil)
constraint: match_1(a_4,l_3,Cons(x,l')) >= match_2(x,l',a_4,l_3,part(a_4,l'))
constraint: part(a_4,l_3) >= match_1(a_4,l_3,l_3)
constraint: 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))
constraint: match_3(l1,l2,x,l',a_4,l_3,True) >= Pair(l1,Cons(x,l2))
constraint: match_3(l1,l2,x,l',a_4,l_3,False) >= Pair(Cons(x,l1),l2)
constraint: match_4(l_5,Nil) >= Nil
constraint: match_4(l_5,Cons(a,l')) >= match_5(a,l',l_5,part(a,l'))
constraint: quick(l_5) >= match_4(l_5,l_5)
constraint: match_5(a,l',l_5,Pair(l1,l2)) >= append(quick(l1),
                                              Cons(a,quick(l2)))
constraint: Marked_part(a_4,l_3) >= Marked_match_1(a_4,l_3,l_3)
constraint: Marked_match_1(a_4,l_3,Cons(x,l')) >= Marked_part(a_4,l')
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
TRS termination of:
[1] test(x_0,y) -> True
[2] test(x_0,y) -> False
[3] append(l1_2,l2_1) -> match_0(l1_2,l2_1,l1_2)
[4] match_0(l1_2,l2_1,Nil) -> l2_1
[5] match_0(l1_2,l2_1,Cons(x,l)) -> Cons(x,append(l,l2_1))
[6] part(a_4,l_3) -> match_1(a_4,l_3,l_3)
[7] match_1(a_4,l_3,Nil) -> Pair(Nil,Nil)
[8] match_1(a_4,l_3,Cons(x,l')) -> match_2(x,l',a_4,l_3,part(a_4,l'))
[9] 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))
[10] match_3(l1,l2,x,l',a_4,l_3,False) -> Pair(Cons(x,l1),l2)
[11] match_3(l1,l2,x,l',a_4,l_3,True) -> Pair(l1,Cons(x,l2))
[12] quick(l_5) -> match_4(l_5,l_5)
[13] match_4(l_5,Nil) -> Nil
[14] match_4(l_5,Cons(a,l')) -> match_5(a,l',l_5,part(a,l'))
[15] match_5(a,l',l_5,Pair(l1,l2)) -> append(quick(l1),Cons(a,quick(l2)))
 ,
 CRITERION: MDP
 [ {
      
     DP termination of:
     <Marked_append(l1_2,l2_1) , Marked_match_0(l1_2,l2_1,l1_2)>
<Marked_match_0(l1_2,l2_1,Cons(x,l)) , Marked_append(l,l2_1)>
<Marked_part(a_4,l_3) , Marked_match_1(a_4,l_3,l_3)>
<Marked_match_1(a_4,l_3,Cons(x,l')) , Marked_match_2(x,l',a_4,l_3,part(a_4,l'))>
<Marked_match_1(a_4,l_3,Cons(x,l')) , Marked_part(a_4,l')>
<Marked_match_2(x,l',a_4,l_3,Pair(l1,l2)) , Marked_match_3(l1,l2,x,l',
                                             a_4,l_3,test(a_4,x))>
<Marked_match_2(x,l',a_4,l_3,Pair(l1,l2)) , Marked_test(a_4,x)>
<Marked_quick(l_5) , Marked_match_4(l_5,l_5)>
<Marked_match_4(l_5,Cons(a,l')) , Marked_match_5(a,l',l_5,part(a,l'))>
<Marked_match_4(l_5,Cons(a,l')) , Marked_part(a,l')>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_append(quick(l1),
                                         Cons(a,quick(l2)))>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l1)>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l2)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_quick(l_5) , Marked_match_4(l_5,l_5)>
<Marked_match_4(l_5,Cons(a,l')) , Marked_match_5(a,l',l_5,part(a,l'))>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l1)>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l2)>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ True ] () = 0; 
 [ part ] (X0,X1) = 1*X1; 
 [ append ] (X0,X1) = 1*X1 + 1*X0; 
 [ match_4 ] (X0,X1) = 1*X1; 
 [ False ] () = 0; 
 [ Marked_match_4 ] (X0,X1) = 2*X1; 
 [ match_2 ] (X0,X1,X2,X3,X4) = 1*X4 + 2*X0 + 2; 
 [ Cons ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ match_5 ] (X0,X1,X2,X3) = 1*X3 + 2*X0 + 2; 
 [ test ] (X0,X1) = 2*X1 + 3*X0; 
 [ Marked_quick ] (X0) = 2*X0; 
 [ Pair ] (X0,X1) = 1*X1 + 1*X0; 
 [ Nil ] () = 0; 
 [ quick ] (X0) = 1*X0; 
 [ match_0 ] (X0,X1,X2) = 1*X2 + 1*X1; 
 [ match_3 ] (X0,X1,X2,X3,X4,X5,X6) = 2*X2 + 1*X1 + 1*X0 + 2; 
 [ match_1 ] (X0,X1,X2) = 1*X2; 
 [ Marked_match_5 ] (X0,X1,X2,X3) = 2*X3; 
 removing <Marked_match_4(l_5,Cons(a,l')),Marked_match_5(a,l',l_5,part(a,l'))>
 [ {
      
     DP termination of:
     <Marked_quick(l_5) , Marked_match_4(l_5,l_5)>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l1)>
<Marked_match_5(a,l',l_5,Pair(l1,l2)) , Marked_quick(l2)>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
{
 
DP termination of:
<Marked_append(l1_2,l2_1) , Marked_match_0(l1_2,l2_1,l1_2)>
<Marked_match_0(l1_2,l2_1,Cons(x,l)) , Marked_append(l,l2_1)>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ True ] () = 0; 
 [ Marked_append ] (X0,X1) = 3*X1 + 1*X0; 
 [ part ] (X0,X1) = 1*X1 + 2; 
 [ Marked_match_0 ] (X0,X1,X2) = 1*X2 + 3*X1; 
 [ append ] (X0,X1) = 1*X1 + 1*X0; 
 [ match_4 ] (X0,X1) = 2*X1; 
 [ False ] () = 0; 
 [ match_2 ] (X0,X1,X2,X3,X4) = 1*X4 + 2*X0 + 2; 
 [ Cons ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ match_5 ] (X0,X1,X2,X3) = 2*X3 + 2*X0; 
 [ test ] (X0,X1) = 2*X1 + 3*X0; 
 [ Pair ] (X0,X1) = 1*X1 + 1*X0 + 1; 
 [ Nil ] () = 0; 
 [ quick ] (X0) = 2*X0; 
 [ match_0 ] (X0,X1,X2) = 1*X2 + 1*X1; 
 [ match_3 ] (X0,X1,X2,X3,X4,X5,X6) = 2*X2 + 1*X1 + 1*X0 + 3; 
 [ match_1 ] (X0,X1,X2) = 1*X2 + 2; 
 removing <Marked_match_0(l1_2,l2_1,Cons(x,l)),Marked_append(l,l2_1)>
 [ {
      
     DP termination of:
     <Marked_append(l1_2,l2_1) , Marked_match_0(l1_2,l2_1,l1_2)>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
{
 
DP termination of:
<Marked_part(a_4,l_3) , Marked_match_1(a_4,l_3,l_3)>
<Marked_match_1(a_4,l_3,Cons(x,l')) , Marked_part(a_4,l')>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ True ] () = 0; 
 [ part ] (X0,X1) = 1*X1; 
 [ append ] (X0,X1) = 1*X1 + 1*X0; 
 [ match_4 ] (X0,X1) = 1*X1; 
 [ False ] () = 0; 
 [ match_2 ] (X0,X1,X2,X3,X4) = 1*X4 + 1; 
 [ Cons ] (X0,X1) = 1*X1 + 1; 
 [ match_5 ] (X0,X1,X2,X3) = 1*X3 + 1; 
 [ test ] (X0,X1) = 2*X1 + 3*X0; 
 [ Pair ] (X0,X1) = 1*X1 + 1*X0; 
 [ Nil ] () = 0; 
 [ quick ] (X0) = 1*X0; 
 [ match_0 ] (X0,X1,X2) = 1*X2 + 1*X1; 
 [ Marked_part ] (X0,X1) = 2*X1 + 3*X0; 
 [ match_3 ] (X0,X1,X2,X3,X4,X5,X6) = 1*X1 + 1*X0 + 1; 
 [ match_1 ] (X0,X1,X2) = 1*X2; 
 [ Marked_match_1 ] (X0,X1,X2) = 2*X2 + 3*X0; 
 removing <Marked_match_1(a_4,l_3,Cons(x,l')),Marked_part(a_4,l')>
 [ {
      
     DP termination of:
     <Marked_part(a_4,l_3) , Marked_match_1(a_4,l_3,l_3)>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
 ]} 
 ]} 

Cime worked for 0.213123 seconds (real time)
Cime Exit Status: 0