Experiments for GWPO (Section 4.5)
| termination tool | Mint version 0.4 with SMT solver Z3 version 4.13.0 |
|---|---|
| problem set | term rewrite systems (TRS_Standard) from the Termination Problem Database version 11.6 with secret problems for TermCOMP 2026 |
| environment | a PC with 11th Gen Intel i7-11850H (16) @ 4.800GHz and 16 GiB memory; Ubuntu 24.04 |
| timeout | 60 seconds timeout for each problem |
| WL | a weighted path order (⩾W, >W) induced by a linear polynomial interpretation and a precedence | WPO(L) |
|---|---|---|
| WM | a weighted path order (⩾W, >W) induced by a max/plus interpretation and a precedence | WPO(M) |
| GLL | a generalized weighted path order (⩾MG, >G) induced by two linear polynomial interpretations | GWPO(L, L#) |
| GLM | a generalized weighted path order (⩾MG, >G) induced by a linear polynomial interpretation, and a max/plus interpretation | GWPO(L, M#) |
| GML | a generalized weighted path order (⩾MG, >G) induced by a max/plus interpretation, and a linear polynomial interpretation | GWPO(M, L#) |
| GMM | a generalized weighted path order (⩾MG, >G) induced by two max/plus interpretations | GWPO(M, M#) |
| SLL | a semantic path order (⩾MS, >S) induced by two linear polynomial interpretations | SPO(L#×L#) |
| SLM | a semantic path order (⩾MS, >S) induced by a linear polynomial interpretation, and a max/plus interpretation | SPO(L#×M#) |
| SML | a semantic path order (⩾MS, >S) induced by a max/plus interpretation, and a linear polynomial interpretation | SPO(M#×L#) |
| SMM | a semantic path order (⩾MS, >S) induced by two max/plus interpretations | SPO(M#×M#) |
| SF | semantic path order (⩾MS, >S) induced by a finite model over {0, 1} | SPO(F#2) | NaTT | TermCOMP 2026 version of NaTT |
| AProVE | TermCOMP 2026 version of AProVE |
| YES | proved termination |
|---|---|
| NO | proved non-termination |
| MAYBE | failed to prove |
| TIMEOUT | exceeded time limit 60 seconds |
| ERROR | terminated with some error |
Note
- The form of linear polynomials is fA(x1, ..., xn) = c0 + c1 x1 + ... + cn xn where c1, ..., cn are either 1 or 0.
- The form of max/plus algebras is fA(x1, ..., xn) = max { d0, d1 + c1 x1, ..., dn + cn xn } where c1, ..., cn are either 1 or 0.
- The experiment runs NaTT and AProVE via Apptainer using Docker images. See also Termination Portal for details.
| status | WL | WM | GLL | GLM | GML | GMM | SLL | SLM | SML | SMM | SF | NaTT | AProVE | total |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| YES | 578 | 616 | 607 | 704 | 703 | 639 | 595 | 700 | 700 | 640 | 246 | 888 | 1036 | 1084 |
| (sec) | 850.64 | 858.12 | 538.45 | 1469.73 | 1047.41 | 1227.67 | 633.48 | 1333.25 | 1696.07 | 1491.55 | 211.75 | 1296.42 | 2270.95 | |
| NO | 60 | 60 | 60 | 60 | 60 | 60 | 60 | 60 | 60 | 60 | 60 | 169 | 276 | 277 |
| (sec) | 0.19 | 0.19 | 0.20 | 0.21 | 0.52 | 0.18 | 0.51 | 0.18 | 0.18 | 0.19 | 0.52 | 166.36 | 1280.14 | |
| MAYBE | 882 | 811 | 855 | 733 | 740 | 782 | 865 | 726 | 722 | 763 | 1206 | 444 | 0 | 1242 |
| (sec) | 821.76 | 1895.54 | 871.66 | 1812.83 | 1474.04 | 2745.10 | 1092.49 | 1929.42 | 2470.74 | 3793.43 | 1935.46 | 1554.74 | 0.00 | |
| TIMEOUT | 22 | 55 | 20 | 45 | 39 | 61 | 22 | 56 | 60 | 79 | 19 | 40 | 230 | 271 |
| (sec) | 1320.00 | 3300.00 | 1200.00 | 2700.00 | 2340.00 | 3660.00 | 1320.00 | 3360.00 | 3600.00 | 4740.00 | 1140.00 | 2400.00 | 13800.00 | |
| ERROR | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 11 | 1 | 0 | 12 |
| (sec) | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 309.36 | 56.92 | 0.00 | |
| total | 1542 | 1542 | 1542 | 1542 | 1542 | 1542 | 1542 | 1542 | 1542 | 1542 | 1542 | 1542 | 1542 |