- : unit = () h : 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: END GUIDED APPLY CRITERIA (Graph splitting) Found 3 components: { --> --> --> --> --> } { --> --> } { --> --> } 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: , CRITERION: SG [ { DP termination of: , 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 [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , 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 [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , 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 [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 0.213123 seconds (real time) Cime Exit Status: 0