The polynomial path order is a termination method that induces polynomial bounds on the innermost runtime complexity of term rewrite systems. Semantic labeling is a transformation technique used for proving termination.

In this paper, we propose an efficient implementation of polynomial path orders together with finite semantic labeling. This automation works by a reduction to the problem of boolean satisfiability. We have implemented the technique and experimental results confirm the feasibility of our approach. By semantic labeling the analytical power of polynomial path orders is significantly increased.