- : 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) -> # [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] eq(#,#) -> true [20] eq(#,1(y)) -> false [21] eq(1(x),#) -> false [22] eq(#,0(y)) -> eq(#,y) [23] eq(0(x),#) -> eq(x,#) [24] eq(1(x),1(y)) -> eq(x,y) [25] eq(0(x),1(y)) -> false [26] eq(1(x),0(y)) -> false [27] eq(0(x),0(y)) -> eq(x,y) [28] ge(0(x),0(y)) -> ge(x,y) [29] ge(0(x),1(y)) -> not(ge(y,x)) [30] ge(1(x),0(y)) -> ge(x,y) [31] ge(1(x),1(y)) -> ge(x,y) [32] ge(x,#) -> true [33] ge(#,0(x)) -> ge(#,x) [34] ge(#,1(x)) -> false [35] log(x) -> -(log'(x),1(#)) [36] log'(#) -> # [37] log'(1(x)) -> +(log'(x),1(#)) [38] log'(0(x)) -> if(ge(x,1(#)),+(log'(x),1(#)),#) [39] *(#,x) -> # [40] *(0(x),y) -> 0( *(x,y)) [41] *(1(x),y) -> +(0( *(x,y)),y) [42] *( *(x,y),z) -> *(x, *(y,z)) [43] *(x,+(y,z)) -> +( *(x,y), *(x,z)) [44] app(nil,l) -> l [45] app(cons(x,l1),l2) -> cons(x,app(l1,l2)) [46] sum(nil) -> 0(#) [47] sum(cons(x,l)) -> +(x,sum(l)) [48] sum(app(l1,l2)) -> +(sum(l1),sum(l2)) [49] prod(nil) -> 1(#) [50] prod(cons(x,l)) -> *(x,prod(l)) [51] prod(app(l1,l2)) -> *(prod(l1),prod(l2)) [52] mem(x,nil) -> false [53] mem(x,cons(y,l)) -> if(eq(x,y),true,mem(x,l)) [54] inter(x,nil) -> nil [55] inter(nil,x) -> nil [56] inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3)) [57] inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3)) [58] inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2) [59] inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1) [60] ifinter(true,x,l1,l2) -> cons(x,inter(l1,l2)) [61] ifinter(false,x,l1,l2) -> inter(l1,l2) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 14 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> } { --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> } { --> } { --> --> --> --> } { --> } { --> } 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)) ; +(+(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 ; eq(#,#) >= true ; eq(#,0(y)) >= eq(#,y) ; eq(#,1(y)) >= false ; eq(0(x),#) >= eq(x,#) ; eq(0(x),0(y)) >= eq(x,y) ; eq(0(x),1(y)) >= false ; eq(1(x),#) >= false ; eq(1(x),0(y)) >= false ; eq(1(x),1(y)) >= eq(x,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 ; log'(#) >= # ; log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) ; log'(1(x)) >= +(log'(x),1(#)) ; log(x) >= -(log'(x),1(#)) ; *(#,x) >= # ; *(0(x),y) >= 0( *(x,y)) ; *(1(x),y) >= +(0( *(x,y)),y) ; *( *(x,y),z) >= *(x, *(y,z)) ; *(x,+(y,z)) >= +( *(x,y), *(x,z)) ; app(nil,l) >= l ; app(cons(x,l1),l2) >= cons(x,app(l1,l2)) ; sum(app(l1,l2)) >= +(sum(l1),sum(l2)) ; sum(nil) >= 0(#) ; sum(cons(x,l)) >= +(x,sum(l)) ; prod(app(l1,l2)) >= *(prod(l1),prod(l2)) ; prod(nil) >= 1(#) ; prod(cons(x,l)) >= *(x,prod(l)) ; mem(x,nil) >= false ; mem(x,cons(y,l)) >= if(eq(x,y),true,mem(x,l)) ; inter(app(l1,l2),l3) >= app(inter(l1,l3),inter(l2,l3)) ; inter(nil,x) >= nil ; inter(cons(x,l1),l2) >= ifinter(mem(x,l2),x,l1,l2) ; inter(l1,app(l2,l3)) >= app(inter(l1,l2),inter(l1,l3)) ; inter(l1,cons(x,l2)) >= ifinter(mem(x,l1),x,l2,l1) ; inter(x,nil) >= nil ; ifinter(false,x,l1,l2) >= inter(l1,l2) ; ifinter(true,x,l1,l2) >= cons(x,inter(l1,l2)) ; 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 === 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 === Time out for these parameters. === 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 === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (Simple graph) Found 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 ; eq(#,#) >= true ; eq(#,0(y)) >= eq(#,y) ; eq(#,1(y)) >= false ; eq(0(x),#) >= eq(x,#) ; eq(0(x),0(y)) >= eq(x,y) ; eq(0(x),1(y)) >= false ; eq(1(x),#) >= false ; eq(1(x),0(y)) >= false ; eq(1(x),1(y)) >= eq(x,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 ; log'(#) >= # ; log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) ; log'(1(x)) >= +(log'(x),1(#)) ; log(x) >= -(log'(x),1(#)) ; *(#,x) >= # ; *(0(x),y) >= 0( *(x,y)) ; *(1(x),y) >= +(0( *(x,y)),y) ; *( *(x,y),z) >= *(x, *(y,z)) ; *(x,+(y,z)) >= +( *(x,y), *(x,z)) ; app(nil,l) >= l ; app(cons(x,l1),l2) >= cons(x,app(l1,l2)) ; sum(app(l1,l2)) >= +(sum(l1),sum(l2)) ; sum(nil) >= 0(#) ; sum(cons(x,l)) >= +(x,sum(l)) ; prod(app(l1,l2)) >= *(prod(l1),prod(l2)) ; prod(nil) >= 1(#) ; prod(cons(x,l)) >= *(x,prod(l)) ; mem(x,nil) >= false ; mem(x,cons(y,l)) >= if(eq(x,y),true,mem(x,l)) ; inter(app(l1,l2),l3) >= app(inter(l1,l3),inter(l2,l3)) ; inter(nil,x) >= nil ; inter(cons(x,l1),l2) >= ifinter(mem(x,l2),x,l1,l2) ; inter(l1,app(l2,l3)) >= app(inter(l1,l2),inter(l1,l3)) ; inter(l1,cons(x,l2)) >= ifinter(mem(x,l1),x,l2,l1) ; inter(x,nil) >= nil ; ifinter(false,x,l1,l2) >= inter(l1,l2) ; ifinter(true,x,l1,l2) >= cons(x,inter(l1,l2)) ; 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) ; } APPLY CRITERIA (SOLVE_ORD) 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 ; eq(#,#) >= true ; eq(#,0(y)) >= eq(#,y) ; eq(#,1(y)) >= false ; eq(0(x),#) >= eq(x,#) ; eq(0(x),0(y)) >= eq(x,y) ; eq(0(x),1(y)) >= false ; eq(1(x),#) >= false ; eq(1(x),0(y)) >= false ; eq(1(x),1(y)) >= eq(x,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 ; log'(#) >= # ; log'(0(x)) >= if(ge(x,1(#)),+(log'(x),1(#)),#) ; log'(1(x)) >= +(log'(x),1(#)) ; log(x) >= -(log'(x),1(#)) ; *(#,x) >= # ; *(0(x),y) >= 0( *(x,y)) ; *(1(x),y) >= +(0( *(x,y)),y) ; *( *(x,y),z) >= *(x, *(y,z)) ; *(x,+(y,z)) >= +( *(x,y), *(x,z)) ; app(nil,l) >= l ; app(cons(x,l1),l2) >= cons(x,app(l1,l2)) ; sum(app(l1,l2)) >= +(sum(l1),sum(l2)) ; sum(nil) >= 0(#) ; sum(cons(x,l)) >= +(x,sum(l)) ; prod(app(l1,l2)) >= *(prod(l1),prod(l2)) ; prod(nil) >= 1(#) ; prod(cons(x,l)) >= *(x,prod(l)) ; mem(x,nil) >= false ; mem(x,cons(y,l)) >= if(eq(x,y),true,mem(x,l)) ; inter(app(l1,l2),l3) >= app(inter(l1,l3),inter(l2,l3)) ; inter(nil,x) >= nil ; inter(cons(x,l1),l2) >= ifinter(mem(x,l2),x,l1,l2) ; inter(l1,app(l2,l3)) >= app(inter(l1,l2),inter(l1,l3)) ; inter(l1,cons(x,l2)) >= ifinter(mem(x,l1),x,l2,l1) ; inter(x,nil) >= nil ; ifinter(false,x,l1,l2) >= inter(l1,l2) ; ifinter(true,x,l1,l2) >= cons(x,inter(l1,l2)) ; 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:{ } === 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 === Time out for these parameters. === 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 === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (ID_CRIT) NOT SOLVED No proof found Cime worked for 60.094068 seconds (real time) Cime Exit Status: 0