CSI

This site provides experiments for the paper CSI: New Evidence – A Progress Report by Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp.

Experiments for Unique normal forms of TRSs (Table 2)

UN denotes unique normal forms with respect to reductions
UNC denotes unique normal forms with respect to conversions
CR denotes confluence

Note that clicking a cell in the Results table below shows the corresponding tool output.

Statistics

	CSI-UN	CSI-UNC	CSI-CR
#yes	43	37	17
total time	100.9	95.9	73.0
average time	2.3	2.6	4.3
#no	27	33	81
total time	23.9	27.0	129.5
average time	0.9	0.8	1.6
#maybe	42	42	13
total time	473.6	474.6	195.8
average time	11.3	11.3	15.1
#timeout	8	8	9
total time	480.0	480.0	540.0
average time	60.0	60.0	60.0
#total	120	120	120
total time	1078.4	1077.5	938.2

Results

	CSI-UN	CSI-UNC	CSI-CR
5	0.5	0.5	0.5
6	0.5	0.5	0.4
7	0.5	0.4	0.5
9	0.4	0.5	0.5
10	0.5	0.4	0.4
13	0.5	0.6	0.4
15	10.7	10.7	10.5
16	1.9	2.1	2.6
21	0.7	0.7	0.6
24	0.4	0.4	20.6
26	0.4	0.4	60.0
27	15.8	15.7	15.7
31	0.4	0.4	0.4
32	0.4	0.4	0.4
38	0.7	0.7	0.7
39	0.7	0.7	0.7
43	0.5	0.5	0.4
44	0.5	0.4	0.4
46	0.6	0.6	0.5
47	0.6	0.7	14.6
49	11.3	11.4	1.0
52	14.9	15.1	14.8
54	0.4	0.4	14.7
56	0.5	0.4	14.7
57	0.4	0.4	14.7
	CSI-UN	CSI-UNC	CSI-CR
58	14.8	15.0	14.9
62	0.9	0.9	0.9
64	1.3	1.4	1.0
70	0.5	0.5	0.5
76	0.6	0.6	0.6
77	5.9	5.7	4.8
78	20.5	20.6	12.3
80	0.6	0.5	0.5
95	0.5	0.4	0.4
98	0.4	0.4	0.6
109	8.1	7.4	5.9
110	60.0	60.0	60.0
113	9.5	9.3	0.9
126	60.0	60.0	60.0
143	0.9	0.5	0.6
144	0.7	0.7	1.0
160	31.8	31.0	32.1
170	60.0	60.0	60.0
173	14.9	14.9	15.3
175	7.0	7.1	4.9
183	1.6	1.6	1.7
185	1.5	1.7	1.5
206	1.5	1.6	1.6
208	17.5	16.8	7.5
212	0.7	0.7	1.5
	CSI-UN	CSI-UNC	CSI-CR
214	0.8	0.8	1.1
215	0.7	0.8	1.2
216	20.9	20.8	10.7
225	0.5	0.5	0.4
226	20.4	20.5	0.6
227	15.0	14.8	14.8
230	0.4	0.4	16.3
231	0.5	0.6	14.7
234	14.6	14.8	14.6
236	5.4	5.6	0.5
237	10.7	10.9	0.6
238	5.1	5.2	0.6
239	0.7	0.7	0.6
240	11.5	11.6	0.6
241	9.6	9.6	0.6
242	2.4	2.4	0.6
243	11.5	11.5	0.6
244	10.7	10.7	0.6
245	12.0	12.1	0.7
246	12.4	12.4	0.7
247	10.8	10.8	0.6
248	0.7	0.6	0.6
249	11.4	11.5	0.7
250	15.2	16.3	15.0
251	11.6	11.5	1.1
	CSI-UN	CSI-UNC	CSI-CR
252	10.8	10.7	0.6
253	11.0	11.1	0.7
254	10.6	10.7	0.6
255	16.9	17.1	0.7
256	60.0	60.0	60.0
257	60.0	60.0	60.0
258	14.0	12.6	0.6
259	2.1	1.9	2.1
260	1.9	2.0	2.1
261	0.5	0.4	0.5
392	0.5	0.5	0.4
414	60.0	60.0	60.0
415	60.0	60.0	60.0
417	60.0	60.0	60.0
442	2.0	2.1	2.0
496	15.9	15.9	15.7
497	0.6	0.6	14.3
498	2.2	2.4	2.5
505	0.4	0.4	0.4
507	0.5	0.5	0.6
508	10.8	10.8	0.7
509	10.5	10.5	0.5
510	7.3	7.1	0.4
511	0.6	0.6	0.5
512	3.0	2.9	0.5
	CSI-UN	CSI-UNC	CSI-CR
g75	0.6	0.6	0.5
g81	0.5	0.6	0.5
g103	0.4	0.5	0.5
g127	0.5	0.5	0.5
g185	0.5	0.5	0.4
g240	0.5	0.5	0.5
g251	0.5	0.5	0.4
g282	0.5	0.6	0.5
g307	0.5	0.6	0.5
fort1	10.5	10.5	0.4
fort2	10.9	11.0	0.6
fort3	10.8	10.9	0.6
fort4	0.5	0.5	0.5
fort5	0.5	0.5	0.5
fort6	0.5	0.6	0.5
fort7	0.5	0.5	0.5
fort8	0.8	0.8	0.8
fort9	0.7	0.7	0.9
fort10	0.5	0.5	0.6
fr	13.8	13.7	0.7