- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] 0(#) -> # [2] +(x,#) -> x [3] +(#,x) -> x [4] +(0(x),0(y)) -> 0(+(x,y)) [5] +(0(x),1(y)) -> 1(+(x,y)) [6] +(1(x),0(y)) -> 1(+(x,y)) [7] +(1(x),1(y)) -> 0(+(+(x,y),1(#))) [8] +(x,+(y,z)) -> +(+(x,y),z) [9] -(x,#) -> x [10] -(#,x) -> # [11] -(0(x),0(y)) -> 0(-(x,y)) [12] -(0(x),1(y)) -> 1(-(-(x,y),1(#))) [13] -(1(x),0(y)) -> 1(-(x,y)) [14] -(1(x),1(y)) -> 0(-(x,y)) [15] not(false) -> true [16] not(true) -> false [17] and(x,true) -> x [18] and(x,false) -> false [19] if(true,x,y) -> x [20] if(false,x,y) -> y [21] ge(0(x),0(y)) -> ge(x,y) [22] ge(0(x),1(y)) -> not(ge(y,x)) [23] ge(1(x),0(y)) -> ge(x,y) [24] ge(1(x),1(y)) -> ge(x,y) [25] ge(x,#) -> true [26] ge(#,1(x)) -> false [27] ge(#,0(x)) -> ge(#,x) [28] val(l(x)) -> x [29] val(n(x,y,z)) -> x [30] min(l(x)) -> x [31] min(n(x,y,z)) -> min(y) [32] max(l(x)) -> x [33] max(n(x,y,z)) -> max(z) [34] bs(l(x)) -> true [35] bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) [36] size(l(x)) -> 1(#) [37] size(n(x,y,z)) -> +(+(size(x),size(y)),1(#)) [38] wb(l(x)) -> true [39] wb(n(x,y,z)) -> and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) Sub problem: guided: DP termination of:

END GUIDED APPLY CRITERIA (Graph splitting) Found 9 components: { --> --> --> --> } { --> } { --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> } { -->

-->

--> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_bs -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_max -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_min -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_wb -> 1 APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { 0(#) >= # ; +(#,x) >= x ; +(0(x),0(y)) >= 0(+(x,y)) ; +(0(x),1(y)) >= 1(+(x,y)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; +(x,+(y,z)) >= +(+(x,y),z) ; -(#,x) >= # ; -(0(x),0(y)) >= 0(-(x,y)) ; -(0(x),1(y)) >= 1(-(-(x,y),1(#))) ; -(1(x),0(y)) >= 1(-(x,y)) ; -(1(x),1(y)) >= 0(-(x,y)) ; -(x,#) >= x ; not(true) >= false ; not(false) >= true ; and(x,true) >= x ; and(x,false) >= false ; if(true,x,y) >= x ; if(false,x,y) >= y ; ge(#,0(x)) >= ge(#,x) ; ge(#,1(x)) >= false ; ge(0(x),0(y)) >= ge(x,y) ; ge(0(x),1(y)) >= not(ge(y,x)) ; ge(1(x),0(y)) >= ge(x,y) ; ge(1(x),1(y)) >= ge(x,y) ; ge(x,#) >= true ; val(l(x)) >= x ; val(n(x,y,z)) >= x ; min(l(x)) >= x ; min(n(x,y,z)) >= min(y) ; max(l(x)) >= x ; max(n(x,y,z)) >= max(z) ; bs(l(x)) >= true ; bs(n(x,y,z)) >= and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) ; size(l(x)) >= 1(#) ; size(n(x,y,z)) >= +(+(size(x),size(y)),1(#)) ; wb(l(x)) >= true ; wb(n(x,y,z)) >= and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) ; Marked_ge(0(x),0(y)) >= Marked_ge(x,y) ; Marked_ge(0(x),1(y)) >= Marked_ge(y,x) ; Marked_ge(1(x),0(y)) >= Marked_ge(x,y) ; Marked_ge(1(x),1(y)) >= Marked_ge(x,y) ; } + Disjunctions:{ { Marked_ge(0(x),0(y)) > Marked_ge(x,y) ; } { Marked_ge(0(x),1(y)) > Marked_ge(y,x) ; } { Marked_ge(1(x),0(y)) > Marked_ge(x,y) ; } { Marked_ge(1(x),1(y)) > Marked_ge(x,y) ; } } === 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: 0(#) >= # constraint: +(#,x) >= x constraint: +(0(x),0(y)) >= 0(+(x,y)) constraint: +(0(x),1(y)) >= 1(+(x,y)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x constraint: +(x,+(y,z)) >= +(+(x,y),z) constraint: -(#,x) >= # constraint: -(0(x),0(y)) >= 0(-(x,y)) constraint: -(0(x),1(y)) >= 1(-(-(x,y),1(#))) constraint: -(1(x),0(y)) >= 1(-(x,y)) constraint: -(1(x),1(y)) >= 0(-(x,y)) constraint: -(x,#) >= x constraint: not(true) >= false constraint: not(false) >= true constraint: and(x,true) >= x constraint: and(x,false) >= false constraint: if(true,x,y) >= x constraint: if(false,x,y) >= y constraint: ge(#,0(x)) >= ge(#,x) constraint: ge(#,1(x)) >= false constraint: ge(0(x),0(y)) >= ge(x,y) constraint: ge(0(x),1(y)) >= not(ge(y,x)) constraint: ge(1(x),0(y)) >= ge(x,y) constraint: ge(1(x),1(y)) >= ge(x,y) constraint: ge(x,#) >= true constraint: val(l(x)) >= x constraint: val(n(x,y,z)) >= x constraint: min(l(x)) >= x constraint: min(n(x,y,z)) >= min(y) constraint: max(l(x)) >= x constraint: max(n(x,y,z)) >= max(z) constraint: bs(l(x)) >= true constraint: bs(n(x,y,z)) >= and(and(ge(x,max(y)),ge(min(z),x)), and(bs(y),bs(z))) constraint: size(l(x)) >= 1(#) constraint: size(n(x,y,z)) >= +(+(size(x),size(y)),1(#)) constraint: wb(l(x)) >= true constraint: wb(n(x,y,z)) >= and(if(ge(size(y),size(z)), ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) constraint: Marked_ge(0(x),0(y)) >= Marked_ge(x,y) constraint: Marked_ge(0(x),1(y)) >= Marked_ge(y,x) constraint: Marked_ge(1(x),0(y)) >= Marked_ge(x,y) constraint: Marked_ge(1(x),1(y)) >= Marked_ge(x,y) APPLY CRITERIA (Subterm criterion) ST: Marked_ge -> 2 APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { 0(#) >= # ; +(#,x) >= x ; +(0(x),0(y)) >= 0(+(x,y)) ; +(0(x),1(y)) >= 1(+(x,y)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; +(x,+(y,z)) >= +(+(x,y),z) ; -(#,x) >= # ; -(0(x),0(y)) >= 0(-(x,y)) ; -(0(x),1(y)) >= 1(-(-(x,y),1(#))) ; -(1(x),0(y)) >= 1(-(x,y)) ; -(1(x),1(y)) >= 0(-(x,y)) ; -(x,#) >= x ; not(true) >= false ; not(false) >= true ; and(x,true) >= x ; and(x,false) >= false ; if(true,x,y) >= x ; if(false,x,y) >= y ; ge(#,0(x)) >= ge(#,x) ; ge(#,1(x)) >= false ; ge(0(x),0(y)) >= ge(x,y) ; ge(0(x),1(y)) >= not(ge(y,x)) ; ge(1(x),0(y)) >= ge(x,y) ; ge(1(x),1(y)) >= ge(x,y) ; ge(x,#) >= true ; val(l(x)) >= x ; val(n(x,y,z)) >= x ; min(l(x)) >= x ; min(n(x,y,z)) >= min(y) ; max(l(x)) >= x ; max(n(x,y,z)) >= max(z) ; bs(l(x)) >= true ; bs(n(x,y,z)) >= and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) ; size(l(x)) >= 1(#) ; size(n(x,y,z)) >= +(+(size(x),size(y)),1(#)) ; wb(l(x)) >= true ; wb(n(x,y,z)) >= and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) ; Marked_-(0(x),0(y)) >= Marked_-(x,y) ; Marked_-(0(x),1(y)) >= Marked_-(-(x,y),1(#)) ; Marked_-(0(x),1(y)) >= Marked_-(x,y) ; Marked_-(1(x),0(y)) >= Marked_-(x,y) ; Marked_-(1(x),1(y)) >= Marked_-(x,y) ; } + Disjunctions:{ { Marked_-(0(x),0(y)) > Marked_-(x,y) ; } { Marked_-(0(x),1(y)) > Marked_-(-(x,y),1(#)) ; } { Marked_-(0(x),1(y)) > Marked_-(x,y) ; } { Marked_-(1(x),0(y)) > Marked_-(x,y) ; } { Marked_-(1(x),1(y)) > Marked_-(x,y) ; } } === 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: 0(#) >= # constraint: +(#,x) >= x constraint: +(0(x),0(y)) >= 0(+(x,y)) constraint: +(0(x),1(y)) >= 1(+(x,y)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x constraint: +(x,+(y,z)) >= +(+(x,y),z) constraint: -(#,x) >= # constraint: -(0(x),0(y)) >= 0(-(x,y)) constraint: -(0(x),1(y)) >= 1(-(-(x,y),1(#))) constraint: -(1(x),0(y)) >= 1(-(x,y)) constraint: -(1(x),1(y)) >= 0(-(x,y)) constraint: -(x,#) >= x constraint: not(true) >= false constraint: not(false) >= true constraint: and(x,true) >= x constraint: and(x,false) >= false constraint: if(true,x,y) >= x constraint: if(false,x,y) >= y constraint: ge(#,0(x)) >= ge(#,x) constraint: ge(#,1(x)) >= false constraint: ge(0(x),0(y)) >= ge(x,y) constraint: ge(0(x),1(y)) >= not(ge(y,x)) constraint: ge(1(x),0(y)) >= ge(x,y) constraint: ge(1(x),1(y)) >= ge(x,y) constraint: ge(x,#) >= true constraint: val(l(x)) >= x constraint: val(n(x,y,z)) >= x constraint: min(l(x)) >= x constraint: min(n(x,y,z)) >= min(y) constraint: max(l(x)) >= x constraint: max(n(x,y,z)) >= max(z) constraint: bs(l(x)) >= true constraint: bs(n(x,y,z)) >= and(and(ge(x,max(y)),ge(min(z),x)), and(bs(y),bs(z))) constraint: size(l(x)) >= 1(#) constraint: size(n(x,y,z)) >= +(+(size(x),size(y)),1(#)) constraint: wb(l(x)) >= true constraint: wb(n(x,y,z)) >= and(if(ge(size(y),size(z)), ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) constraint: Marked_-(0(x),0(y)) >= Marked_-(x,y) constraint: Marked_-(0(x),1(y)) >= Marked_-(-(x,y),1(#)) constraint: Marked_-(0(x),1(y)) >= Marked_-(x,y) constraint: Marked_-(1(x),0(y)) >= Marked_-(x,y) constraint: Marked_-(1(x),1(y)) >= Marked_-(x,y) APPLY CRITERIA (Subterm criterion) ST: Marked_size -> 1 APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { 0(#) >= # ; +(#,x) >= x ; +(0(x),0(y)) >= 0(+(x,y)) ; +(0(x),1(y)) >= 1(+(x,y)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; +(x,+(y,z)) >= +(+(x,y),z) ; -(#,x) >= # ; -(0(x),0(y)) >= 0(-(x,y)) ; -(0(x),1(y)) >= 1(-(-(x,y),1(#))) ; -(1(x),0(y)) >= 1(-(x,y)) ; -(1(x),1(y)) >= 0(-(x,y)) ; -(x,#) >= x ; not(true) >= false ; not(false) >= true ; and(x,true) >= x ; and(x,false) >= false ; if(true,x,y) >= x ; if(false,x,y) >= y ; ge(#,0(x)) >= ge(#,x) ; ge(#,1(x)) >= false ; ge(0(x),0(y)) >= ge(x,y) ; ge(0(x),1(y)) >= not(ge(y,x)) ; ge(1(x),0(y)) >= ge(x,y) ; ge(1(x),1(y)) >= ge(x,y) ; ge(x,#) >= true ; val(l(x)) >= x ; val(n(x,y,z)) >= x ; min(l(x)) >= x ; min(n(x,y,z)) >= min(y) ; max(l(x)) >= x ; max(n(x,y,z)) >= max(z) ; bs(l(x)) >= true ; bs(n(x,y,z)) >= and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) ; size(l(x)) >= 1(#) ; size(n(x,y,z)) >= +(+(size(x),size(y)),1(#)) ; wb(l(x)) >= true ; wb(n(x,y,z)) >= and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) ; Marked_+(0(x),0(y)) >= Marked_+(x,y) ; Marked_+(0(x),1(y)) >= Marked_+(x,y) ; Marked_+(1(x),0(y)) >= Marked_+(x,y) ; Marked_+(1(x),1(y)) >= Marked_+(+(x,y),1(#)) ; Marked_+(1(x),1(y)) >= Marked_+(x,y) ; Marked_+(x,+(y,z)) >= Marked_+(+(x,y),z) ; Marked_+(x,+(y,z)) >= Marked_+(x,y) ; } + Disjunctions:{ { Marked_+(0(x),0(y)) > Marked_+(x,y) ; } { Marked_+(0(x),1(y)) > Marked_+(x,y) ; } { Marked_+(1(x),0(y)) > Marked_+(x,y) ; } { Marked_+(1(x),1(y)) > Marked_+(+(x,y),1(#)) ; } { Marked_+(1(x),1(y)) > Marked_+(x,y) ; } { Marked_+(x,+(y,z)) > Marked_+(+(x,y),z) ; } { Marked_+(x,+(y,z)) > Marked_+(x,y) ; } } === 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: 0(#) >= # constraint: +(#,x) >= x constraint: +(0(x),0(y)) >= 0(+(x,y)) constraint: +(0(x),1(y)) >= 1(+(x,y)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x constraint: +(x,+(y,z)) >= +(+(x,y),z) constraint: -(#,x) >= # constraint: -(0(x),0(y)) >= 0(-(x,y)) constraint: -(0(x),1(y)) >= 1(-(-(x,y),1(#))) constraint: -(1(x),0(y)) >= 1(-(x,y)) constraint: -(1(x),1(y)) >= 0(-(x,y)) constraint: -(x,#) >= x constraint: not(true) >= false constraint: not(false) >= true constraint: and(x,true) >= x constraint: and(x,false) >= false constraint: if(true,x,y) >= x constraint: if(false,x,y) >= y constraint: ge(#,0(x)) >= ge(#,x) constraint: ge(#,1(x)) >= false constraint: ge(0(x),0(y)) >= ge(x,y) constraint: ge(0(x),1(y)) >= not(ge(y,x)) constraint: ge(1(x),0(y)) >= ge(x,y) constraint: ge(1(x),1(y)) >= ge(x,y) constraint: ge(x,#) >= true constraint: val(l(x)) >= x constraint: val(n(x,y,z)) >= x constraint: min(l(x)) >= x constraint: min(n(x,y,z)) >= min(y) constraint: max(l(x)) >= x constraint: max(n(x,y,z)) >= max(z) constraint: bs(l(x)) >= true constraint: bs(n(x,y,z)) >= and(and(ge(x,max(y)),ge(min(z),x)), and(bs(y),bs(z))) constraint: size(l(x)) >= 1(#) constraint: size(n(x,y,z)) >= +(+(size(x),size(y)),1(#)) constraint: wb(l(x)) >= true constraint: wb(n(x,y,z)) >= and(if(ge(size(y),size(z)), ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) constraint: Marked_+(0(x),0(y)) >= Marked_+(x,y) constraint: Marked_+(0(x),1(y)) >= Marked_+(x,y) constraint: Marked_+(1(x),0(y)) >= Marked_+(x,y) constraint: Marked_+(1(x),1(y)) >= Marked_+(+(x,y),1(#)) constraint: Marked_+(1(x),1(y)) >= Marked_+(x,y) constraint: Marked_+(x,+(y,z)) >= Marked_+(+(x,y),z) constraint: Marked_+(x,+(y,z)) >= Marked_+(x,y) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 2 components: { --> --> --> --> } { --> } APPLY CRITERIA (Subterm criterion) ST: Marked_+ -> 2 APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { 0(#) >= # ; +(#,x) >= x ; +(0(x),0(y)) >= 0(+(x,y)) ; +(0(x),1(y)) >= 1(+(x,y)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; +(x,+(y,z)) >= +(+(x,y),z) ; -(#,x) >= # ; -(0(x),0(y)) >= 0(-(x,y)) ; -(0(x),1(y)) >= 1(-(-(x,y),1(#))) ; -(1(x),0(y)) >= 1(-(x,y)) ; -(1(x),1(y)) >= 0(-(x,y)) ; -(x,#) >= x ; not(true) >= false ; not(false) >= true ; and(x,true) >= x ; and(x,false) >= false ; if(true,x,y) >= x ; if(false,x,y) >= y ; ge(#,0(x)) >= ge(#,x) ; ge(#,1(x)) >= false ; ge(0(x),0(y)) >= ge(x,y) ; ge(0(x),1(y)) >= not(ge(y,x)) ; ge(1(x),0(y)) >= ge(x,y) ; ge(1(x),1(y)) >= ge(x,y) ; ge(x,#) >= true ; val(l(x)) >= x ; val(n(x,y,z)) >= x ; min(l(x)) >= x ; min(n(x,y,z)) >= min(y) ; max(l(x)) >= x ; max(n(x,y,z)) >= max(z) ; bs(l(x)) >= true ; bs(n(x,y,z)) >= and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) ; size(l(x)) >= 1(#) ; size(n(x,y,z)) >= +(+(size(x),size(y)),1(#)) ; wb(l(x)) >= true ; wb(n(x,y,z)) >= and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) ; Marked_+(1(x),1(y)) >= Marked_+(+(x,y),1(#)) ; } + Disjunctions:{ { Marked_+(1(x),1(y)) > Marked_+(+(x,y),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: 0(#) >= # constraint: +(#,x) >= x constraint: +(0(x),0(y)) >= 0(+(x,y)) constraint: +(0(x),1(y)) >= 1(+(x,y)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x constraint: +(x,+(y,z)) >= +(+(x,y),z) constraint: -(#,x) >= # constraint: -(0(x),0(y)) >= 0(-(x,y)) constraint: -(0(x),1(y)) >= 1(-(-(x,y),1(#))) constraint: -(1(x),0(y)) >= 1(-(x,y)) constraint: -(1(x),1(y)) >= 0(-(x,y)) constraint: -(x,#) >= x constraint: not(true) >= false constraint: not(false) >= true constraint: and(x,true) >= x constraint: and(x,false) >= false constraint: if(true,x,y) >= x constraint: if(false,x,y) >= y constraint: ge(#,0(x)) >= ge(#,x) constraint: ge(#,1(x)) >= false constraint: ge(0(x),0(y)) >= ge(x,y) constraint: ge(0(x),1(y)) >= not(ge(y,x)) constraint: ge(1(x),0(y)) >= ge(x,y) constraint: ge(1(x),1(y)) >= ge(x,y) constraint: ge(x,#) >= true constraint: val(l(x)) >= x constraint: val(n(x,y,z)) >= x constraint: min(l(x)) >= x constraint: min(n(x,y,z)) >= min(y) constraint: max(l(x)) >= x constraint: max(n(x,y,z)) >= max(z) constraint: bs(l(x)) >= true constraint: bs(n(x,y,z)) >= and(and(ge(x,max(y)),ge(min(z),x)), and(bs(y),bs(z))) constraint: size(l(x)) >= 1(#) constraint: size(n(x,y,z)) >= +(+(size(x),size(y)),1(#)) constraint: wb(l(x)) >= true constraint: wb(n(x,y,z)) >= and(if(ge(size(y),size(z)), ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) constraint: Marked_+(1(x),1(y)) >= Marked_+(+(x,y),1(#)) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] 0(#) -> # [2] +(x,#) -> x [3] +(#,x) -> x [4] +(0(x),0(y)) -> 0(+(x,y)) [5] +(0(x),1(y)) -> 1(+(x,y)) [6] +(1(x),0(y)) -> 1(+(x,y)) [7] +(1(x),1(y)) -> 0(+(+(x,y),1(#))) [8] +(x,+(y,z)) -> +(+(x,y),z) [9] -(x,#) -> x [10] -(#,x) -> # [11] -(0(x),0(y)) -> 0(-(x,y)) [12] -(0(x),1(y)) -> 1(-(-(x,y),1(#))) [13] -(1(x),0(y)) -> 1(-(x,y)) [14] -(1(x),1(y)) -> 0(-(x,y)) [15] not(false) -> true [16] not(true) -> false [17] and(x,true) -> x [18] and(x,false) -> false [19] if(true,x,y) -> x [20] if(false,x,y) -> y [21] ge(0(x),0(y)) -> ge(x,y) [22] ge(0(x),1(y)) -> not(ge(y,x)) [23] ge(1(x),0(y)) -> ge(x,y) [24] ge(1(x),1(y)) -> ge(x,y) [25] ge(x,#) -> true [26] ge(#,1(x)) -> false [27] ge(#,0(x)) -> ge(#,x) [28] val(l(x)) -> x [29] val(n(x,y,z)) -> x [30] min(l(x)) -> x [31] min(n(x,y,z)) -> min(y) [32] max(l(x)) -> x [33] max(n(x,y,z)) -> max(z) [34] bs(l(x)) -> true [35] bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) [36] size(l(x)) -> 1(#) [37] size(n(x,y,z)) -> +(+(size(x),size(y)),1(#)) [38] wb(l(x)) -> true [39] wb(n(x,y,z)) -> and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))), ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) , CRITERION: MDP [ { DP termination of:

, CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ # ] () = 0; [ bs ] (X0) = 0; [ and ] (X0,X1) = 2*X0 + 0; [ - ] (X0,X1) = 1*X0 + 0; [ l ] (X0) = 1 + 3*X0 + 0; [ + ] (X0,X1) = 1*X0 + 2*X1 + 0; [ wb ] (X0) = 0; [ ge ] (X0,X1) = 0; [ not ] (X0) = 0; [ Marked_ge ] (X0,X1) = 1*X0 + 1*X1 + 0; [ min ] (X0) = 2*X0 + 0; [ 0 ] (X0) = 1 + 1*X0 + 0; [ size ] (X0) = 2*X0 + 0; [ if ] (X0,X1,X2) = 2*X1 + 2*X2 + 0; [ true ] () = 0; [ n ] (X0,X1,X2) = 2 + 2*X0 + 2*X1 + 2*X2 + 0; [ 1 ] (X0) = 1 + 1*X0 + 0; [ val ] (X0) = 3 + 3*X0 + 0; [ false ] () = 0; [ max ] (X0) = 1*X0 + 0; ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of:

, CRITERION: ORD [ Solution found: polynomial interpretation = [ # ] () = 0; [ bs ] (X0) = 2 + 0; [ and ] (X0,X1) = 1*X0 + 0; [ Marked_- ] (X0,X1) = 2*X0 + 2*X1 + 0; [ - ] (X0,X1) = 1*X0 + 0; [ l ] (X0) = 2 + 3*X0 + 0; [ + ] (X0,X1) = 1*X0 + 2*X1 + 0; [ wb ] (X0) = 0; [ ge ] (X0,X1) = 0; [ not ] (X0) = 0; [ min ] (X0) = 1*X0 + 0; [ 0 ] (X0) = 2 + 1*X0 + 0; [ size ] (X0) = 2*X0 + 0; [ if ] (X0,X1,X2) = 1*X1 + 1*X2 + 0; [ true ] () = 0; [ n ] (X0,X1,X2) = 2 + 1*X0 + 2*X1 + 2*X2 + 0; [ 1 ] (X0) = 2 + 1*X0 + 0; [ val ] (X0) = 2 + 3*X0 + 0; [ false ] () = 0; [ max ] (X0) = 1*X0 + 0; ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ # ] () = 0; [ bs ] (X0) = 0; [ and ] (X0,X1) = 1*X0; [ - ] (X0,X1) = 1*X0; [ l ] (X0) = 3*X0 + 1; [ + ] (X0,X1) = 2*X1 + 1*X0; [ wb ] (X0) = 2; [ ge ] (X0,X1) = 0; [ not ] (X0) = 0; [ min ] (X0) = 1*X0; [ 0 ] (X0) = 1*X0 + 2; [ size ] (X0) = 2*X0; [ if ] (X0,X1,X2) = 1*X2 + 2*X1; [ Marked_+ ] (X0,X1) = 2*X1; [ true ] () = 0; [ n ] (X0,X1,X2) = 1*X2 + 3*X1 + 2*X0 + 2; [ 1 ] (X0) = 1*X0 + 2; [ val ] (X0) = 3*X0 + 3; [ false ] () = 0; [ max ] (X0) = 2*X0; removing < Marked_+(1(x),0(y)),Marked_+(x,y)> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ # ] () = 0; [ bs ] (X0) = 3*X0 + 0; [ and ] (X0,X1) = 1*X0 + 0; [ - ] (X0,X1) = 1*X0 + 0; [ l ] (X0) = 3*X0 + 0; [ + ] (X0,X1) = 1*X0 + 1*X1 + 0; [ wb ] (X0) = 3 + 1*X0 + 0; [ ge ] (X0,X1) = 2*X0 + 0; [ not ] (X0) = 0; [ min ] (X0) = 1*X0 + 0; [ 0 ] (X0) = 1 + 1*X0 + 0; [ size ] (X0) = 1 + 1*X0 + 0; [ if ] (X0,X1,X2) = 1*X1 + 1*X2 + 0; [ Marked_+ ] (X0,X1) = 1*X0 + 2*X1 + 0; [ true ] () = 0; [ n ] (X0,X1,X2) = 2 + 3*X0 + 1*X1 + 2*X2 + 0; [ 1 ] (X0) = 1 + 1*X0 + 0; [ val ] (X0) = 2 + 3*X0 + 0; [ false ] () = 0; [ max ] (X0) = 1*X0 + 0; ]} ]} ]} ]} ]} Cime worked for 1.047417 seconds (real time) Cime Exit Status: 0