YES LCTRS Theories Core, Ints Signature f2: Int -> Int u_27: (Int, Int) -> Int Rules u_27(!n, !w_6) -> +(+(!n, -(!n, 1)), !w_6) f2(!n) -> u_27(!n, f2(-(!n, 2))) [>(!n, 1)] f2(!n) -> !n [<=(!n, 1)] * DPGraph approximation on the DP problem dependency pairs: {f2#(!n) -> u_27#(!n, f2(-(!n, 2))) [>(!n, 1)] , f2#(!n) -> f2#(-(!n, 2)) [>(!n, 1)]} rules: {u_27(!n, !w_6) -> +(+(!n, -(!n, 1)), !w_6) , f2(!n) -> u_27(!n, f2(-(!n, 2))) [>(!n, 1)] , f2(!n) -> !n [<=(!n, 1)]} resulting in the DP graph DPGraph with indexed dependency pairs {1: f2#(!n) -> u_27#(!n, f2(-(!n, 2))) [>(!n, 1)] , 2: f2#(!n) -> f2#(-(!n, 2)) [>(!n, 1)]} and edges 1 -> {} 2 -> {1, 2} with 1 SCC(s) SCC: {f2#(!n) -> f2#(-(!n, 2)) [>(!n, 1)]} * Value criterion after 1 iteration(s) with the projections: Iteration 1: projection(s): v(f2#) = 1 removing the rule(s): {f2#(!n) -> f2#(-(!n, 2)) [>(!n, 1)]} Elapsed Time: 24.56 ms