- : 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) -> # [10] -(x,#) -> 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(true) -> false [16] not(false) -> true [17] if(true,x,y) -> x [18] if(false,x,y) -> y [19] ge(0(x),0(y)) -> ge(x,y) [20] ge(0(x),1(y)) -> not(ge(y,x)) [21] ge(1(x),0(y)) -> ge(x,y) [22] ge(1(x),1(y)) -> ge(x,y) [23] ge(x,#) -> true [24] ge(#,0(x)) -> ge(#,x) [25] ge(#,1(x)) -> false [26] log(x) -> -(log'(x),1(#)) [27] log'(#) -> # [28] log'(1(x)) -> +(log'(x),1(#)) [29] log'(0(x)) -> if(ge(x,1(#)),+(log'(x),1(#)),#) Sub problem: guided: DP termination of:

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

-->

--> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } 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)) ; +(+(x,y),z) >= +(x,+(y,z)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; -(#,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(false) >= true ; not(true) >= false ; if(false,x,y) >= y ; if(true,x,y) >= x ; 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 ; log'(#) >= # ; log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) ; log'(1(x)) >= +(log'(x),1(#)) ; log(x) >= -(log'(x),1(#)) ; 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: +(+(x,y),z) >= +(x,+(y,z)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x 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(false) >= true constraint: not(true) >= false constraint: if(false,x,y) >= y constraint: if(true,x,y) >= x 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: log'(#) >= # constraint: log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) constraint: log'(1(x)) >= +(log'(x),1(#)) constraint: log(x) >= -(log'(x),1(#)) 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 (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)) ; +(+(x,y),z) >= +(x,+(y,z)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; -(#,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(false) >= true ; not(true) >= false ; if(false,x,y) >= y ; if(true,x,y) >= x ; 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 ; log'(#) >= # ; log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) ; log'(1(x)) >= +(log'(x),1(#)) ; log(x) >= -(log'(x),1(#)) ; Marked_log'(0(x)) >= Marked_log'(x) ; Marked_log'(1(x)) >= Marked_log'(x) ; } + Disjunctions:{ { Marked_log'(0(x)) > Marked_log'(x) ; } { Marked_log'(1(x)) > Marked_log'(x) ; } } === 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: +(+(x,y),z) >= +(x,+(y,z)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x 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(false) >= true constraint: not(true) >= false constraint: if(false,x,y) >= y constraint: if(true,x,y) >= x 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: log'(#) >= # constraint: log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) constraint: log'(1(x)) >= +(log'(x),1(#)) constraint: log(x) >= -(log'(x),1(#)) constraint: Marked_log'(0(x)) >= Marked_log'(x) constraint: Marked_log'(1(x)) >= Marked_log'(x) 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)) ; +(+(x,y),z) >= +(x,+(y,z)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; -(#,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(false) >= true ; not(true) >= false ; if(false,x,y) >= y ; if(true,x,y) >= x ; 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 ; log'(#) >= # ; log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) ; log'(1(x)) >= +(log'(x),1(#)) ; log(x) >= -(log'(x),1(#)) ; 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: +(+(x,y),z) >= +(x,+(y,z)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x 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(false) >= true constraint: not(true) >= false constraint: if(false,x,y) >= y constraint: if(true,x,y) >= x 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: log'(#) >= # constraint: log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) constraint: log'(1(x)) >= +(log'(x),1(#)) constraint: log(x) >= -(log'(x),1(#)) 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 (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)) ; +(+(x,y),z) >= +(x,+(y,z)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; -(#,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(false) >= true ; not(true) >= false ; if(false,x,y) >= y ; if(true,x,y) >= x ; 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 ; log'(#) >= # ; log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) ; log'(1(x)) >= +(log'(x),1(#)) ; log(x) >= -(log'(x),1(#)) ; Marked_ge(#,0(x)) >= Marked_ge(#,x) ; } + Disjunctions:{ { Marked_ge(#,0(x)) > Marked_ge(#,x) ; } } === 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: +(+(x,y),z) >= +(x,+(y,z)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x 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(false) >= true constraint: not(true) >= false constraint: if(false,x,y) >= y constraint: if(true,x,y) >= x 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: log'(#) >= # constraint: log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) constraint: log'(1(x)) >= +(log'(x),1(#)) constraint: log(x) >= -(log'(x),1(#)) constraint: Marked_ge(#,0(x)) >= Marked_ge(#,x) 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)) ; +(+(x,y),z) >= +(x,+(y,z)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; -(#,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(false) >= true ; not(true) >= false ; if(false,x,y) >= y ; if(true,x,y) >= x ; 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 ; log'(#) >= # ; log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) ; log'(1(x)) >= +(log'(x),1(#)) ; log(x) >= -(log'(x),1(#)) ; Marked_+(0(x),0(y)) >= Marked_+(x,y) ; Marked_+(0(x),1(y)) >= Marked_+(x,y) ; Marked_+(+(x,y),z) >= Marked_+(y,z) ; Marked_+(+(x,y),z) >= Marked_+(x,+(y,z)) ; 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) ; } + Disjunctions:{ { Marked_+(0(x),0(y)) > Marked_+(x,y) ; } { Marked_+(0(x),1(y)) > Marked_+(x,y) ; } { Marked_+(+(x,y),z) > Marked_+(y,z) ; } { Marked_+(+(x,y),z) > Marked_+(x,+(y,z)) ; } { 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) ; } } === 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: +(+(x,y),z) >= +(x,+(y,z)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x 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(false) >= true constraint: not(true) >= false constraint: if(false,x,y) >= y constraint: if(true,x,y) >= x 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: log'(#) >= # constraint: log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) constraint: log'(1(x)) >= +(log'(x),1(#)) constraint: log(x) >= -(log'(x),1(#)) constraint: Marked_+(0(x),0(y)) >= Marked_+(x,y) constraint: Marked_+(0(x),1(y)) >= Marked_+(x,y) constraint: Marked_+(+(x,y),z) >= Marked_+(y,z) constraint: Marked_+(+(x,y),z) >= Marked_+(x,+(y,z)) 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) 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 1 components: { --> --> --> --> } 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)) ; +(+(x,y),z) >= +(x,+(y,z)) ; +(1(x),0(y)) >= 1(+(x,y)) ; +(1(x),1(y)) >= 0(+(+(x,y),1(#))) ; +(x,#) >= x ; -(#,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(false) >= true ; not(true) >= false ; if(false,x,y) >= y ; if(true,x,y) >= x ; 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 ; log'(#) >= # ; log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) ; log'(1(x)) >= +(log'(x),1(#)) ; log(x) >= -(log'(x),1(#)) ; Marked_+(+(x,y),z) >= Marked_+(y,z) ; Marked_+(+(x,y),z) >= Marked_+(x,+(y,z)) ; } + Disjunctions:{ { Marked_+(+(x,y),z) > Marked_+(y,z) ; } { Marked_+(+(x,y),z) > Marked_+(x,+(y,z)) ; } } === 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 === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.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: +(+(x,y),z) >= +(x,+(y,z)) constraint: +(1(x),0(y)) >= 1(+(x,y)) constraint: +(1(x),1(y)) >= 0(+(+(x,y),1(#))) constraint: +(x,#) >= x 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(false) >= true constraint: not(true) >= false constraint: if(false,x,y) >= y constraint: if(true,x,y) >= x 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: log'(#) >= # constraint: log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) constraint: log'(1(x)) >= +(log'(x),1(#)) constraint: log(x) >= -(log'(x),1(#)) constraint: Marked_+(+(x,y),z) >= Marked_+(y,z) constraint: Marked_+(+(x,y),z) >= Marked_+(x,+(y,z)) 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) -> # [10] -(x,#) -> 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(true) -> false [16] not(false) -> true [17] if(true,x,y) -> x [18] if(false,x,y) -> y [19] ge(0(x),0(y)) -> ge(x,y) [20] ge(0(x),1(y)) -> not(ge(y,x)) [21] ge(1(x),0(y)) -> ge(x,y) [22] ge(1(x),1(y)) -> ge(x,y) [23] ge(x,#) -> true [24] ge(#,0(x)) -> ge(#,x) [25] ge(#,1(x)) -> false [26] log(x) -> -(log'(x),1(#)) [27] log'(#) -> # [28] log'(1(x)) -> +(log'(x),1(#)) [29] log'(0(x)) -> if(ge(x,1(#)),+(log'(x),1(#)),#) , CRITERION: MDP [ { DP termination of:

, CRITERION: SG [ { DP termination of:

, CRITERION: ORD [ Solution found: polynomial interpretation = [ # ] () = 0; [ if ] (X0,X1,X2) = 1*X1 + 1*X2 + 0; [ - ] (X0,X1) = 1*X0 + 0; [ + ] (X0,X1) = 1*X0 + 1*X1 + 0; [ log' ] (X0) = 1*X0 + 0; [ not ] (X0) = 0; [ 0 ] (X0) = 2 + 1*X0 + 0; [ Marked_- ] (X0,X1) = 2*X0 + 2*X1 + 0; [ ge ] (X0,X1) = 2 + 3*X0 + 0; [ false ] () = 0; [ 1 ] (X0) = 2 + 1*X0 + 0; [ log ] (X0) = 1 + 1*X0 + 0; [ true ] () = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ # ] () = 0; [ if ] (X0,X1,X2) = 1*X1 + 2*X2 + 0; [ - ] (X0,X1) = 1*X0 + 0; [ Marked_log' ] (X0) = 3*X0 + 0; [ + ] (X0,X1) = 1*X0 + 1*X1 + 0; [ log' ] (X0) = 1*X0 + 0; [ not ] (X0) = 0; [ 0 ] (X0) = 1 + 1*X0 + 0; [ ge ] (X0,X1) = 2*X1 + 0; [ false ] () = 0; [ 1 ] (X0) = 1 + 1*X0 + 0; [ log ] (X0) = 1 + 1*X0 + 0; [ true ] () = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ # ] () = 0; [ if ] (X0,X1,X2) = 1*X1 + 1*X2 + 0; [ - ] (X0,X1) = 1*X0 + 0; [ + ] (X0,X1) = 1*X0 + 1*X1 + 0; [ log' ] (X0) = 1*X0 + 0; [ not ] (X0) = 0; [ Marked_ge ] (X0,X1) = 2*X0 + 2*X1 + 0; [ 0 ] (X0) = 2 + 1*X0 + 0; [ ge ] (X0,X1) = 0; [ false ] () = 0; [ 1 ] (X0) = 2 + 1*X0 + 0; [ log ] (X0) = 1 + 1*X0 + 0; [ true ] () = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ # ] () = 0; [ if ] (X0,X1,X2) = 1*X1 + 1*X2 + 0; [ - ] (X0,X1) = 1*X0 + 2*X1 + 0; [ + ] (X0,X1) = 1*X0 + 1*X1 + 0; [ log' ] (X0) = 2*X0 + 0; [ not ] (X0) = 0; [ Marked_ge ] (X0,X1) = 3*X1 + 0; [ 0 ] (X0) = 1 + 1*X0 + 0; [ ge ] (X0,X1) = 2 + 1*X0 + 3*X1 + 0; [ false ] () = 0; [ 1 ] (X0) = 1 + 1*X0 + 0; [ log ] (X0) = 3 + 2*X0 + 0; [ true ] () = 0; ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ # ] () = 0; [ if ] (X0,X1,X2) = 2*X2 + 1*X1 + 2; [ - ] (X0,X1) = 1*X0; [ + ] (X0,X1) = 1*X1 + 1*X0; [ log' ] (X0) = 3*X0; [ not ] (X0) = 0; [ 0 ] (X0) = 1*X0 + 2; [ ge ] (X0,X1) = 2*X0; [ false ] () = 0; [ 1 ] (X0) = 1*X0 + 2; [ log ] (X0) = 3*X0 + 1; [ true ] () = 0; [ Marked_+ ] (X0,X1) = 2*X1 + 2*X0; removing < Marked_+(1(x),0(y)),Marked_+(x,y)>< Marked_+(1(x),1(y)),Marked_+(x,y)> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: Matrix polynomial interpretation (strict sub matrices size: 1x1) = [ # ] () = [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ if ] (X0,X1,X2) = [ [ 1 , 0 , 0 ] [ 0 , 1 , 0 ] [ 0 , 0 , 1 ] ]*X2 + [ [ 1 , 0 , 0 ] [ 0 , 1 , 0 ] [ 0 , 0 , 1 ] ]*X1 + [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X0 + [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ - ] (X0,X1) = [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X1 + [ [ 1 , 0 , 0 ] [ 0 , 1 , 0 ] [ 0 , 0 , 1 ] ]*X0 + [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ + ] (X0,X1) = [ [ 1 , 0 , 0 ] [ 0 , 1 , 0 ] [ 0 , 0 , 1 ] ]*X1 + [ [ 1 , 0 , 0 ] [ 0 , 1 , 0 ] [ 0 , 0 , 1 ] ]*X0 + [ [ 0 , 0 , 0 ] [ 1 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ log' ] (X0) = [ [ 1 , 0 , 0 ] [ 1 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X0 + [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ not ] (X0) = [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X0 + [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ 0 ] (X0) = [ [ 1 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X0 + [ [ 1 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ ge ] (X0,X1) = [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X1 + [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X0 + [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ false ] () = [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ 1 ] (X0) = [ [ 1 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X0 + [ [ 1 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ log ] (X0) = [ [ 1 , 0 , 0 ] [ 1 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X0 + [ [ 0 , 1 , 1 ] [ 0 , 1 , 1 ] [ 1 , 1 , 0 ] ]; [ true ] () = [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; [ Marked_+ ] (X0,X1) = [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X1 + [ [ 0 , 1 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]*X0 + [ [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] [ 0 , 0 , 0 ] ]; ]} ]} ]} ]} ]} Cime worked for 4.937323 seconds (real time) Cime Exit Status: 0