- : unit = () - : 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 (Subterm criterion) 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 (Simple graph) Found 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))) ; } APPLY CRITERIA (SOLVE_ORD) 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:{ } === 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 === No solution found for these parameters.(1149 bt (792) [787]) === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) >= sortSu(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t))))) constraint: sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(te(a),sortSu(t))))) >= sortSu(cons(te(a), sortSu( circ( sortSu(s), sortSu(t))))) constraint: sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(sop(lift),sortSu(t))))) >= sortSu(cons( sop( lift), sortSu( circ( sortSu( s), sortSu(t))))) constraint: 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))) constraint: sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) >= sortSu(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) constraint: sortSu(circ(sortSu(id),sortSu(s))) >= sortSu(s) constraint: sortSu(circ(sortSu(s),sortSu(id))) >= sortSu(s) constraint: te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) >= te(msubst( te( a), sortSu( circ( sortSu( s), sortSu(t))))) constraint: te(msubst(te(a),sortSu(id))) >= te(a) constraint: te(subst(te(a),sortSu(id))) >= te(a) constraint: Marked_te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) > Marked_te(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) constraint: Marked_te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) >= Marked_sortSu(circ(sortSu(s),sortSu(t))) constraint: Marked_sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) > Marked_te(msubst(te(a),sortSu(t))) constraint: Marked_sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) > Marked_sortSu(circ(sortSu(s),sortSu(t))) constraint: Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(te(a),sortSu(t))))) > Marked_sortSu( circ(sortSu(s), sortSu(t))) constraint: Marked_sortSu(circ(sortSu(cons(sop(lift),sortSu(s))), sortSu(cons(sop(lift),sortSu(t))))) > Marked_sortSu( circ( sortSu( s), sortSu(t))) constraint: 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))) constraint: 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))) constraint: Marked_sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) > Marked_sortSu(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) constraint: Marked_sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) > Marked_sortSu(circ(sortSu(t),sortSu(u))) SOLVED { 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))))) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ sortSu ] (X0) = 2*X0 + 0; [ subst ] (X0,X1) = 1*X0 + 0; [ circ ] (X0,X1) = 1 + 2*X0 + 1*X1 + 2*X1*X0 + 0; [ te ] (X0) = 2*X0 + 0; [ Marked_sortSu ] (X0) = 2 + 2*X0 + 0; [ lift ] () = 1 + 0; [ cons ] (X0,X1) = 2 + 2*X0 + 1*X1 + 0; [ Marked_te ] (X0) = 1 + 1*X0 + 0; [ sop ] (X0) = 2 + 1*X0 + 0; [ msubst ] (X0,X1) = 1 + 2*X0 + 1*X1 + 2*X1*X0 + 0; [ id ] () = 0; ]} ]} ]} Cime worked for 173.588603 seconds (real time) Cime Exit Status: 0