- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) [2] Frozen(m,Sum_constant(Left),n,s) -> Term_sub(m,s) [3] Frozen(m,Sum_constant(Right),n,s) -> Term_sub(n,s) [4] Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) [5] Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) [6] Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) [7] Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) [8] Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) [9] Term_sub(Term_var(x),Id) -> Term_var(x) [10] Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m [11] Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) [12] Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) [13] Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) [14] Sum_sub(xi,Id) -> Sum_term_var(xi) [15] Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) [16] Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) [17] Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) [18] Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) [19] Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) [20] Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) [21] Concat(Id,s) -> s Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 3 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) ; Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) ; Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi,Term_sub(n,s)) ; Sum_sub(xi,Id) >= Sum_term_var(xi) ; Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) ; Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) ; Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) ; Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) ; Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) ; Term_sub(Term_var(x),Id) >= Term_var(x) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m ; Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) ; Concat(Id,s) >= s ; Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t),Concat(s,t)) ; Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) ; Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) ; Marked_Concat(Cons_usual(x,m,s),t) >= Marked_Concat(s,t) ; Marked_Concat(Cons_usual(x,m,s),t) >= Marked_Term_sub(m,t) ; Marked_Concat(Cons_sum(xi,k,s),t) >= Marked_Concat(s,t) ; Marked_Concat(Concat(s,t),u) >= Marked_Concat(t,u) ; Marked_Concat(Concat(s,t),u) >= Marked_Concat(s,Concat(t,u)) ; Marked_Term_sub(Term_sub(m,s),t) >= Marked_Concat(s,t) ; Marked_Term_sub(Term_sub(m,s),t) >= Marked_Term_sub(m,Concat(s,t)) ; Marked_Term_sub(Case(m,xi,n),s) >= Marked_Frozen(m,Sum_sub(xi,s),n,s) ; Marked_Term_sub(Term_app(m,n),s) >= Marked_Term_sub(n,s) ; Marked_Term_sub(Term_app(m,n),s) >= Marked_Term_sub(m,s) ; Marked_Term_sub(Term_pair(m,n),s) >= Marked_Term_sub(n,s) ; Marked_Term_sub(Term_pair(m,n),s) >= Marked_Term_sub(m,s) ; Marked_Term_sub(Term_inl(m),s) >= Marked_Term_sub(m,s) ; Marked_Term_sub(Term_inr(m),s) >= Marked_Term_sub(m,s) ; Marked_Frozen(m,Sum_constant(Left),n,s) >= Marked_Term_sub(m,s) ; Marked_Frozen(m,Sum_constant(Right),n,s) >= Marked_Term_sub(n,s) ; Marked_Frozen(m,Sum_term_var(xi),n,s) >= Marked_Term_sub(n,s) ; Marked_Frozen(m,Sum_term_var(xi),n,s) >= Marked_Term_sub(m,s) ; } + Disjunctions:{ { Marked_Concat(Cons_usual(x,m,s),t) > Marked_Concat(s,t) ; } { Marked_Concat(Cons_usual(x,m,s),t) > Marked_Term_sub(m,t) ; } { Marked_Concat(Cons_sum(xi,k,s),t) > Marked_Concat(s,t) ; } { Marked_Concat(Concat(s,t),u) > Marked_Concat(t,u) ; } { Marked_Concat(Concat(s,t),u) > Marked_Concat(s,Concat(t,u)) ; } { Marked_Term_sub(Term_sub(m,s),t) > Marked_Concat(s,t) ; } { Marked_Term_sub(Term_sub(m,s),t) > Marked_Term_sub(m,Concat(s,t)) ; } { Marked_Term_sub(Case(m,xi,n),s) > Marked_Frozen(m,Sum_sub(xi,s),n,s) ; } { Marked_Term_sub(Term_app(m,n),s) > Marked_Term_sub(n,s) ; } { Marked_Term_sub(Term_app(m,n),s) > Marked_Term_sub(m,s) ; } { Marked_Term_sub(Term_pair(m,n),s) > Marked_Term_sub(n,s) ; } { Marked_Term_sub(Term_pair(m,n),s) > Marked_Term_sub(m,s) ; } { Marked_Term_sub(Term_inl(m),s) > Marked_Term_sub(m,s) ; } { Marked_Term_sub(Term_inr(m),s) > Marked_Term_sub(m,s) ; } { Marked_Frozen(m,Sum_constant(Left),n,s) > Marked_Term_sub(m,s) ; } { Marked_Frozen(m,Sum_constant(Right),n,s) > Marked_Term_sub(n,s) ; } { Marked_Frozen(m,Sum_term_var(xi),n,s) > Marked_Term_sub(n,s) ; } { Marked_Frozen(m,Sum_term_var(xi),n,s) > Marked_Term_sub(m,s) ; } } === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) constraint: Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) constraint: Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi, Term_sub(n,s)) constraint: Sum_sub(xi,Id) >= Sum_term_var(xi) constraint: Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) constraint: Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) constraint: Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) constraint: Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) constraint: Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s), Term_sub(n,s)) constraint: Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) constraint: Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) constraint: Term_sub(Term_var(x),Id) >= Term_var(x) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m constraint: Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) constraint: Concat(Id,s) >= s constraint: Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t), Concat(s,t)) constraint: Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) constraint: Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) constraint: Marked_Concat(Cons_usual(x,m,s),t) >= Marked_Concat(s,t) constraint: Marked_Concat(Cons_usual(x,m,s),t) >= Marked_Term_sub(m,t) constraint: Marked_Concat(Cons_sum(xi,k,s),t) >= Marked_Concat(s,t) constraint: Marked_Concat(Concat(s,t),u) >= Marked_Concat(t,u) constraint: Marked_Concat(Concat(s,t),u) >= Marked_Concat(s,Concat(t,u)) constraint: Marked_Term_sub(Term_sub(m,s),t) >= Marked_Concat(s,t) constraint: Marked_Term_sub(Term_sub(m,s),t) >= Marked_Term_sub(m,Concat(s,t)) constraint: Marked_Term_sub(Case(m,xi,n),s) >= Marked_Frozen(m,Sum_sub(xi,s), n,s) constraint: Marked_Term_sub(Term_app(m,n),s) >= Marked_Term_sub(n,s) constraint: Marked_Term_sub(Term_app(m,n),s) >= Marked_Term_sub(m,s) constraint: Marked_Term_sub(Term_pair(m,n),s) >= Marked_Term_sub(n,s) constraint: Marked_Term_sub(Term_pair(m,n),s) >= Marked_Term_sub(m,s) constraint: Marked_Term_sub(Term_inl(m),s) >= Marked_Term_sub(m,s) constraint: Marked_Term_sub(Term_inr(m),s) >= Marked_Term_sub(m,s) constraint: Marked_Frozen(m,Sum_constant(Left),n,s) >= Marked_Term_sub(m,s) constraint: Marked_Frozen(m,Sum_constant(Right),n,s) >= Marked_Term_sub(n,s) constraint: Marked_Frozen(m,Sum_term_var(xi),n,s) >= Marked_Term_sub(n,s) constraint: Marked_Frozen(m,Sum_term_var(xi),n,s) >= Marked_Term_sub(m,s) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) ; Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) ; Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi,Term_sub(n,s)) ; Sum_sub(xi,Id) >= Sum_term_var(xi) ; Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) ; Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) ; Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) ; Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) ; Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) ; Term_sub(Term_var(x),Id) >= Term_var(x) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m ; Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) ; Concat(Id,s) >= s ; Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t),Concat(s,t)) ; Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) ; Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) ; Marked_Sum_sub(xi,Cons_usual(y,m,s)) >= Marked_Sum_sub(xi,s) ; Marked_Sum_sub(xi,Cons_sum(psi,k,s)) >= Marked_Sum_sub(xi,s) ; } + Disjunctions:{ { Marked_Sum_sub(xi,Cons_usual(y,m,s)) > Marked_Sum_sub(xi,s) ; } { Marked_Sum_sub(xi,Cons_sum(psi,k,s)) > Marked_Sum_sub(xi,s) ; } } === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) constraint: Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) constraint: Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi, Term_sub(n,s)) constraint: Sum_sub(xi,Id) >= Sum_term_var(xi) constraint: Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) constraint: Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) constraint: Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) constraint: Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) constraint: Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s), Term_sub(n,s)) constraint: Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) constraint: Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) constraint: Term_sub(Term_var(x),Id) >= Term_var(x) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m constraint: Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) constraint: Concat(Id,s) >= s constraint: Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t), Concat(s,t)) constraint: Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) constraint: Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) constraint: Marked_Sum_sub(xi,Cons_usual(y,m,s)) >= Marked_Sum_sub(xi,s) constraint: Marked_Sum_sub(xi,Cons_sum(psi,k,s)) >= Marked_Sum_sub(xi,s) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) ; Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) ; Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi,Term_sub(n,s)) ; Sum_sub(xi,Id) >= Sum_term_var(xi) ; Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) ; Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) ; Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) ; Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) ; Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) ; Term_sub(Term_var(x),Id) >= Term_var(x) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m ; Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) ; Concat(Id,s) >= s ; Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t),Concat(s,t)) ; Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) ; Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) ; Marked_Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Marked_Term_sub(Term_var(x), s) ; Marked_Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Marked_Term_sub(Term_var(x), s) ; } + Disjunctions:{ { Marked_Term_sub(Term_var(x),Cons_usual(y,m,s)) > Marked_Term_sub(Term_var(x), s) ; } { Marked_Term_sub(Term_var(x),Cons_sum(xi,k,s)) > Marked_Term_sub(Term_var(x), s) ; } } === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) constraint: Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) constraint: Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi, Term_sub(n,s)) constraint: Sum_sub(xi,Id) >= Sum_term_var(xi) constraint: Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) constraint: Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) constraint: Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) constraint: Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) constraint: Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s), Term_sub(n,s)) constraint: Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) constraint: Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) constraint: Term_sub(Term_var(x),Id) >= Term_var(x) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m constraint: Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) constraint: Concat(Id,s) >= s constraint: Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t), Concat(s,t)) constraint: Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) constraint: Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) constraint: Marked_Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Marked_Term_sub( Term_var( x),s) constraint: Marked_Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Marked_Term_sub( Term_var( x),s) APPLY CRITERIA (Graph splitting) Found 2 components: { --> --> --> --> } { --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) ; Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) ; Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi,Term_sub(n,s)) ; Sum_sub(xi,Id) >= Sum_term_var(xi) ; Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) ; Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) ; Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) ; Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) ; Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) ; Term_sub(Term_var(x),Id) >= Term_var(x) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m ; Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) ; Concat(Id,s) >= s ; Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t),Concat(s,t)) ; Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) ; Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) ; Marked_Term_sub(Term_sub(m,s),t) >= Marked_Term_sub(m,Concat(s,t)) ; Marked_Term_sub(Term_inl(m),s) >= Marked_Term_sub(m,s) ; } + Disjunctions:{ { Marked_Term_sub(Term_sub(m,s),t) > Marked_Term_sub(m,Concat(s,t)) ; } { Marked_Term_sub(Term_inl(m),s) > Marked_Term_sub(m,s) ; } } === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) constraint: Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) constraint: Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi, Term_sub(n,s)) constraint: Sum_sub(xi,Id) >= Sum_term_var(xi) constraint: Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) constraint: Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) constraint: Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) constraint: Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) constraint: Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s), Term_sub(n,s)) constraint: Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) constraint: Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) constraint: Term_sub(Term_var(x),Id) >= Term_var(x) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m constraint: Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) constraint: Concat(Id,s) >= s constraint: Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t), Concat(s,t)) constraint: Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) constraint: Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) constraint: Marked_Term_sub(Term_sub(m,s),t) >= Marked_Term_sub(m,Concat(s,t)) constraint: Marked_Term_sub(Term_inl(m),s) >= Marked_Term_sub(m,s) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) ; Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) ; Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi,Term_sub(n,s)) ; Sum_sub(xi,Id) >= Sum_term_var(xi) ; Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) ; Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) ; Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) ; Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) ; Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) ; Term_sub(Term_var(x),Id) >= Term_var(x) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m ; Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) ; Concat(Id,s) >= s ; Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t),Concat(s,t)) ; Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) ; Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) ; Marked_Concat(Cons_sum(xi,k,s),t) >= Marked_Concat(s,t) ; Marked_Concat(Concat(s,t),u) >= Marked_Concat(t,u) ; Marked_Concat(Concat(s,t),u) >= Marked_Concat(s,Concat(t,u)) ; } + Disjunctions:{ { Marked_Concat(Cons_sum(xi,k,s),t) > Marked_Concat(s,t) ; } { Marked_Concat(Concat(s,t),u) > Marked_Concat(t,u) ; } { Marked_Concat(Concat(s,t),u) > Marked_Concat(s,Concat(t,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 === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) constraint: Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) constraint: Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi, Term_sub(n,s)) constraint: Sum_sub(xi,Id) >= Sum_term_var(xi) constraint: Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) constraint: Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) constraint: Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) constraint: Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) constraint: Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s), Term_sub(n,s)) constraint: Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) constraint: Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) constraint: Term_sub(Term_var(x),Id) >= Term_var(x) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m constraint: Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) constraint: Concat(Id,s) >= s constraint: Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t), Concat(s,t)) constraint: Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) constraint: Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) constraint: Marked_Concat(Cons_sum(xi,k,s),t) >= Marked_Concat(s,t) constraint: Marked_Concat(Concat(s,t),u) >= Marked_Concat(t,u) constraint: Marked_Concat(Concat(s,t),u) >= Marked_Concat(s,Concat(t,u)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) ; Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) ; Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi,Term_sub(n,s)) ; Sum_sub(xi,Id) >= Sum_term_var(xi) ; Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) ; Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) ; Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) ; Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) ; Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) ; Term_sub(Term_var(x),Id) >= Term_var(x) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m ; Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) ; Concat(Id,s) >= s ; Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t),Concat(s,t)) ; Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) ; Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) ; Marked_Term_sub(Term_sub(m,s),t) >= Marked_Term_sub(m,Concat(s,t)) ; } + Disjunctions:{ { Marked_Term_sub(Term_sub(m,s),t) > Marked_Term_sub(m,Concat(s,t)) ; } } === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) constraint: Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) constraint: Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi, Term_sub(n,s)) constraint: Sum_sub(xi,Id) >= Sum_term_var(xi) constraint: Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) constraint: Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) constraint: Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) constraint: Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) constraint: Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s), Term_sub(n,s)) constraint: Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) constraint: Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) constraint: Term_sub(Term_var(x),Id) >= Term_var(x) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m constraint: Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) constraint: Concat(Id,s) >= s constraint: Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t), Concat(s,t)) constraint: Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) constraint: Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) constraint: Marked_Term_sub(Term_sub(m,s),t) >= Marked_Term_sub(m,Concat(s,t)) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) ; Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) ; Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi,Term_sub(n,s)) ; Sum_sub(xi,Id) >= Sum_term_var(xi) ; Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) ; Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) ; Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) ; Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) ; Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) ; Term_sub(Term_var(x),Id) >= Term_var(x) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m ; Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) ; Concat(Id,s) >= s ; Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t),Concat(s,t)) ; Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) ; Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) ; Marked_Concat(Concat(s,t),u) >= Marked_Concat(t,u) ; Marked_Concat(Concat(s,t),u) >= Marked_Concat(s,Concat(t,u)) ; } + Disjunctions:{ { Marked_Concat(Concat(s,t),u) > Marked_Concat(t,u) ; } { Marked_Concat(Concat(s,t),u) > Marked_Concat(s,Concat(t,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 === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) constraint: Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) constraint: Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi, Term_sub(n,s)) constraint: Sum_sub(xi,Id) >= Sum_term_var(xi) constraint: Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) constraint: Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) constraint: Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) constraint: Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) constraint: Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s), Term_sub(n,s)) constraint: Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) constraint: Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) constraint: Term_sub(Term_var(x),Id) >= Term_var(x) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m constraint: Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) constraint: Concat(Id,s) >= s constraint: Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t), Concat(s,t)) constraint: Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) constraint: Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) constraint: Marked_Concat(Concat(s,t),u) >= Marked_Concat(t,u) constraint: Marked_Concat(Concat(s,t),u) >= Marked_Concat(s,Concat(t,u)) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) ; Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) ; Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi,Term_sub(n,s)) ; Sum_sub(xi,Id) >= Sum_term_var(xi) ; Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) ; Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) ; Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) ; Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) ; Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) ; Term_sub(Term_var(x),Id) >= Term_var(x) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m ; Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) ; Concat(Id,s) >= s ; Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t),Concat(s,t)) ; Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) ; Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) ; Marked_Sum_sub(xi,Cons_usual(y,m,s)) >= Marked_Sum_sub(xi,s) ; } + Disjunctions:{ { Marked_Sum_sub(xi,Cons_usual(y,m,s)) > Marked_Sum_sub(xi,s) ; } } === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) constraint: Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) constraint: Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi, Term_sub(n,s)) constraint: Sum_sub(xi,Id) >= Sum_term_var(xi) constraint: Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) constraint: Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) constraint: Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) constraint: Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) constraint: Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s), Term_sub(n,s)) constraint: Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) constraint: Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) constraint: Term_sub(Term_var(x),Id) >= Term_var(x) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m constraint: Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) constraint: Concat(Id,s) >= s constraint: Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t), Concat(s,t)) constraint: Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) constraint: Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) constraint: Marked_Sum_sub(xi,Cons_usual(y,m,s)) >= Marked_Sum_sub(xi,s) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) ; Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) ; Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi,Term_sub(n,s)) ; Sum_sub(xi,Id) >= Sum_term_var(xi) ; Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) ; Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) ; Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) ; Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) ; Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s),Term_sub(n,s)) ; Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) ; Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) ; Term_sub(Term_var(x),Id) >= Term_var(x) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) ; Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m ; Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) ; Concat(Id,s) >= s ; Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t),Concat(s,t)) ; Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) ; Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) ; Marked_Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Marked_Term_sub(Term_var(x), s) ; } + Disjunctions:{ { Marked_Term_sub(Term_var(x),Cons_usual(y,m,s)) > Marked_Term_sub(Term_var(x), s) ; } } === 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: Frozen(m,Sum_constant(Left),n,s) >= Term_sub(m,s) constraint: Frozen(m,Sum_constant(Right),n,s) >= Term_sub(n,s) constraint: Frozen(m,Sum_term_var(xi),n,s) >= Case(Term_sub(m,s),xi, Term_sub(n,s)) constraint: Sum_sub(xi,Id) >= Sum_term_var(xi) constraint: Sum_sub(xi,Cons_usual(y,m,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_sub(xi,s) constraint: Sum_sub(xi,Cons_sum(psi,k,s)) >= Sum_constant(k) constraint: Term_sub(Term_sub(m,s),t) >= Term_sub(m,Concat(s,t)) constraint: Term_sub(Case(m,xi,n),s) >= Frozen(m,Sum_sub(xi,s),n,s) constraint: Term_sub(Term_app(m,n),s) >= Term_app(Term_sub(m,s),Term_sub(n,s)) constraint: Term_sub(Term_pair(m,n),s) >= Term_pair(Term_sub(m,s), Term_sub(n,s)) constraint: Term_sub(Term_inl(m),s) >= Term_inl(Term_sub(m,s)) constraint: Term_sub(Term_inr(m),s) >= Term_inr(Term_sub(m,s)) constraint: Term_sub(Term_var(x),Id) >= Term_var(x) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Term_sub(Term_var(x),s) constraint: Term_sub(Term_var(x),Cons_usual(y,m,s)) >= m constraint: Term_sub(Term_var(x),Cons_sum(xi,k,s)) >= Term_sub(Term_var(x),s) constraint: Concat(Id,s) >= s constraint: Concat(Cons_usual(x,m,s),t) >= Cons_usual(x,Term_sub(m,t), Concat(s,t)) constraint: Concat(Cons_sum(xi,k,s),t) >= Cons_sum(xi,k,Concat(s,t)) constraint: Concat(Concat(s,t),u) >= Concat(s,Concat(t,u)) constraint: Marked_Term_sub(Term_var(x),Cons_usual(y,m,s)) >= Marked_Term_sub( Term_var( x),s) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) [2] Frozen(m,Sum_constant(Left),n,s) -> Term_sub(m,s) [3] Frozen(m,Sum_constant(Right),n,s) -> Term_sub(n,s) [4] Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) [5] Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) [6] Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) [7] Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) [8] Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) [9] Term_sub(Term_var(x),Id) -> Term_var(x) [10] Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m [11] Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) [12] Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) [13] Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) [14] Sum_sub(xi,Id) -> Sum_term_var(xi) [15] Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) [16] Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) [17] Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) [18] Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) [19] Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) [20] Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) [21] Concat(Id,s) -> s , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ Frozen ] (X0,X1,X2,X3) = 2*X3*X2 + 2*X3*X0 + 2*X3 + 1*X2 + 1*X0 + 2; [ Concat ] (X0,X1) = 2*X1*X0 + 1*X1 + 1*X0; [ Term_app ] (X0,X1) = 2*X1 + 1*X0 + 2; [ Sum_constant ] (X0) = 0; [ Marked_Frozen ] (X0,X1,X2,X3) = 2*X2 + 2*X0; [ Term_var ] (X0) = 0; [ Term_sub ] (X0,X1) = 2*X1*X0 + 1*X1 + 1*X0; [ Marked_Term_sub ] (X0,X1) = 2*X0; [ Term_inl ] (X0) = 1*X0; [ Right ] () = 0; [ Cons_usual ] (X0,X1,X2) = 1*X2 + 2*X1 + 1; [ Sum_sub ] (X0,X1) = 0; [ Marked_Concat ] (X0,X1) = 1*X0; [ Term_pair ] (X0,X1) = 2*X1 + 1*X0 + 2; [ Left ] () = 0; [ Id ] () = 0; [ Case ] (X0,X1,X2) = 1*X2 + 1*X0 + 2; [ Term_inr ] (X0) = 1*X0 + 1; [ Sum_term_var ] (X0) = 0; [ Cons_sum ] (X0,X1,X2) = 1*X2; removing < Marked_Term_sub(Term_app(m,n),s),Marked_Term_sub(m,s)>< Marked_Term_sub(Term_pair(m,n),s),Marked_Term_sub(m,s)>< Marked_Term_sub(Term_inr(m),s),Marked_Term_sub(m,s)>< Marked_Concat(Cons_usual(x,m,s),t),Marked_Concat(s,t)> [ { DP termination of: