NTI: Non-Termination Analysis for Term Rewriting and Logic Programming — Reproducibility Capsule

Abstract

NTI (Non-Termination Inference) is an open-source Java tool for proving termination and non-termination of term rewrite systems and logic programs. This reproducibility capsule accompanies the manuscript “NTI: Non-Termination Analysis for Term Rewriting and Logic Programming”. The capsule archives NTI version 2026.09, exactly as published at GitHub commit 88a47f9db976fc7c1ad1921057f0a68d68748137. It includes the complete source code, an executable JAR, compilation and usage documentation, license notices, and the corresponding sources of the bundled SAT4J Core 2.3.6 dependency. No additional source patch is required. Nine examples support reproduction of the manuscript: three illustrative examples and six instances from its Impact table. Their input files, expected verdicts, reference outputs and provenance are included. A Python runner executes the examples with time limits and records the results. The REPRODUCING.md file explains the workflow, and SHA-256 checksums allow file integrity verification. An optional Dockerfile builds the software from source with Java 21. All 888 tests passed with the standard Maven configuration, both on macOS arm64 with Java 24 and on Docker Linux arm64 with Temurin Java 21.0.12. All nine example verdicts were reproduced in both environments; the Docker example runs required no network access. No tests were skipped. Build and execution reports are included. Java 21 or later is required to run the supplied JAR. Docker and Python are optional conveniences; no prebuilt Docker image is included. The capsule reproduces the selected manuscript examples, but does not rerun all historical competition experiments or establish the full historical regression coverage.