Experiments for ``An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting''

General Information
non-reachability tool	prototype infeasibility tool inf-tool with SMT solver Z3 version 4.8.12.
certifier	CeTA version 3.2
problem set	infeasibility problems used in the inefasibility of the CoCo 2024 full-run
environment	a PC with 11th Gen Intel i7-11850H (16) @ 4.800GHz and 16 GiB memory; Ubuntu 23.10
timeout	60 seconds timeout for each problem

Abbreviations
poly-nat(+CeTA)	co-rewrite pair induced by linear polynomials on natural numbers	inf-tool -o poly-nat -f file.ari (-c)
poly-negint(+CeTA)	co-rewrite pair induced by linear polynomials on integers below 0	inf-tool -o poly-negint -f file.ari (-c)
wpol(+CeTA)	weighted path orders induced by linear polynomials on natural numbers	inf-tool -o wpol -f file.ari (-c)
NaTT	NaTT, the version which participated in CoCo 2024 INF
nonreach(+CeTA)	nonreach version 1.2 (+ CeTA)	nonreach (--output-simple Certificate) -f file.ari
Moca(+CeTA)	Moca version 0.3 (+ CeTA)
infChecker	infChecker version 2024
CO3	CO3 version 2.5

Meanings of Statuses
Y: YES	proved/certified infeasibility
N: NO	proved/certified non-infeasibility
M: MAYBE	failed to prove/certify
T: TIMEOUT	exceeded time limit 60 seconds
E: ERROR	tool terminated with some error

Note

The form of linear polynomials used by the prototype tool is f_A(x₁, ..., x_n) = f₀ + f₁ x₁ + ... + f_n x_n where f₁, ..., f_n are either 1 or 0.
The data for NaTT, Moca(+CeTA), infChecker and CO3 is migrated from the CoCo 2024 full-run. Others are generated on an author's PC.
The tool nonreach only accepts the old CoCo format and generates certificates in CPF-2, so the conversion tools are used for the experiment.
The prototype tool gave the first certified proofs to the following 8 problems:
- 721 (poly-nat, poly-negint, wpol)
- 748 (poly-negint)
- 769 (poly-negint)
- 979 (poly-nat, poly-negint, wpol)
- 1127 (wpol)
- 1129 (wpol)
- 1130 (wpol)
- 1613 (poly-nat, wpol)

Summary
status	poly-nat	poly-nat+CeTA	poly-negint	poly-negint+CeTA	wpol	wpol+CeTA	NaTT	nonreach	nonreach+CeTA	Moca	Moca+CeTA	infChecker	CO3	total
YES	21	21	24	24	22	22	43	43	31	49	32	63	30	78
(sec)	0.38	0.81	0.44	0.94	0.60	1.00	18.28	2.94	3.35	124.32	66.76	1194.08	0.34
NO	0	0	0	0	0	0	0	17	0	0	0	43	0	43
(sec)	0.00	0.00	0.00	0.00	0.00	0.00	0.00	1.20	0.00	0.00	0.00	6.61	0.00
MAYBE	125	125	122	122	124	124	27	86	103	66	70	0	116	134
(sec)	2.07	2.42	2.14	2.50	7.24	8.29	322.19	5.95	7.61	301.11	360.58	0.00	1.30
TIMEOUT	0	0	0	0	0	0	76	0	0	31	44	40	0	97
(sec)	0.00	0.00	0.00	0.00	0.00	0.00	4560.00	0.00	0.00	1860.00	2640.00	2400.00	0.00
ERROR	0	0	0	0	0	0	0	0	12	0	0	0	0	12
(sec)	0.00	0.00	0.00	0.00	0.00	0.00	0.00	0.00	1.35	0.00	0.00	0.00	0.00
total	146	146	146	146	146	146	146	146	146	146	146	146	146

Individual results
file	poly-nat	poly-nat+CeTA	poly-negint	poly-negint+CeTA	wpol	wpol+CeTA	NaTT	nonreach	nonreach+CeTA	Moca	Moca+CeTA	infChecker	CO3
664	0.02	0.02	0.02	0.03	0.04	0.04	60.00	0.06	0.07	60.00	60.00	60.00	0.01
665	0.02	0.03	0.02	0.02	0.07	0.08	60.00	0.07	0.05	3.38	60.00	60.00	0.01
666	0.02	0.02	0.02	0.02	0.21	0.22	60.00	0.08	0.05	4.76	6.22	0.13	0.01
667	0.02	0.02	0.02	0.02	0.22	0.29	60.00	0.07	0.08	4.50	17.00	0.11	0.02
668	0.02	0.02	0.02	0.02	0.21	0.22	60.00	0.07	0.09	4.53	17.14	0.13	0.02
669	0.02	0.02	0.02	0.03	0.21	0.22	60.00	0.06	0.07	15.93	17.10	0.64	0.02
670	0.02	0.02	0.02	0.02	0.22	0.26	60.00	0.07	0.06	15.80	17.28	0.64	0.02
671	0.02	0.02	0.02	0.02	0.21	0.25	60.00	0.06	0.07	15.45	17.35	0.65	0.02
672	0.02	0.02	0.02	0.03	0.22	0.33	60.00	0.09	0.06	5.08	17.33	0.63	0.02
673	0.02	0.02	0.02	0.02	0.21	0.27	60.00	0.08	0.07	15.78	17.28	0.68	0.02
674	0.02	0.02	0.02	0.03	0.22	0.25	60.00	0.05	0.08	5.27	17.26	0.65	0.02
675	0.02	0.02	0.02	0.02	0.21	0.25	60.00	0.07	0.08	16.51	18.50	60.00	0.02
676	0.02	0.02	0.02	0.02	0.21	0.25	60.00	0.06	0.08	16.37	17.88	60.00	0.02
677	0.02	0.02	0.02	0.02	0.22	0.26	60.00	0.06	0.06	16.36	19.18	60.00	0.02
678	0.02	0.02	0.02	0.02	0.22	0.25	60.00	0.09	0.10	17.61	48.23	60.00	0.02
679	0.02	0.02	0.02	0.02	0.22	0.27	60.00	0.06	0.08	17.68	18.72	60.00	0.02
680	0.02	0.02	0.02	0.02	0.22	0.23	60.00	0.07	0.08	16.88	19.16	60.00	0.01
681	0.02	0.02	0.02	0.02	0.21	0.25	60.00	0.06	0.06	18.08	18.50	0.43	0.02
682	0.02	0.02	0.02	0.03	0.21	0.26	60.00	0.08	0.05	32.67	60.00	60.00	0.02
683	0.02	0.02	0.02	0.03	0.22	0.26	60.00	0.08	0.07	18.69	60.00	60.00	0.01
684	0.02	0.02	0.02	0.03	0.22	0.25	60.00	0.06	0.06	60.00	60.00	60.00	0.02
685	0.02	0.02	0.02	0.02	0.21	0.22	60.00	0.08	0.07	33.40	60.00	60.00	0.02
686	0.02	0.03	0.02	0.02	0.22	0.23	60.00	0.06	0.06	48.33	60.00	60.00	0.02
687	0.01	0.02	0.01	0.03	0.01	0.02	0.34	0.08	0.11	0.13	0.13	20.31	0.01
688	0.02	0.04	0.02	0.04	0.02	0.05	0.42	0.06	0.07	60.00	60.00	20.15	0.01
689	0.02	0.05	0.02	0.05	0.02	0.06	0.42	0.07	0.08	60.00	60.00	20.22	0.01
690	0.02	0.03	0.02	0.03	0.02	0.04	60.00	0.08	0.06	60.00	60.00	60.00	0.01
691	0.02	0.02	0.01	0.02	0.02	0.03	60.00	0.07	0.06	60.00	60.00	60.00	0.01
692	0.02	0.02	0.01	0.02	0.02	0.03	60.00	0.08	0.07	0.36	0.40	0.06	0.01
693	0.02	0.03	0.02	0.03	0.03	0.05	0.41	0.06	0.11	0.27	60.00	20.16	0.01
694	0.02	0.04	0.02	0.05	0.03	0.05	0.37	0.05	0.12	0.31	60.00	20.16	0.01
695	0.02	0.04	0.02	0.05	0.03	0.05	0.38	0.06	0.10	2.16	60.00	20.22	0.01
696	0.02	0.05	0.02	0.05	0.03	0.05	0.39	0.08	0.10	2.38	60.00	20.23	0.01
697	0.02	0.03	0.02	0.03	0.02	0.04	60.00	0.08	0.07	0.45	0.37	0.05	0.01
698	0.02	0.02	0.02	0.02	0.03	0.02	56.29	0.06	0.06	0.23	0.24	0.05	0.01
699	0.02	0.02	0.02	0.02	0.02	0.03	55.14	0.08	0.09	0.34	0.45	0.06	0.01
700	0.02	0.02	0.02	0.02	0.03	0.02	60.00	0.06	0.08	0.42	5.72	0.05	0.01
701	0.02	0.02	0.02	0.02	0.03	0.03	60.00	0.08	0.08	0.19	0.26	0.06	0.01
702	0.02	0.02	0.02	0.02	0.02	0.03	60.00	0.06	0.07	0.39	0.44	0.06	0.01
703	0.02	0.02	0.02	0.02	0.03	0.03	60.00	0.05	0.06	0.34	5.63	0.06	0.01
704	0.02	0.02	0.02	0.02	0.04	0.04	60.00	0.07	0.07	2.11	60.00	60.00	0.01
705	0.02	0.02	0.02	0.02	0.02	0.03	60.00	0.07	0.07	60.00	60.00	20.16	0.01
706	0.02	0.02	0.02	0.02	0.02	0.02	60.00	0.07	0.07	60.00	60.00	20.14	0.01
707	0.01	0.04	0.02	0.03	0.03	0.05	0.32	0.09	0.10	0.18	60.00	20.08	0.01
708	0.02	0.03	0.02	0.03	0.03	0.05	29.37	0.06	0.08	60.00	60.00	60.00	0.01
709	0.02	0.02	0.02	0.02	0.05	0.05	60.00	0.07	0.08	60.00	60.00	60.00	0.01
710	0.01	0.02	0.02	0.02	0.02	0.02	49.24	0.09	0.05	0.37	0.29	0.03	0.01
711	0.01	0.02	0.01	0.02	0.02	0.02	27.12	0.05	0.06	9.03	19.60	20.22	0.02
712	0.01	0.02	0.02	0.02	0.02	0.02	38.41	0.05	0.07	8.09	20.98	20.23	0.02
713	0.02	0.02	0.02	0.02	0.03	0.05	60.00	0.08	0.05	4.51	60.00	60.00	0.01
714	0.01	0.02	0.01	0.02	0.03	0.03	60.00	0.10	0.07	2.09	2.25	0.05	0.01
715	0.01	0.02	0.01	0.02	0.02	0.02	60.00	0.06	0.06	0.08	0.16	20.05	0.01
716	0.01	0.02	0.02	0.02	0.03	0.02	60.00	0.06	0.10	0.12	0.15	20.05	0.01
717	0.02	0.02	0.02	0.02	0.03	0.03	60.00	0.08	0.07	0.34	0.50	0.06	0.01
718	0.02	0.02	0.02	0.02	0.02	0.03	60.00	0.07	0.07	0.29	0.47	0.07	0.01
719	0.02	0.02	0.02	0.02	0.02	0.03	60.00	0.08	0.09	0.31	0.51	0.06	0.01
720	0.01	0.03	0.02	0.03	0.02	0.04	0.32	0.07	0.10	0.96	2.85	20.20	0.01
721	0.02	0.04	0.02	0.04	0.02	0.05	0.35	0.08	0.10	60.00	60.00	20.25	0.01
722	0.02	0.03	0.02	0.03	0.02	0.04	4.64	0.07	0.06	0.33	2.34	0.05	0.02
723	0.02	0.02	0.02	0.02	0.03	0.02	4.63	0.09	0.06	0.43	0.46	0.05	0.02
724	0.02	0.02	0.02	0.02	0.03	0.03	60.00	0.09	0.07	60.00	60.00	60.00	0.01
725	0.02	0.02	0.02	0.02	0.03	0.03	60.00	0.08	0.09	0.31	0.38	0.05	0.01
726	0.02	0.02	0.02	0.02	0.03	0.03	60.00	0.05	0.07	2.45	2.28	0.06	0.01
727	0.01	0.02	0.02	0.02	0.02	0.02	0.94	0.06	0.10	0.20	0.26	0.06	0.01
728	0.01	0.02	0.02	0.02	0.01	0.02	60.00	0.07	0.10	0.23	0.24	0.05	0.01
729	0.02	0.02	0.02	0.02	0.02	0.02	15.12	0.06	0.06	1.31	0.80	20.17	0.01
730	0.01	0.02	0.02	0.02	0.02	0.02	60.00	0.06	0.10	0.37	0.51	0.05	0.01
731	0.01	0.02	0.02	0.02	0.04	0.04	60.00	0.07	0.07	0.51	2.28	0.06	0.01
732	0.02	0.02	0.02	0.02	0.02	0.02	60.00	0.07	0.06	0.37	0.48	0.05	0.01
733	0.02	0.02	0.02	0.02	0.02	0.02	60.00	0.08	0.08	0.36	0.37	0.05	0.01
734	0.01	0.02	0.02	0.02	0.02	0.02	60.00	0.08	0.08	0.36	0.45	0.06	0.01
735	0.01	0.02	0.02	0.02	0.02	0.02	60.00	0.05	0.05	0.39	0.42	0.06	0.01
736	0.01	0.02	0.02	0.02	0.02	0.02	0.53	0.07	0.08	0.39	0.43	0.06	0.01
737	0.01	0.02	0.02	0.02	0.02	0.02	0.48	0.08	0.07	0.38	0.42	0.05	0.01
738	0.01	0.02	0.02	0.02	0.02	0.02	60.00	0.07	0.08	0.06	0.18	60.00	0.01
739	0.01	0.02	0.02	0.02	0.04	0.05	0.48	0.06	0.12	2.65	0.97	20.25	0.01
740	0.01	0.02	0.02	0.02	0.03	0.04	0.46	0.08	0.10	2.20	2.62	20.38	0.01
741	0.02	0.02	0.02	0.02	0.02	0.02	60.00	0.06	0.06	60.00	60.00	20.22	0.02
742	0.02	0.02	0.02	0.02	0.04	0.05	60.00	0.08	0.07	60.00	60.00	60.00	0.01
743	0.02	0.02	0.02	0.02	0.04	0.04	60.00	0.08	0.07	60.00	60.00	60.00	0.01
744	0.01	0.02	0.02	0.02	0.04	0.04	0.61	0.08	0.12	60.00	60.00	60.00	0.01
745	0.02	0.02	0.02	0.02	0.04	0.04	60.00	0.07	0.08	0.37	0.29	0.07	0.01
746	0.01	0.02	0.02	0.02	0.04	0.04	60.00	0.07	0.07	60.00	60.00	60.00	0.02
747	0.02	0.02	0.02	0.02	0.04	0.04	60.00	0.08	0.06	0.28	0.35	0.07	0.01
748	0.02	0.02	0.02	0.03	0.04	0.04	0.72	0.07	0.13	60.00	60.00	20.25	0.01
749	0.01	0.02	0.02	0.03	0.04	0.04	60.00	0.12	0.07	60.00	60.00	60.00	0.01
750	0.02	0.02	0.02	0.02	0.04	0.04	60.00	0.06	0.08	60.00	60.00	60.00	0.01
751	0.02	0.02	0.02	0.02	0.03	0.04	0.60	0.07	0.16	60.00	60.00	60.00	0.01
752	0.01	0.02	0.02	0.02	0.04	0.04	60.00	0.05	0.08	0.34	0.34	0.08	0.01
753	0.02	0.02	0.02	0.02	0.04	0.04	60.00	0.04	0.06	60.00	60.00	60.00	0.01
754	0.02	0.02	0.02	0.02	0.04	0.04	60.00	0.08	0.06	60.00	60.00	60.00	0.01
755	0.02	0.02	0.02	0.03	0.04	0.04	0.61	0.09	0.12	60.00	60.00	20.26	0.01
756	0.02	0.03	0.02	0.05	0.04	0.04	0.66	0.09	0.12	60.00	60.00	20.27	0.01
757	0.01	0.02	0.02	0.04	0.04	0.04	60.00	0.06	0.09	60.00	60.00	60.00	0.01
758	0.02	0.02	0.01	0.02	0.02	0.02	0.46	0.08	0.06	0.64	0.71	20.14	0.01
759	0.02	0.02	0.02	0.02	0.02	0.02	0.41	0.09	0.07	0.55	0.72	20.13	0.01
760	0.02	0.02	0.02	0.02	0.02	0.02	60.00	0.07	0.07	1.99	2.56	60.00	0.01
761	0.02	0.04	0.02	0.04	0.02	0.04	0.37	0.07	0.14	0.60	0.74	20.16	0.01
762	0.02	0.05	0.02	0.05	0.03	0.05	0.38	0.06	0.12	0.65	0.71	20.23	0.01
763	0.02	0.03	0.02	0.03	0.02	0.04	60.00	0.08	0.08	2.37	2.62	60.00	0.01
764	0.02	0.02	0.02	0.02	0.02	0.03	0.68	0.07	0.08	1.86	0.47	0.05	0.01
765	0.02	0.02	0.02	0.02	0.03	0.02	60.00	0.08	0.08	0.36	0.41	20.39	0.01
766	0.02	0.02	0.02	0.02	0.03	0.03	0.52	0.07	0.10	1.76	1.83	20.09	0.01
767	0.02	0.02	0.01	0.02	0.02	0.02	60.00	0.06	0.10	0.20	0.22	20.43	0.01
768	0.02	0.01	0.01	0.02	0.02	0.02	60.00	0.07	0.08	0.40	0.39	20.30	0.01
769	0.01	0.02	0.02	0.04	0.02	0.02	0.33	0.07	0.07	0.20	0.24	20.12	0.01
770	0.02	0.02	0.02	0.03	0.02	0.02	5.39	0.06	0.10	0.11	0.17	20.16	0.01
771	0.02	0.03	0.02	0.03	0.02	0.02	0.28	0.06	0.09	0.49	0.68	20.32	0.01
772	0.02	0.04	0.02	0.05	0.02	0.02	0.26	0.06	0.08	0.14	0.18	20.33	0.01
773	0.02	0.03	0.02	0.03	0.02	0.02	60.00	0.07	0.08	2.60	6.89	0.07	0.01
774	0.01	0.02	0.01	0.02	0.02	0.02	5.36	0.08	0.09	0.13	0.18	20.17	0.01
775	0.01	0.04	0.02	0.04	0.02	0.04	0.29	0.08	0.11	0.10	0.18	20.17	0.01
776	0.01	0.03	0.02	0.03	0.02	0.04	5.31	0.07	0.08	0.07	0.17	20.57	0.01
777	0.02	0.01	0.02	0.02	0.02	0.03	60.00	0.08	0.12	0.11	0.16	20.11	0.01
778	0.02	0.03	0.02	0.04	0.03	0.05	0.35	0.05	0.08	0.07	0.13	20.24	0.01
779	0.01	0.03	0.01	0.03	0.02	0.03	0.59	0.07	0.08	0.08	0.13	20.27	0.01
780	0.01	0.02	0.02	0.02	0.02	0.02	60.00	0.08	0.08	0.83	0.22	20.22	0.01
781	0.02	0.01	0.02	0.02	0.01	0.02	0.70	0.07	0.11	1.20	0.13	0.05	0.01
782	0.02	0.01	0.01	0.02	0.02	0.02	0.66	0.08	0.12	0.13	0.15	0.05	0.01
783	0.01	0.02	0.02	0.02	0.01	0.02	5.84	0.08	0.14	0.16	0.41	20.24	0.01
784	0.01	0.02	0.02	0.01	0.02	0.02	0.72	0.06	0.10	0.07	0.68	20.31	0.01
785	0.02	0.02	0.02	0.02	0.03	0.04	60.00	0.04	0.08	2.28	60.00	60.00	0.01
786	0.01	0.02	0.02	0.02	0.04	0.03	60.00	0.07	0.09	60.00	60.00	60.00	0.01
787	0.02	0.02	0.01	0.02	0.02	0.02	0.73	0.06	0.15	0.07	0.62	20.15	0.01
788	0.02	0.04	0.01	0.03	0.03	0.04	0.36	0.07	0.10	0.11	2.28	20.11	0.01
789	0.02	0.05	0.01	0.05	0.02	0.05	0.29	0.07	0.08	0.13	0.17	20.16	0.01
790	0.02	0.03	0.01	0.03	0.02	0.03	3.41	0.09	0.07	0.13	0.18	20.10	0.01
791	0.02	0.02	0.02	0.02	0.02	0.02	0.65	0.04	0.08	0.08	0.12	20.10	0.01
979	0.02	0.03	0.02	0.03	0.04	0.04	0.39	0.04	0.10	60.00	60.00	20.22	0.02
980	0.01	0.03	0.02	0.03	0.03	0.04	60.00	0.09	0.09	60.00	60.00	20.24	0.02
982	0.02	0.03	0.01	0.02	0.03	0.04	0.37	0.06	0.08	6.26	6.82	60.00	0.01
984	0.02	0.05	0.02	0.04	0.04	0.04	0.31	0.06	0.10	0.08	0.11	20.19	0.01
990	0.00	0.01	0.00	0.01	0.01	0.01	0.33	0.07	0.07	1.54	1.62	20.13	0.01
991	0.00	0.01	0.00	0.01	0.01	0.01	0.30	0.05	0.07	0.13	2.69	20.42	0.01
995	0.02	0.03	0.02	0.03	0.02	0.03	0.28	0.06	0.10	0.29	0.22	0.09	0.01
996	0.01	0.02	0.01	0.02	0.02	0.02	0.33	0.07	0.10	0.13	0.14	21.40	0.01
997	0.02	0.02	0.02	0.02	0.02	0.02	0.29	0.08	0.12	0.08	0.12	0.09	0.01
998	0.02	0.02	0.02	0.02	0.02	0.02	0.41	0.07	0.13	0.42	2.08	20.15	0.01
999	0.02	0.01	0.02	0.02	0.02	0.02	0.41	0.07	0.13	0.41	0.43	20.15	0.01
1000	0.02	0.02	0.02	0.02	0.02	0.03	1.37	0.06	0.13	0.35	3.92	20.26	0.01
1127	0.01	0.01	0.02	0.02	0.02	0.04	0.42	0.05	0.06	0.34	0.42	60.00	0.01
1128	0.01	0.01	0.02	0.02	0.02	0.04	8.93	0.05	0.05	0.36	0.34	0.05	0.01
1129	0.02	0.01	0.01	0.01	0.02	0.04	0.35	0.07	0.06	0.40	0.38	60.00	0.01
1130	0.01	0.01	0.02	0.02	0.03	0.04	0.41	0.10	0.07	0.16	0.22	60.00	0.01
1612	0.01	0.02	0.02	0.02	0.04	0.04	0.81	0.07	0.06	60.00	60.00	60.00	0.01
1613	0.02	0.03	0.02	0.02	0.03	0.05	0.65	0.07	0.08	60.00	60.00	20.26	0.01