The extension of classical imperative programs with real-valued random\nvariables and random branching gives rise to probabilistic programs. The\ntermination problem is one of the most fundamental liveness properties for such\nprograms. The qualitative (aka almost-sure) termination problem asks whether a\ngiven program terminates with probability 1. Ranking functions provide a sound\nand complete approach for termination of non-probabilistic programs, and their\nextension to probabilistic programs is achieved via ranking supermartingales\n(RSMs). RSMs have been extended to lexicographic RSMs to handle programs with\ninvolved control-flow structure, as well as for compositional approach. There\nare two key limitations of the existing RSM-based approaches: First, the\nlexicographic RSM-based approach requires a strong nonnegativity assumption,\nwhich need not always be satisfied. The second key limitation of the existing\nRSM-based algorithmic approaches is that they rely on pre-computed invariants.\nThe main drawback of relying on pre-computed invariants is the\ninsufficiency-inefficiency trade-off: weak invariants might be insufficient for\nRSMs to prove termination, while using strong invariants leads to inefficiency\nin computing them. Our contributions are twofold: First, we show how to relax\nthe strong nonnegativity condition and still provide soundness guarantee for\nalmost-sure termination. Second, we present an incremental approach where the\nprocess of computing lexicographic RSMs proceeds by iterative pruning of parts\nof the program that were already shown to be terminating, in cooperation with a\nsafety prover. In particular, our technique does not rely on strong\npre-computed invariants. We present experimental results to show the\napplicability of our approach to examples of probabilistic programs from the\nliterature.\n