Features
Processor
Intel(R) Core(TM) i5-7300U CPU @ 2.60GHz 2.71GHz
RAM
8.00 GB
OS
Linux 4.4.0-17134-Microsoft
Program Versions
Mace4 (64) version 2009-11A, November 2009.
Prover9 (64) version 2009-11A, November 2009.
AGES, version 1.0
Barcelogic 2016
infChecker, version 1.0
muTerm, version 5.0
Database
COPS and New Examples
Timeout
120s
Date
09.01.21
Examples
confident-1.0.5
ConCon+CeTA
ConCon
Ex16_LucFSTTCS21_JOIN.trs
20.087
0.9
0.9
Ex16_LucFSTTCS21_ORIENTED.trs
120
0.9
1.39
JLAMP21CTRS.trs
0.001
1.17
0.85
JLAMP21CTRS_1.trs
0.005
1.31
0.9
JLAMP21CTRS_2.trs
67.05
1.09
1.46
DerOkaSivT4_SalvaEx.trs
31.007
1.43
1.43
osp1-ctrs.trs
25.008
1.09
1.15
osp2-ctrs.trs
25.008
1.15
1.16
osp3-ctrs.trs
20.027
0.99
0.94
osp4-ctrs.trs
0.001
1.42
0.93
osp5-ctrs.trs
120
1.54
1.69
osp6-ctrs.trs
120
1.1
1.14
osp7-ctrs.trs
120
1.2
1.35
osp8-ctrs.trs
45.075
1.09
1.14
osp9-ctrs.trs
25.019
1.06
1.11
ex-weakness.trs
25.034
1.29
0.96
262.trs
120
1.25
1.35
263.trs
120
1.27
2.12
264.trs
0.005
1.19
1.17
266.trs
0.001
1.36
1.35
267.trs
0.001
1.39
1.71
268.trs
0.001
1.22
1.25
271.trs
35.019
1.23
1.29
272.trs
120
1.48
5
278.trs
120
1.61
2.29
279.trs
120
60.14
60.14
284.trs
106.01
58.74
58.74
285.trs
101.064
2.96
5.1
286.trs
85.012
1.36
2.27
287.trs
0.001
1.17
1.22
288.trs
25.045
1.43
2.07
289.trs
120
1.25
2.49
292.trs
120
2.49
6.51
293.trs
0.009
1.25
1.6
294.trs
0.001
1.21
1.17
307.trs
0.001
1.34
1.36
308.trs
25.032
1.29
1.34
310.trs
25.011
1.33
1.84
311.trs
20.037
1.2
1.52
312.trs
20.042
1.22
1.56
313.trs
0.041
1.44
2.28
315.trs
25.062
1.25
1.81
316.trs
10.001
1.33
1.98
317.trs
20.02
1.23
1.42
319.trs
5.002
1.2
1.68
321.trs
25.044
1.27
1.56
322.trs
120
1.5
1.68
323.trs
25.017
1.25
1.37
324.trs
41.005
0.95
2.35
325.trs
25.043
1.29
1.64
326.trs
20.015
1.27
2.3
327.trs
120
5.82
10.17
328.trs
120
1.45
2.56
329.trs
120
1.56
1.78
330.trs
67.012
1.26
1.7
332.trs
46.05
1.36
1.54
333.trs
0.001
1.3
1.3
334.trs
0.001
1.23
1.19
335.trs
120
1.48
1.72
336.trs
40.012
1.27
1.48
337.trs
120
31.9
31.9
339.trs
0.011
1.59
1.72
340.trs
20.029
0
3.35
341.trs
0.001
1.25
1.2
342.trs
80.043
2.12
2.12
343.trs
0.001
1.27
1.2
344.trs
0.001
1.24
1.29
345.trs
0.007
1.29
1.29
346.trs
0.011
1.48
1.48
347.trs
0.006
1.29
1.29
348.trs
0.007
1.9
1.9
349.trs
75.091
1.35
1.35
350.trs
0.008
1.57
1.57
351.trs
20.004
1.41
1.74
352.trs
72.082
1.23
1.72
353.trs
20.042
1.41
1.78
354.trs
0.001
1.31
1.9
355.trs
0.001
1.15
1.45
356.trs
0.001
1.19
1.12
357.trs
30.076
1.41
1.68
358.trs
25.012
1.24
1.24
359.trs
0.001
1.17
1.41
360.trs
20.017
1.35
1.7
361.trs
112.047
0
3.55
362.trs
25.006
1.27
1.73
363.trs
20.038
1.33
1.43
364.trs
0.001
1.24
1.25
365.trs
120
3.2
3.2
366.trs
25.017
1.16
1.24
367.trs
20.037
1.26
1.68
368.trs
3.071
1.25
1.25
369.trs
19.035
1.31
1.49
370.trs
5.093
1.55
3.04
371.trs
0.096
1.22
1.75
372.trs
35.089
1.23
1.55
373.trs
20.024
1.18
1.29
374.trs
25.024
1.14
1.25
375.trs
5.003
1.33
1.81
376.trs
0.001
1.25
1.26
Examples
confident-1.0.5
ConCon+CeTA
ConCon
377.trs
25.043
1.25
1.4
378.trs
120
58.74
58.74
379.trs
25.035
1.14
1.66
380.trs
0.001
1.26
1.23
381.trs
46.006
1.34
1.67
382.trs
10.003
1.26
1.7
383.trs
25.059
1.18
1.37
384.trs
25.046
1.24
1.48
385.trs
35.002
1.31
1.3
386.trs
0.001
1.16
1.35
387.trs
120
2.27
2.27
388.trs
0.001
1.25
1.53
389.trs
93.045
32.02
32.02
390.trs
0.001
1.2
1.14
391.trs
120
1.38
1.85
403.trs
25.033
1.32
1.27
404.trs
79.05
1.37
2
405.trs
120
32.11
32.11
406.trs
120
3.33
3.33
407.trs
120
2.9
2.9
408.trs
82.05
1.76
3.39
409.trs
82.057
2.93
2.93
410.trs
25.043
1.31
1.96
411.trs
25.045
1.37
2.01
439.trs
120
1.29
1.37
440.trs
45.035
58.55
2.36
441.trs
55.028
1.26
1.3
488.trs
0.001
1.33
1.37
489.trs
46.02
1.67
3.98
490.trs
0.001
1.19
1.19
491.trs
25.032
1.35
2.06
492.trs
20.089
1.27
1.95
493.trs
120.001
1.69
4.15
494.trs
25.027
1.32
2.12
495.trs
25.029
1.21
1.27
499.trs
120
58.59
34.06
522.trs
46.018
1.79
3.67
523.trs
0.016
4.55
2.42
524.trs
0.006
0.97
1.25
527.trs
0.001
1.23
1.21
528.trs
0.001
1.34
1.36
529.trs
120
58.57
18.42
546.trs
5.002
1.23
1.24
547.trs
25.022
1.27
1.3
548.trs
0.001
0.91
1.15
549.trs
0.004
1.19
1.12
550.trs
0.009
1.43
2.06
551.trs
120
1.45
5.38
552.trs
120
1.44
4.12
553.trs
57.074
5.08
5.08
790.trs
103.096
2.75
2.75
791.trs
107.012
2.2
2.2
792.trs
25.037
1.24
1.59
793.trs
20.003
1.23
1.2
794.trs
21.017
1.17
1.39
796.trs
25.013
1.11
1.22
798.trs
120
58.75
58.75
799.trs
0.001
1.24
1.23
805.trs
120
1.56
3.77
807.trs
120
1.14
2
1123.trs
67.035
2.08
6.14
1138.trs
40.059
1.11
1.49
1139.trs
25.017
1.3
1.8
1140.trs
20.043
1.3
1.33
confident-1.0.5
ConCon+CeTA
ConCon
Time
3076.235
729.61
681.07
#YES
70
67
75
#MAYBE
51
50
41
#NO
42
46
47
Avg.YES
15.57
1.38
2.02
Avg.NO
26.42
1.25
1.53