cl-banner

CSI


Description

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 437.6 474.6 195.8
average time 11.3 11.3 15.1
#time out 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

 

Nach oben scrollen