Features
ProcessorIntel(R) Core(TM) i5-7300U CPU @ 2.60GHz 2.71GHz
RAM8.00 GB
OSLinux 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
DatabaseCOPS and New Examples
Timeout120s
Date09.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