- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] and(false,false) -> false [2] and(true,false) -> false [3] and(false,true) -> false [4] and(true,true) -> true [5] eq(nil,nil) -> true [6] eq(cons(T,L),nil) -> false [7] eq(nil,cons(T,L)) -> false [8] eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) [9] eq(var(L),var(Lp)) -> eq(L,Lp) [10] eq(var(L),apply(T,S)) -> false [11] eq(var(L),lambda(X,T)) -> false [12] eq(apply(T,S),var(L)) -> false [13] eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) [14] eq(apply(T,S),lambda(X,Tp)) -> false [15] eq(lambda(X,T),var(L)) -> false [16] eq(lambda(X,T),apply(Tp,Sp)) -> false [17] eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) [18] if(true,var(K),var(L)) -> var(K) [19] if(false,var(K),var(L)) -> var(L) [20] ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) [21] ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) [22] ren(X,Y,lambda(Z,T)) -> lambda(var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T))) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 2 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { and(false,false) >= false ; and(false,true) >= false ; and(true,false) >= false ; and(true,true) >= true ; eq(nil,nil) >= true ; eq(nil,cons(T,L)) >= false ; eq(cons(T,L),nil) >= false ; eq(cons(T,L),cons(Tp,Lp)) >= and(eq(T,Tp),eq(L,Lp)) ; eq(var(L),var(Lp)) >= eq(L,Lp) ; eq(var(L),apply(T,S)) >= false ; eq(var(L),lambda(X,T)) >= false ; eq(apply(T,S),var(L)) >= false ; eq(apply(T,S),apply(Tp,Sp)) >= and(eq(T,Tp),eq(S,Sp)) ; eq(apply(T,S),lambda(X,Tp)) >= false ; eq(lambda(X,T),var(L)) >= false ; eq(lambda(X,T),apply(Tp,Sp)) >= false ; eq(lambda(X,T),lambda(Xp,Tp)) >= and(eq(T,Tp),eq(X,Xp)) ; if(false,var(K),var(L)) >= var(L) ; if(true,var(K),var(L)) >= var(K) ; ren(var(L),var(K),var(Lp)) >= if(eq(L,Lp),var(K),var(Lp)) ; ren(X,Y,apply(T,S)) >= apply(ren(X,Y,T),ren(X,Y,S)) ; ren(X,Y,lambda(Z,T)) >= lambda(var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), ren(X,Y, ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T))) ; Marked_ren(X,Y,apply(T,S)) >= Marked_ren(X,Y,T) ; Marked_ren(X,Y,apply(T,S)) >= Marked_ren(X,Y,S) ; Marked_ren(X,Y,lambda(Z,T)) >= Marked_ren(X,Y, ren(Z, var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), T)) ; Marked_ren(X,Y,lambda(Z,T)) >= Marked_ren(Z, var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), T) ; } + Disjunctions:{ { Marked_ren(X,Y,apply(T,S)) > Marked_ren(X,Y,T) ; } { Marked_ren(X,Y,apply(T,S)) > Marked_ren(X,Y,S) ; } { Marked_ren(X,Y,lambda(Z,T)) > Marked_ren(X,Y, ren(Z, var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), T)) ; } { Marked_ren(X,Y,lambda(Z,T)) > Marked_ren(Z, var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: and(false,false) >= false constraint: and(false,true) >= false constraint: and(true,false) >= false constraint: and(true,true) >= true constraint: eq(nil,nil) >= true constraint: eq(nil,cons(T,L)) >= false constraint: eq(cons(T,L),nil) >= false constraint: eq(cons(T,L),cons(Tp,Lp)) >= and(eq(T,Tp),eq(L,Lp)) constraint: eq(var(L),var(Lp)) >= eq(L,Lp) constraint: eq(var(L),apply(T,S)) >= false constraint: eq(var(L),lambda(X,T)) >= false constraint: eq(apply(T,S),var(L)) >= false constraint: eq(apply(T,S),apply(Tp,Sp)) >= and(eq(T,Tp),eq(S,Sp)) constraint: eq(apply(T,S),lambda(X,Tp)) >= false constraint: eq(lambda(X,T),var(L)) >= false constraint: eq(lambda(X,T),apply(Tp,Sp)) >= false constraint: eq(lambda(X,T),lambda(Xp,Tp)) >= and(eq(T,Tp),eq(X,Xp)) constraint: if(false,var(K),var(L)) >= var(L) constraint: if(true,var(K),var(L)) >= var(K) constraint: ren(var(L),var(K),var(Lp)) >= if(eq(L,Lp),var(K),var(Lp)) constraint: ren(X,Y,apply(T,S)) >= apply(ren(X,Y,T),ren(X,Y,S)) constraint: ren(X,Y,lambda(Z,T)) >= lambda(var(cons(X, cons(Y,cons(lambda(Z,T),nil)))), ren(X,Y, ren(Z, var(cons(X, cons(Y,cons(lambda(Z,T),nil)))), T))) constraint: Marked_ren(X,Y,apply(T,S)) >= Marked_ren(X,Y,T) constraint: Marked_ren(X,Y,apply(T,S)) >= Marked_ren(X,Y,S) constraint: Marked_ren(X,Y,lambda(Z,T)) >= Marked_ren(X,Y, ren(Z, var(cons(X, cons(Y,cons(lambda(Z,T),nil)))) ,T)) constraint: Marked_ren(X,Y,lambda(Z,T)) >= Marked_ren(Z, var(cons(X, cons(Y,cons(lambda(Z,T),nil)))), T) APPLY CRITERIA (Subterm criterion) ST: Marked_eq -> 2 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { and(false,false) >= false ; and(false,true) >= false ; and(true,false) >= false ; and(true,true) >= true ; eq(nil,nil) >= true ; eq(nil,cons(T,L)) >= false ; eq(cons(T,L),nil) >= false ; eq(cons(T,L),cons(Tp,Lp)) >= and(eq(T,Tp),eq(L,Lp)) ; eq(var(L),var(Lp)) >= eq(L,Lp) ; eq(var(L),apply(T,S)) >= false ; eq(var(L),lambda(X,T)) >= false ; eq(apply(T,S),var(L)) >= false ; eq(apply(T,S),apply(Tp,Sp)) >= and(eq(T,Tp),eq(S,Sp)) ; eq(apply(T,S),lambda(X,Tp)) >= false ; eq(lambda(X,T),var(L)) >= false ; eq(lambda(X,T),apply(Tp,Sp)) >= false ; eq(lambda(X,T),lambda(Xp,Tp)) >= and(eq(T,Tp),eq(X,Xp)) ; if(false,var(K),var(L)) >= var(L) ; if(true,var(K),var(L)) >= var(K) ; ren(var(L),var(K),var(Lp)) >= if(eq(L,Lp),var(K),var(Lp)) ; ren(X,Y,apply(T,S)) >= apply(ren(X,Y,T),ren(X,Y,S)) ; ren(X,Y,lambda(Z,T)) >= lambda(var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), ren(X,Y, ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T))) ; Marked_ren(X,Y,lambda(Z,T)) >= Marked_ren(X,Y, ren(Z, var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), T)) ; Marked_ren(X,Y,lambda(Z,T)) >= Marked_ren(Z, var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), T) ; } + Disjunctions:{ { Marked_ren(X,Y,lambda(Z,T)) > Marked_ren(X,Y, ren(Z, var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), T)) ; } { Marked_ren(X,Y,lambda(Z,T)) > Marked_ren(Z, var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), 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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: and(false,false) >= false constraint: and(false,true) >= false constraint: and(true,false) >= false constraint: and(true,true) >= true constraint: eq(nil,nil) >= true constraint: eq(nil,cons(T,L)) >= false constraint: eq(cons(T,L),nil) >= false constraint: eq(cons(T,L),cons(Tp,Lp)) >= and(eq(T,Tp),eq(L,Lp)) constraint: eq(var(L),var(Lp)) >= eq(L,Lp) constraint: eq(var(L),apply(T,S)) >= false constraint: eq(var(L),lambda(X,T)) >= false constraint: eq(apply(T,S),var(L)) >= false constraint: eq(apply(T,S),apply(Tp,Sp)) >= and(eq(T,Tp),eq(S,Sp)) constraint: eq(apply(T,S),lambda(X,Tp)) >= false constraint: eq(lambda(X,T),var(L)) >= false constraint: eq(lambda(X,T),apply(Tp,Sp)) >= false constraint: eq(lambda(X,T),lambda(Xp,Tp)) >= and(eq(T,Tp),eq(X,Xp)) constraint: if(false,var(K),var(L)) >= var(L) constraint: if(true,var(K),var(L)) >= var(K) constraint: ren(var(L),var(K),var(Lp)) >= if(eq(L,Lp),var(K),var(Lp)) constraint: ren(X,Y,apply(T,S)) >= apply(ren(X,Y,T),ren(X,Y,S)) constraint: ren(X,Y,lambda(Z,T)) >= lambda(var(cons(X, cons(Y,cons(lambda(Z,T),nil)))), ren(X,Y, ren(Z, var(cons(X, cons(Y,cons(lambda(Z,T),nil)))), T))) constraint: Marked_ren(X,Y,lambda(Z,T)) >= Marked_ren(X,Y, ren(Z, var(cons(X, cons(Y,cons(lambda(Z,T),nil)))) ,T)) constraint: Marked_ren(X,Y,lambda(Z,T)) >= Marked_ren(Z, var(cons(X, cons(Y,cons(lambda(Z,T),nil)))), T) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] and(false,false) -> false [2] and(true,false) -> false [3] and(false,true) -> false [4] and(true,true) -> true [5] eq(nil,nil) -> true [6] eq(cons(T,L),nil) -> false [7] eq(nil,cons(T,L)) -> false [8] eq(cons(T,L),cons(Tp,Lp)) -> and(eq(T,Tp),eq(L,Lp)) [9] eq(var(L),var(Lp)) -> eq(L,Lp) [10] eq(var(L),apply(T,S)) -> false [11] eq(var(L),lambda(X,T)) -> false [12] eq(apply(T,S),var(L)) -> false [13] eq(apply(T,S),apply(Tp,Sp)) -> and(eq(T,Tp),eq(S,Sp)) [14] eq(apply(T,S),lambda(X,Tp)) -> false [15] eq(lambda(X,T),var(L)) -> false [16] eq(lambda(X,T),apply(Tp,Sp)) -> false [17] eq(lambda(X,T),lambda(Xp,Tp)) -> and(eq(T,Tp),eq(X,Xp)) [18] if(true,var(K),var(L)) -> var(K) [19] if(false,var(K),var(L)) -> var(L) [20] ren(var(L),var(K),var(Lp)) -> if(eq(L,Lp),var(K),var(Lp)) [21] ren(X,Y,apply(T,S)) -> apply(ren(X,Y,T),ren(X,Y,S)) [22] ren(X,Y,lambda(Z,T)) -> lambda(var(cons(X,cons(Y,cons(lambda(Z,T),nil)))), ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T))) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: CG using polynomial interpretation = [ false ] () = 0; [ lambda ] (X0,X1) = 2*X1; [ nil ] () = 0; [ true ] () = 0; [ ren ] (X0,X1,X2) = 1*X2; [ var ] (X0) = 0; [ and ] (X0,X1) = 0; [ if ] (X0,X1,X2) = 0; [ cons ] (X0,X1) = 0; [ eq ] (X0,X1) = 0; [ Marked_ren ] (X0,X1,X2) = 1*X2; [ apply ] (X0,X1) = 2*X1 + 2*X0 + 2; removing [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ false ] () = 0; [ lambda ] (X0,X1) = 2 + 1*X1 + 0; [ nil ] () = 0; [ true ] () = 0; [ ren ] (X0,X1,X2) = 1*X2 + 0; [ var ] (X0) = 0; [ and ] (X0,X1) = 0; [ if ] (X0,X1,X2) = 0; [ cons ] (X0,X1) = 0; [ eq ] (X0,X1) = 0; [ Marked_ren ] (X0,X1,X2) = 2*X2 + 0; [ apply ] (X0,X1) = 0; ]} ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 1.185399 seconds (real time) Cime Exit Status: 0