Features
Processor
Intel(R) Core(TM)2 Duo 2.16GHz
RAM
1GB SDRAM
OS
Ubuntu-Linux 2.6.24-19-generic
Program Versions
MuTerm + MultiSolver
Database
TPDB 4.0 (May 2007)
Timeout
240s
Date
07.20.22
Proving Operational Termination vs. Proving Termination
TPDB CTRS Problems
COPS CTRS Problems
Examples
MU-TERM (operational termination)
MU-TERM (termination)
TRS_Conditional/COPS/262.xml
0.01
29.61
TRS_Conditional/COPS/263.xml
0.02
1.02
TRS_Conditional/COPS/264.xml
0.00
1.44
TRS_Conditional/COPS/266.xml
0.40
30.56
TRS_Conditional/COPS/267.xml
0.00
29.95
TRS_Conditional/COPS/268.xml
0.01
29.82
TRS_Conditional/COPS/271.xml
0.19
30.02
TRS_Conditional/COPS/272.xml
0.01
30.04
TRS_Conditional/COPS/286.xml
0.03
29.96
TRS_Conditional/COPS/288.xml
0.10
0.59
TRS_Conditional/COPS/289.xml
240
240
TRS_Conditional/COPS/292.xml
0.04
4.89
TRS_Conditional/COPS/293.xml
0.02
0.18
TRS_Conditional/COPS/294.xml
0.00
0.44
TRS_Conditional/COPS/307.xml
0.00
29.96
TRS_Conditional/COPS/308.xml
0.01
0.85
TRS_Conditional/COPS/310.xml
0.37
30.31
TRS_Conditional/COPS/311.xml
240
240
TRS_Conditional/COPS/312.xml
240
240
TRS_Conditional/COPS/315.xml
0.04
9.14
TRS_Conditional/COPS/316.xml
0.02
1.89
TRS_Conditional/COPS/317.xml
0.05
0.19
TRS_Conditional/COPS/319.xml
0.01
1.11
TRS_Conditional/COPS/321.xml
0.00
13.59
TRS_Conditional/COPS/322.xml
0.06
30.01
TRS_Conditional/COPS/323.xml
0.04
1.18
TRS_Conditional/COPS/324.xml
0.03
29.96
TRS_Conditional/COPS/325.xml
0.01
4.35
TRS_Conditional/COPS/326.xml
0.00
29.97
TRS_Conditional/COPS/329.xml
240
240
TRS_Conditional/COPS/330.xml
0.00
1.03
TRS_Conditional/COPS/332.xml
0.01
1.69
TRS_Conditional/COPS/333.xml
0.00
2.78
TRS_Conditional/COPS/334.xml
0.05
0.40
TRS_Conditional/COPS/337.xml
240
240
TRS_Conditional/COPS/339.xml
0.00
7.11
TRS_Conditional/COPS/340.xml
0.00
3.09
TRS_Conditional/COPS/341.xml
0.01
0.62
TRS_Conditional/COPS/342.xml
157.30
186.98
TRS_Conditional/COPS/343.xml
0.00
29.93
TRS_Conditional/COPS/344.xml
0.00
1.02
TRS_Conditional/COPS/351.xml
0.03
29.93
TRS_Conditional/COPS/353.xml
109.35
154.44
TRS_Conditional/COPS/354.xml
0.00
0.76
TRS_Conditional/COPS/355.xml
0.01
0.13
TRS_Conditional/COPS/356.xml
0.04
0.26
TRS_Conditional/COPS/358.xml
0.01
0.44
TRS_Conditional/COPS/359.xml
0.00
0.78
TRS_Conditional/COPS/361.xml
240
240
TRS_Conditional/COPS/364.xml
0.01
0.95
TRS_Conditional/COPS/365.xml
0.00
0.58
TRS_Conditional/COPS/366.xml
0.00
0.47
TRS_Conditional/COPS/367.xml
0.00
0.27
TRS_Conditional/COPS/368.xml
0.01
0.42
TRS_Conditional/COPS/369.xml
0.05
2.83
TRS_Conditional/COPS/370.xml
0.01
6.47
TRS_Conditional/COPS/371.xml
0.01
0.55
TRS_Conditional/COPS/372.xml
0.00
3.55
TRS_Conditional/COPS/373.xml
0.01
1.40
TRS_Conditional/COPS/374.xml
0.00
0.63
TRS_Conditional/COPS/375.xml
0.01
1.29
TRS_Conditional/COPS/376.xml
0.01
0.41
TRS_Conditional/COPS/377.xml
0.01
2.11
TRS_Conditional/COPS/378.xml
153.73
182.28
TRS_Conditional/COPS/379.xml
0.00
29.91
TRS_Conditional/COPS/380.xml
0.00
0.79
TRS_Conditional/COPS/381.xml
0.00
1.95
TRS_Conditional/COPS/382.xml
0.02
2.93
TRS_Conditional/COPS/383.xml
0.02
1.03
TRS_Conditional/COPS/384.xml
0.02
2.23
TRS_Conditional/COPS/385.xml
0.01
0.69
TRS_Conditional/COPS/387.xml
0.00
0.48
TRS_Conditional/COPS/388.xml
0.00
29.92
TRS_Conditional/COPS/389.xml
0.00
29.74
TRS_Conditional/COPS/390.xml
0.00
0.35
TRS_Conditional/COPS/391.xml
0.75
0.55
TRS_Conditional/COPS/403.xml
0.00
0.68
TRS_Conditional/COPS/404.xml
0.00
0.52
TRS_Conditional/COPS/405.xml
240
240
TRS_Conditional/COPS/406.xml
0.01
2.53
TRS_Conditional/COPS/407.xml
0.06
29.86
TRS_Conditional/COPS/408.xml
0.02
2.02
TRS_Conditional/COPS/409.xml
0.01
29.88
TRS_Conditional/COPS/410.xml
0.00
2.72
TRS_Conditional/COPS/411.xml
0.00
29.87
TRS_Conditional/Mixed_CTRS/AAECC-ring-cond.xml
240
240
TRS_Conditional/Mixed_CTRS/AAECCcond.xml
240
240
TRS_Conditional/Mixed_CTRS/fib.xml
35.80
65.39
TRS_Conditional/Mixed_CTRS/gcd.xml
0.15
29.97
TRS_Conditional/Mixed_CTRS/quick.xml
0.04
0.05
TRS_Conditional/Mixed_CTRS/quicksort.xml
1.95
31.37
TRS_Conditional/Mixed_CTRS/quotrem.xml
0.20
30.22
TRS_Conditional/Mixed_CTRS_2014/ex1-lucmes-wrla14.xml
240
240
TRS_Conditional/Mixed_CTRS_2014/ex1-muterm14.xml
0.05
0.15
TRS_Conditional/Mixed_CTRS_2014/ex2-lucmes-wrla14.xml
198.54
240
TRS_Conditional/Mixed_CTRS_2014/ex2-muterm14.xml
0.01
0.22
TRS_Conditional/Mixed_CTRS_2014/ex3-muterm14.xml
0.01
30.01
TRS_Conditional/Mixed_CTRS_2014/hosc08-ex5-aecc-p46.xml
0.17
29.95
TRS_Conditional/Mixed_CTRS_2014/jlap09-ex16.xml
0.10
30.09
TRS_Conditional/Mixed_CTRS_2014/jlap09-ex17.xml
205.61
235.41
TRS_Conditional/Mixed_CTRS_2014/logic.xml
240
240
TRS_Conditional/Mixed_CTRS_2014/lucMarMes.xml
0.01
0.24
TRS_Conditional/Mixed_CTRS_2014/mar.xml
240
240
TRS_Conditional/Mixed_CTRS_2014/mar_simple1.xml
240
240
TRS_Conditional/Mixed_CTRS_2014/mar_simple2.xml
240
240
TRS_Conditional/Mixed_CTRS_2014/minus1.xml
0.01
0.68
TRS_Conditional/Mixed_CTRS_2014/ohl.xml
134.07
164.48
TRS_Conditional/Mixed_CTRS_2014/ohl190.xml
0.01
0.49
TRS_Conditional/Mixed_CTRS_2014/ohl194.xml
0.29
30.30
TRS_Conditional/Mixed_CTRS_2014/ohl196.xml
0.02
0.39
TRS_Conditional/Mixed_CTRS_2014/ohl206.xml
0.01
29.89
TRS_Conditional/Mixed_CTRS_2014/ohl211.xml
0.06
0.54
TRS_Conditional/Mixed_CTRS_2014/ohl216.xml
0.00
0.92
TRS_Conditional/Mixed_CTRS_2014/ohl228.xml
137.16
167.15
TRS_Conditional/Mixed_CTRS_2014/ohl230.xml
0.04
29.92
TRS_Conditional/Mixed_CTRS_2014/plus1.xml
0.02
29.93
TRS_Conditional/Mixed_CTRS_2014/sche128.xml
0.14
0.81
MU-TERM (operational termination)
MU-TERM (termination)
#YES
86
90
#MAYBE
15
16
#NO
16
11
Examples
MU-TERM (operational termination)
MU-TERM (termination)
1123.trs
0.05
2.79
1138.trs
0.00
29.95
1139.trs
0.04
5.07
1140.trs
0.00
29.90
1158.trs
0.01
0.94
1159.trs
0.00
0.53
262.trs
0.00
29.79
263.trs
0.00
0.77
264.trs
0.05
1.27
265.trs
0.00
0.06
266.trs
0.35
30.42
267.trs
0.00
29.93
268.trs
0.00
29.84
271.trs
0.12
30.12
272.trs
0.00
29.99
277.trs
0.00
29.88
278.trs
240
240
279.trs
240
240
284.trs
0.00
1.46
285.trs
0.00
2.07
286.trs
0.00
29.95
287.trs
0.00
1.83
288.trs
0.12
0.54
289.trs
240
240
292.trs
0.00
4.14
293.trs
0.00
0.24
294.trs
0.00
0.38
307.trs
0.00
30.08
308.trs
0.06
0.73
309.trs
0.00
29.86
310.trs
0.26
30.32
311.trs
240
240
312.trs
240
240
313.trs
0.04
64.23
314.trs
0.00
29.97
315.trs
0.00
10.20
316.trs
0.05
2.73
317.trs
0.00
0.15
318.trs
0.00
29.95
319.trs
0.00
1.17
320.trs
0.00
29.94
321.trs
0.02
13.60
322.trs
0.00
30.07
323.trs
0.00
1.11
324.trs
0.00
30.03
325.trs
0.01
4.20
326.trs
0.00
29.96
327.trs
0.21
30.08
328.trs
0.00
29.60
329.trs
240
240
330.trs
0.00
0.78
332.trs
0.05
1.70
333.trs
0.00
2.89
334.trs
0.00
0.43
335.trs
0.10
30.23
336.trs
0.00
30.01
337.trs
240
240
339.trs
0.00
7.22
340.trs
0.00
3.07
341.trs
0.00
0.60
342.trs
157.30
187.50
343.trs
0.00
29.87
344.trs
0.00
1.03
345.trs
0.00
29.94
346.trs
0.00
30.03
347.trs
0.00
29.89
348.trs
0.00
30.03
349.trs
0.00
29.97
350.trs
0.00
30.08
351.trs
0.00
30.08
352.trs
0.00
29.93
353.trs
240
240
354.trs
0.01
0.75
355.trs
0.02
0.15
356.trs
0.00
0.30
357.trs
240
240
358.trs
0.00
0.43
359.trs
0.00
0.74
360.trs
134.57
164.27
361.trs
240
240
362.trs
0.09
30.05
Examples 99%
MU-TERM (operational termination)
MU-TERM (termination)
363.trs
205.44
235.78
364.trs
0.00
0.97
365.trs
0.00
0.67
366.trs
0.00
0.49
367.trs
0.00
0.29
368.trs
0.04
0.40
369.trs
0.03
2.79
370.trs
0.00
6.67
371.trs
0.00
0.57
372.trs
0.00
3.41
373.trs
0.01
1.41
374.trs
0.04
0.61
375.trs
0.00
1.21
376.trs
0.00
0.39
377.trs
0.03
2.15
378.trs
152.51
183.75
379.trs
0.04
29.78
380.trs
0.00
0.71
381.trs
0.00
1.99
382.trs
0.00
2.83
383.trs
0.00
0.88
384.trs
0.00
2.27
385.trs
0.00
0.73
386.trs
0.00
0.29
387.trs
0.00
0.39
388.trs
0.02
29.95
389.trs
0.00
29.70
390.trs
0.00
0.27
391.trs
0.73
0.55
403.trs
0.00
0.64
404.trs
0.00
0.40
405.trs
240
240
406.trs
0.00
2.54
407.trs
0.00
29.86
408.trs
0.00
2.04
409.trs
0.00
29.94
410.trs
0.00
2.73
411.trs
0.05
29.84
439.trs
0.04
2.14
440.trs
0.00
2.35
441.trs
0.29
30.20
488.trs
0.00
29.94
489.trs
0.00
0.79
490.trs
0.00
0.49
491.trs
0.00
0.58
492.trs
0.00
0.86
493.trs
0.13
29.80
494.trs
0.00
29.86
495.trs
0.00
29.83
499.trs
240
240
522.trs
0.03
0.75
523.trs
0.56
29.60
524.trs
0.00
29.79
527.trs
0.00
29.99
528.trs
0.00
29.95
529.trs
240
240
546.trs
0.07
30.10
547.trs
0.00
0.30
548.trs
0.00
0.64
549.trs
0.00
0.31
550.trs
0.02
0.45
551.trs
0.02
1.76
552.trs
0.00
1.45
553.trs
0.00
1.31
790.trs
0.00
30.01
791.trs
0.00
29.99
792.trs
0.06
29.94
793.trs
0.06
29.90
794.trs
0.00
0.46
796.trs
0.05
29.98
798.trs
0.21
30.13
799.trs
198.53
29.98
805.trs
0.00
29.93
806.trs
0.05
0.66
807.trs
0.00
0.33
MU-TERM (operational termination)
MU-TERM (termination)
#YES
95
110
#MAYBE
32
27
#NO
29
19