- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t))))) [2] sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(te(a),sortSu(t))))) -> sortSu(cons(te(a),sortSu(circ(sortSu(s),sortSu(t))))) [3] sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(sop(lift),sortSu(t))))) -> sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))) [4] sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) [5] sortSu(circ(sortSu(s),sortSu(id))) -> sortSu(s) [6] sortSu(circ(sortSu(id),sortSu(s))) -> sortSu(s) [7] sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) -> sortSu(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))), sortSu(u))) [8] te(subst(te(a),sortSu(id))) -> te(a) [9] te(msubst(te(a),sortSu(id))) -> te(a) [10] te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) >= sortSu(cons( te( msubst( te( a), sortSu(t))), sortSu( circ( sortSu( s), sortSu(t))))) ; sortSu(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) >= sortSu(cons(te(a),sortSu(circ(sortSu(s),sortSu(t))))) ; sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(sop(lift),sortSu(t))))) >= sortSu(cons(sop(lift), sortSu(circ( sortSu(s), sortSu(t))))) ; sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) >= sortSu(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))), sortSu(u))) ; sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) >= sortSu( circ( sortSu(s), sortSu( circ( sortSu( t), sortSu(u))))) ; sortSu(circ(sortSu(id),sortSu(s))) >= sortSu(s) ; sortSu(circ(sortSu(s),sortSu(id))) >= sortSu(s) ; te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) >= te(msubst(te(a), sortSu(circ( sortSu( s), sortSu(t))))) ; te(msubst(te(a),sortSu(id))) >= te(a) ; te(subst(te(a),sortSu(id))) >= te(a) ; Marked_te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) >= Marked_te( msubst( te(a), sortSu( circ( sortSu(s), sortSu(t))))) ; Marked_te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) >= Marked_sortSu( circ(sortSu(s), sortSu(t))) ; Marked_sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) >= Marked_te( msubst( te(a), sortSu(t))) ; Marked_sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) >= Marked_sortSu( circ( sortSu( s), sortSu(t))) ; Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(te(a),sortSu(t))))) >= Marked_sortSu(circ( sortSu( s), sortSu(t))) ; Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(sop(lift),sortSu(t))))) >= Marked_sortSu( circ(sortSu(s), sortSu(t))) ; Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) >= Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))), sortSu(u))) ; Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) >= Marked_sortSu(circ(sortSu(s),sortSu(t))) ; Marked_sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) >= Marked_sortSu(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) ; Marked_sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) >= Marked_sortSu(circ(sortSu(t),sortSu(u))) ; } + Disjunctions:{ { Marked_te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) > Marked_te( msubst( te(a), sortSu( circ( sortSu(s), sortSu(t))))) ; } { Marked_te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) > Marked_sortSu( circ(sortSu(s), sortSu(t))) ; } { Marked_sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) > Marked_te( msubst( te(a), sortSu(t))) ; } { Marked_sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) > Marked_sortSu( circ( sortSu( s), sortSu(t))) ; } { Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(te(a),sortSu(t))))) > Marked_sortSu(circ( sortSu(s), sortSu(t))) ; } { Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(sop(lift),sortSu(t))))) > Marked_sortSu( circ(sortSu(s), sortSu(t))) ; } { Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) > Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))), sortSu(u))) ; } { Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) > Marked_sortSu(circ(sortSu(s),sortSu(t))) ; } { Marked_sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) > Marked_sortSu(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) ; } { Marked_sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) > Marked_sortSu(circ(sortSu(t),sortSu(u))) ; } } === 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 : 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 : 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 : 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 : 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 timeout reached === STOPING TIMER virtual === Time out 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 === 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 148.192835 seconds (real time) Cime Exit Status: 0