Benchmark

LabelMeaning
SSolution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A}
OBest solution found
TCPU time (TO for Time Out)
(out)(err)Standard output and standard error for each solver

ColorMeaning for Complete SolversMeaning for Incomplete Solvers
TextBest solver columnBest solver column
TextOptimal solution with the best CPU timeBest solution with the best CPU time
TextOptimal solution and finished within the Time OutBest solution without the best CPU time
TextOptimal solution and did not finish within the Time OutSolution found but not the best
TextTime OutTime Out
TextBuggy solutionBuggy solution

Instance file name Best solver Sat4j-i ubcsat-irots
ped2.B.recomb1-0.01-1.wcnf O = 7
T = 5.29
O = 7
T = 5.29
(out)(err)
O = 1350
T = 179.44
(out)(err)
ped2.B.recomb1-0.01-2.wcnf O = 7
T = 5.65
O = 7
T = 5.65
(out)(err)
O = 155499436
T = 199.73
(out)(err)
ped2.B.recomb1-0.01-3.wcnf O = 6
T = 4.22
O = 6
T = 4.22
(out)(err)
O = 131
T = 195.86
(out)(err)
ped2.B.recomb1-0.01-4.wcnf O = 7
T = 4.09
O = 7
T = 4.09
(out)(err)
O = 1397043
T = 169.41
(out)(err)
ped2.B.recomb1-0.01-5.wcnf O = 7
T = 5.41
O = 7
T = 5.41
(out)(err)
O = 143453563
T = 156.56
(out)(err)
ped2.B.recomb1-0.10-10.wcnf O = 6
T = 5.10
O = 6
T = 5.10
(out)(err)
O = 1573708
T = 195.94
(out)(err)
ped2.B.recomb1-0.10-6.wcnf O = 7
T = 6.04
O = 7
T = 6.04
(out)(err)
O = 183464708
T = 150.77
(out)(err)
ped2.B.recomb1-0.10-7.wcnf O = 588
T = 5.91
O = 588
T = 5.91
(out)(err)
O = 17880566
T = 151.76
(out)(err)
ped2.B.recomb1-0.10-8.wcnf O = 589
T = 4.58
O = 589
T = 4.58
(out)(err)
O = 148141070
T = 144.49
(out)(err)
ped2.B.recomb1-0.10-9.wcnf O = 7
T = 7.69
O = 7
T = 7.69
(out)(err)
O = 152761760
T = 163.21
(out)(err)
ped2.B.recomb1-0.20-11.wcnf O = 7
T = 8.47
O = 7
T = 8.47
(out)(err)
O = 143
T = 209.43
(out)(err)
ped2.B.recomb1-0.20-12.wcnf O = 7
T = 12.01
O = 7
T = 12.01
(out)(err)
O = 157376063
T = 166.10
(out)(err)
ped2.B.recomb1-0.20-13.wcnf O = 7
T = 7.63
O = 7
T = 7.63
(out)(err)
O = 1
T = 158.16
(out)(err)
ped2.B.recomb1-0.20-14.wcnf O = 7
T = 7.10
O = 7
T = 7.10
(out)(err)
O = 12947
T = 189.24
(out)(err)
ped2.B.recomb1-0.20-15.wcnf O = 7
T = 14.23
O = 7
T = 14.23
(out)(err)
O = 182527556
T = 141.18
(out)(err)
ped2.G.recomb1-0.01-1.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 11
T = 190.83
(out)(err)
ped2.G.recomb1-0.01-2.wcnf O = 8771
T = 12.14
O = 8771
T = 12.14
(out)(err)
O = 93594155389
T = 194.37
(out)(err)
ped2.G.recomb1-0.01-3.wcnf O = 11672
T = 29.15
O = 11672
T = 29.15
(out)(err)
O = 15268
T = 194.39
(out)(err)
ped2.G.recomb1-0.01-4.wcnf O = 11665
T = 204.52
O = 11665
T = 204.52
(out)(err)
O = 85779
T = 191.56
(out)(err)
ped2.G.recomb1-0.01-5.wcnf O = 3525
T = 179.34
O = 3525
T = 179.34
(out)(err)
O = 112805820349
T = 190.35
(out)(err)
ped2.G.recomb1-0.10-10.wcnf O = N/A
T = TO
O = 5272
T = 218.36
(out)(err)
O = 8413269181
T = 190.45
(out)(err)
ped2.G.recomb1-0.10-6.wcnf O = N/A
T = TO
O = 9928
T = 16.38
(out)(err)
O = 106690637347
T = 190.84
(out)(err)
ped2.G.recomb1-0.10-7.wcnf O = N/A
T = TO
O = 4694
T = 158.60
(out)(err)
O = 1309484737
T = 191.74
(out)(err)
ped2.G.recomb1-0.10-8.wcnf O = N/A
T = TO
O = 23891
T = 63.05
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb1-0.10-9.wcnf O = N/A
T = TO
O = 7023
T = 199.10
(out)(err)
O = 153527834978
T = 193.83
(out)(err)
ped2.G.recomb1-0.20-11.wcnf O = N/A
T = TO
O = 8760
T = 19.43
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb1-0.20-12.wcnf O = N/A
T = TO
O = 63996
T = 22.86
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb1-0.20-13.wcnf O = N/A
T = TO
O = 42489
T = 21.05
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb1-0.20-14.wcnf O = N/A
T = TO
O = 20399
T = 21.97
(out)(err)
O = 8045545872000
T = 6.83
(out)(err)
ped2.G.recomb1-0.20-15.wcnf O = N/A
T = TO
O = 29109
T = 22.77
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb10-0.01-1.wcnf O = 143075
T = 18.16
O = 143075
T = 18.16
(out)(err)
O = 84806182
T = 190.14
(out)(err)
ped2.G.recomb10-0.01-2.wcnf O = 90175
T = 15.83
O = 90175
T = 15.83
(out)(err)
O = 121797021973
T = 190.91
(out)(err)
ped2.G.recomb10-0.01-3.wcnf O = 122732
T = 224.42
O = 122732
T = 224.42
(out)(err)
O = 93957
T = 190.13
(out)(err)
ped2.G.recomb10-0.01-4.wcnf O = 127985
T = 13.88
O = 127985
T = 13.88
(out)(err)
O = 112324758735
T = 189.21
(out)(err)
ped2.G.recomb10-0.01-5.wcnf O = 138432
T = 13.07
O = 138432
T = 13.07
(out)(err)
O = 121208938958
T = 193.76
(out)(err)
ped2.G.recomb10-0.10-10.wcnf O = N/A
T = TO
O = 154729
T = 18.27
(out)(err)
O = 114
T = 192.17
(out)(err)
ped2.G.recomb10-0.10-6.wcnf O = N/A
T = TO
O = 142512
T = 20.95
(out)(err)
O = 1585846
T = 190.43
(out)(err)
ped2.G.recomb10-0.10-7.wcnf O = N/A
T = TO
O = 104727
T = 18.97
(out)(err)
O = 161481935294
T = 193.51
(out)(err)
ped2.G.recomb10-0.10-8.wcnf O = N/A
T = TO
O = 129148
T = 21.30
(out)(err)
O = 153196372153
T = 196.38
(out)(err)
ped2.G.recomb10-0.10-9.wcnf O = N/A
T = TO
O = 139598
T = 17.14
(out)(err)
O = 195158506861
T = 199.93
(out)(err)
ped2.G.recomb10-0.20-11.wcnf O = N/A
T = TO
O = 152394
T = 23.39
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb10-0.20-12.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb10-0.20-13.wcnf O = N/A
T = TO
O = 111703
T = 25.32
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb10-0.20-14.wcnf O = N/A
T = TO
O = 112284
T = 29.65
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb10-0.20-15.wcnf O = N/A
T = TO
O = 144261
T = 25.58
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb5-0.01-1.wcnf O = 59357
T = 14.39
O = 59357
T = 14.39
(out)(err)
O = 106017096246
T = 199.05
(out)(err)
ped2.G.recomb5-0.01-2.wcnf O = 89010
T = 15.18
O = 89010
T = 15.18
(out)(err)
O = 162401371851
T = 197.51
(out)(err)
ped2.G.recomb5-0.01-3.wcnf O = 69238
T = 14.60
O = 69238
T = 14.60
(out)(err)
O = 127954942753
T = 198.95
(out)(err)
ped2.G.recomb5-0.01-4.wcnf O = 42494
T = 12.61
O = 42494
T = 12.61
(out)(err)
O = 114078061625
T = 187.29
(out)(err)
ped2.G.recomb5-0.01-5.wcnf O = 65762
T = 10.94
O = 65762
T = 10.94
(out)(err)
O = 91680444224
T = 192.90
(out)(err)
ped2.G.recomb5-0.10-10.wcnf O = N/A
T = TO
O = 66914
T = 50.63
(out)(err)
O = 127377722184
T = 195.83
(out)(err)
ped2.G.recomb5-0.10-6.wcnf O = 61125
T = 16.62
O = 61125
T = 16.62
(out)(err)
O = 148535189824
T = 190.84
(out)(err)
ped2.G.recomb5-0.10-7.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 116387359995
T = 192.75
(out)(err)
ped2.G.recomb5-0.10-8.wcnf O = N/A
T = TO
O = 64596
T = 20.79
(out)(err)
O = 151443139
T = 197.23
(out)(err)
ped2.G.recomb5-0.10-9.wcnf O = N/A
T = TO
O = 70991
T = 17.49
(out)(err)
O = 1620
T = 196.08
(out)(err)
ped2.G.recomb5-0.20-11.wcnf O = N/A
T = TO
O = 73908
T = 22.38
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb5-0.20-12.wcnf O = N/A
T = TO
O = 57040
T = 23.27
(out)(err)
O = 7513851317440
T = 6.52
(out)(err)
ped2.G.recomb5-0.20-13.wcnf O = N/A
T = TO
O = 97752
T = 24.75
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb5-0.20-14.wcnf O = N/A
T = TO
O = 64600
T = 32.76
(out)(err)
O = N/A
T = TO
(out)(err)
ped2.G.recomb5-0.20-15.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
ped3.D.recomb10-0.20-11.wcnf O = 690
T = 7.32
O = 690
T = 7.32
(out)(err)
O = 57346327
T = 69.19
(out)(err)
ped3.D.recomb10-0.20-12.wcnf O = 349
T = 3.95
O = 349
T = 3.95
(out)(err)
O = 59442118
T = 164.93
(out)(err)
ped3.D.recomb10-0.20-13.wcnf O = 350
T = 56.26
O = 350
T = 56.26
(out)(err)
O = 47358438
T = 178.68
(out)(err)
ped3.D.recomb10-0.20-14.wcnf O = 7
T = 5.58
O = 7
T = 5.58
(out)(err)
O = 41058803
T = 106.05
(out)(err)
ped3.D.recomb10-0.20-15.wcnf O = 689
T = 5.04
O = 689
T = 5.04
(out)(err)
O = 48419626
T = 81.91
(out)(err)
ped3.E.recomb10-0.20-11.wcnf O = 20869
T = 7.48
O = 20869
T = 7.48
(out)(err)
O = 563057235
T = 145.00
(out)(err)
ped3.E.recomb10-0.20-12.wcnf O = 20869
T = 37.15
O = 20869
T = 37.15
(out)(err)
O = 568705554
T = 233.66
(out)(err)
ped3.E.recomb10-0.20-13.wcnf O = 11647
T = 282.24
O = 11647
T = 282.24
(out)(err)
O = 499287846
T = 147.64
(out)(err)
ped3.E.recomb10-0.20-14.wcnf O = 19838
T = 8.07
O = 19838
T = 8.07
(out)(err)
O = 632477997
T = 139.37
(out)(err)
ped3.E.recomb10-0.20-15.wcnf O = 8570
T = 199.23
O = 8570
T = 199.23
(out)(err)
O = 546169178
T = 180.96
(out)(err)
ped3.F.recomb10-0.01-1.wcnf O = 14374
T = 5.23
O = 14374
T = 5.23
(out)(err)
O = 559646186
T = 123.94
(out)(err)
ped3.F.recomb10-0.01-2.wcnf O = 19832
T = 99.36
O = 19832
T = 99.36
(out)(err)
O = 499759421
T = 66.24
(out)(err)
ped3.F.recomb10-0.01-3.wcnf O = 8571
T = 5.51
O = 8571
T = 5.51
(out)(err)
O = 510793169
T = 83.29
(out)(err)
ped3.F.recomb10-0.01-4.wcnf O = 7207
T = 219.26
O = 7207
T = 219.26
(out)(err)
O = 484003165
T = 43.77
(out)(err)
ped3.F.recomb10-0.01-5.wcnf O = 9598
T = 216.89
O = 9598
T = 216.89
(out)(err)
O = 518675722
T = 58.28
(out)(err)
ped3.F.recomb10-0.10-10.wcnf O = 11304
T = 5.93
O = 11304
T = 5.93
(out)(err)
O = 621106688
T = 192.70
(out)(err)
ped3.F.recomb10-0.10-6.wcnf O = 8921
T = 7.19
O = 8921
T = 7.19
(out)(err)
O = 547031942
T = 92.94
(out)(err)
ped3.F.recomb10-0.10-7.wcnf O = 11654
T = 9.27
O = 11654
T = 9.27
(out)(err)
O = 537575663
T = 115.42
(out)(err)
ped3.F.recomb10-0.10-8.wcnf O = 20196
T = 7.06
O = 20196
T = 7.06
(out)(err)
O = 452492415
T = 192.49
(out)(err)
ped3.F.recomb10-0.10-9.wcnf O = 6871
T = 5.47
O = 6871
T = 5.47
(out)(err)
O = 479292958
T = 189.93
(out)(err)
ped3.F.recomb10-0.20-11.wcnf O = 9268
T = 178.71
O = 9268
T = 178.71
(out)(err)
O = 386301259
T = 179.14
(out)(err)
ped3.F.recomb10-0.20-12.wcnf O = 15406
T = 31.55
O = 15406
T = 31.55
(out)(err)
O = 365790478
T = 192.55
(out)(err)
ped3.F.recomb10-0.20-13.wcnf O = 2416
T = 44.89
O = 2416
T = 44.89
(out)(err)
O = 490313752
T = 207.73
(out)(err)
ped3.F.recomb10-0.20-14.wcnf O = 8234
T = 6.75
O = 8234
T = 6.75
(out)(err)
O = 405167776
T = 126.19
(out)(err)
ped3.F.recomb10-0.20-15.wcnf O = 8574
T = 132.40
O = 8574
T = 132.40
(out)(err)
O = 658931794
T = 194.73
(out)(err)
ped3.G.recomb10-0.01-1.wcnf O = 27022
T = 7.05
O = 27022
T = 7.05
(out)(err)
O = 7355
T = 225.63
(out)(err)
ped3.G.recomb10-0.01-2.wcnf O = 21572
T = 7.40
O = 21572
T = 7.40
(out)(err)
O = 984110
T = 174.22
(out)(err)
ped3.G.recomb10-0.01-3.wcnf O = 23955
T = 7.33
O = 23955
T = 7.33
(out)(err)
O = 1249890626
T = 233.52
(out)(err)
ped3.G.recomb10-0.01-4.wcnf O = 30775
T = 7.45
O = 30775
T = 7.45
(out)(err)
O = 8806
T = 222.20
(out)(err)
ped3.G.recomb10-0.01-5.wcnf O = 20207
T = 6.79
O = 20207
T = 6.79
(out)(err)
O = 1346523555
T = 238.63
(out)(err)
ped3.G.recomb10-0.10-10.wcnf O = 31133
T = 9.33
O = 31133
T = 9.33
(out)(err)
O = 925448212
T = 197.61
(out)(err)
ped3.G.recomb10-0.10-6.wcnf O = 29775
T = 7.67
O = 29775
T = 7.67
(out)(err)
O = 8599387
T = 217.12
(out)(err)
ped3.G.recomb10-0.10-7.wcnf O = 29758
T = 7.56
O = 29758
T = 7.56
(out)(err)
O = 991023561
T = 216.31
(out)(err)
ped3.G.recomb10-0.10-8.wcnf O = 28058
T = 98.09
O = 28058
T = 98.09
(out)(err)
O = 939196002
T = 225.44
(out)(err)
ped3.G.recomb10-0.10-9.wcnf O = 25325
T = 7.66
O = 25325
T = 7.66
(out)(err)
O = 91
T = 231.50
(out)(err)
ped3.G.recomb10-0.20-11.wcnf O = 22950
T = 196.33
O = 22950
T = 196.33
(out)(err)
O = 860005239
T = 205.88
(out)(err)
ped3.G.recomb10-0.20-12.wcnf O = 28411
T = 8.98
O = 28411
T = 8.98
(out)(err)
O = 1298170423
T = 211.13
(out)(err)
ped3.G.recomb10-0.20-13.wcnf O = 35588
T = 13.85
O = 35588
T = 13.85
(out)(err)
O = 870376430
T = 224.39
(out)(err)
ped3.G.recomb10-0.20-14.wcnf O = 24992
T = 9.76
O = 24992
T = 9.76
(out)(err)
O = 1139494922
T = 208.43
(out)(err)
ped3.G.recomb10-0.20-15.wcnf O = 28747
T = 9.09
O = 28747
T = 9.09
(out)(err)
O = 1015463719
T = 204.17
(out)(err)
comp01.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 31292
T = 14.86
(out)(err)
comp02.wcnf O = N/A
T = TO
O = 135
T = 284.41
(out)(err)
O = 1687811
T = 238.98
(out)(err)
comp03.wcnf O = N/A
T = TO
O = 349
T = 5.31
(out)(err)
O = 786258
T = 238.66
(out)(err)
comp04.wcnf O = N/A
T = TO
O = 66
T = 205.62
(out)(err)
O = 943924
T = 254.31
(out)(err)
comp05.wcnf O = N/A
T = TO
O = 1062
T = 5.30
(out)(err)
O = 2203447
T = 91.74
(out)(err)
comp06.wcnf O = N/A
T = TO
O = 247
T = 264.45
(out)(err)
O = 1684307
T = 238.06
(out)(err)
comp07.wcnf O = N/A
T = TO
O = 799
T = 244.25
(out)(err)
O = 502
T = 223.02
(out)(err)
comp08.wcnf O = N/A
T = TO
O = 91
T = 27.88
(out)(err)
O = 2190589
T = 242.70
(out)(err)
comp09.wcnf O = N/A
T = TO
O = 218
T = 248.04
(out)(err)
O = 1785767
T = 244.97
(out)(err)
comp10.wcnf O = N/A
T = TO
O = 190
T = 280.13
(out)(err)
O = 6901735
T = 230.33
(out)(err)
comp12.wcnf O = N/A
T = TO
O = 1299
T = 5.48
(out)(err)
O = 4462285
T = 234.81
(out)(err)
comp13.wcnf O = N/A
T = TO
O = 180
T = 77.46
(out)(err)
O = 1564936
T = 238.95
(out)(err)
comp14.wcnf O = N/A
T = TO
O = 138
T = 240.10
(out)(err)
O = 1536729
T = 238.94
(out)(err)
comp15.wcnf O = N/A
T = TO
O = 349
T = 5.68
(out)(err)
O = 718172
T = 234.76
(out)(err)
comp16.wcnf O = N/A
T = TO
O = 99
T = 221.97
(out)(err)
O = 7675777
T = 227.98
(out)(err)
comp17.wcnf O = N/A
T = TO
O = 280
T = 281.99
(out)(err)
O = 5870274
T = 238.99
(out)(err)
comp18.wcnf O = N/A
T = TO
O = 293
T = 5.25
(out)(err)
O = 708255
T = 111.16
(out)(err)
comp19.wcnf O = N/A
T = TO
O = 218
T = 32.86
(out)(err)
O = 1782698
T = 239.04
(out)(err)
comp20.wcnf O = N/A
T = TO
O = 544
T = 26.66
(out)(err)
O = 2500754
T = 238.00
(out)(err)
comp21.wcnf O = N/A
T = TO
O = 281
T = 166.27
(out)(err)
O = 57416
T = 239.44
(out)(err)
dds1.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
dds4.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
test1.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 66831
T = 27.72
(out)(err)
test2.wcnf O = N/A
T = TO
O = 274
T = 194.13
(out)(err)
O = 103615
T = 87.31
(out)(err)
test3.wcnf O = N/A
T = TO
O = 414
T = 161.46
(out)(err)
O = 456173
T = 237.67
(out)(err)
test4.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = 726685
T = 239.06
(out)(err)
mancoosi-test-i1000d0u98-0.wcnf O = 107076495
T = 45.51
O = 107076495
T = 45.51
(out)(err)
O = 68012273556
T = 148.36
(out)(err)
mancoosi-test-i1000d0u98-1.wcnf O = 122084955
T = 63.77
O = 122084955
T = 63.77
(out)(err)
O = 52008391880
T = 156.34
(out)(err)
mancoosi-test-i1000d0u98-10.wcnf O = 152083527
T = 34.20
O = 152083527
T = 34.20
(out)(err)
O = 18424944401
T = 97.55
(out)(err)
mancoosi-test-i1000d0u98-11.wcnf O = 122139402
T = 4.22
O = 122139402
T = 4.22
(out)(err)
O = 51662799212
T = 152.06
(out)(err)
mancoosi-test-i1000d0u98-12.wcnf O = 77077762
T = 249.64
O = 77077762
T = 249.64
(out)(err)
O = 35509978
T = 260.68
(out)(err)
mancoosi-test-i1000d0u98-13.wcnf O = 182245730
T = 6.81
O = 182245730
T = 6.81
(out)(err)
O = 84316232889
T = 150.33
(out)(err)
mancoosi-test-i1000d0u98-14.wcnf O = 137147806
T = 170.12
O = 137147806
T = 170.12
(out)(err)
O = 51513095810
T = 217.52
(out)(err)
mancoosi-test-i1000d0u98-15.wcnf O = 92031744
T = 23.87
O = 92031744
T = 23.87
(out)(err)
O = 51798474712
T = 123.65
(out)(err)
mancoosi-test-i1000d0u98-16.wcnf O = 137075245
T = 26.44
O = 137075245
T = 26.44
(out)(err)
O = 51888343070
T = 121.49
(out)(err)
mancoosi-test-i1000d0u98-17.wcnf O = 152192544
T = 98.36
O = 152192544
T = 98.36
(out)(err)
O = 84706651795
T = 243.00
(out)(err)
mancoosi-test-i1000d0u98-18.wcnf O = 152228825
T = 6.46
O = 152228825
T = 6.46
(out)(err)
O = 67621455055
T = 140.22
(out)(err)
mancoosi-test-i1000d0u98-19.wcnf O = 92049939
T = 47.26
O = 92049939
T = 47.26
(out)(err)
O = 18484487630
T = 151.92
(out)(err)
mancoosi-test-i1000d0u98-2.wcnf O = 77059701
T = 6.44
O = 77059701
T = 6.44
(out)(err)
O = 68282
T = 149.24
(out)(err)
mancoosi-test-i1000d0u98-20.wcnf O = 122103134
T = 278.08
O = 122103134
T = 278.08
(out)(err)
O = 84736378017
T = 124.29
(out)(err)
mancoosi-test-i1000d0u98-21.wcnf O = 77041487
T = 70.66
O = 77041487
T = 70.66
(out)(err)
O = 18514741284
T = 200.21
(out)(err)
mancoosi-test-i1000d0u98-22.wcnf O = 92086312
T = 35.39
O = 92086312
T = 35.39
(out)(err)
O = 51498232797
T = 156.91
(out)(err)
mancoosi-test-i1000d0u98-23.wcnf O = 62014822
T = 6.73
O = 62014822
T = 6.73
(out)(err)
O = 68312
T = 180.26
(out)(err)
mancoosi-test-i1000d0u98-24.wcnf O = 167273676
T = 32.64
O = 167273676
T = 32.64
(out)(err)
O = 51482715596
T = 182.40
(out)(err)
mancoosi-test-i1000d0u98-3.wcnf O = 91959146
T = 50.21
O = 91959146
T = 50.21
(out)(err)
O = 67967303338
T = 217.37
(out)(err)
mancoosi-test-i1000d0u98-4.wcnf O = 122175781
T = 8.99
O = 122175781
T = 8.99
(out)(err)
O = 67921896016
T = 216.74
(out)(err)
mancoosi-test-i1000d0u98-5.wcnf O = 107058295
T = 80.17
O = 107058295
T = 80.17
(out)(err)
O = 83895815318
T = 36.91
(out)(err)
mancoosi-test-i1000d0u98-6.wcnf O = 137093314
T = 7.14
O = 137093314
T = 7.14
(out)(err)
O = 51558339522
T = 104.44
(out)(err)
mancoosi-test-i1000d0u98-7.wcnf O = 92104395
T = 14.03
O = 92104395
T = 14.03
(out)(err)
O = 843915482
T = 93.25
(out)(err)
mancoosi-test-i1000d0u98-8.wcnf O = 137057008
T = 148.68
O = 137057008
T = 148.68
(out)(err)
O = 51618245
T = 208.31
(out)(err)
mancoosi-test-i1000d0u98-9.wcnf O = 167164758
T = 6.38
O = 167164758
T = 6.38
(out)(err)
O = 18379374068
T = 218.72
(out)(err)
mancoosi-test-i2000d0u98-25.wcnf O = 332548069
T = 154.03
O = 332548069
T = 154.03
(out)(err)
O = 224078437
T = 89.17
(out)(err)
mancoosi-test-i2000d0u98-26.wcnf O = 302513043
T = 142.14
O = 302513043
T = 142.14
(out)(err)
O = 255018186
T = 134.94
(out)(err)
mancoosi-test-i2000d0u98-27.wcnf O = 317557787
T = 279.34
O = 317557787
T = 279.34
(out)(err)
O = 66584748641
T = 99.49
(out)(err)
mancoosi-test-i2000d0u98-28.wcnf O = 287468291
T = 203.04
O = 287468291
T = 203.04
(out)(err)
O = 192747978917
T = 126.70
(out)(err)
mancoosi-test-i2000d0u98-29.wcnf O = 332675238
T = 278.10
O = 332675238
T = 278.10
(out)(err)
O = 35674761396
T = 232.21
(out)(err)
mancoosi-test-i2000d0u98-30.wcnf O = 212389892
T = 14.91
O = 212389892
T = 14.91
(out)(err)
O = 224243276002
T = 180.98
(out)(err)
mancoosi-test-i2000d0u98-31.wcnf O = 302585711
T = 159.75
O = 302585711
T = 159.75
(out)(err)
O = 192507935805
T = 95.21
(out)(err)
mancoosi-test-i2000d0u98-32.wcnf O = 422762096
T = 80.13
O = 422762096
T = 80.13
(out)(err)
O = 161267054
T = 217.35
(out)(err)
mancoosi-test-i2000d0u98-33.wcnf O = 347574599
T = 279.98
O = 347574599
T = 279.98
(out)(err)
O = 224123080905
T = 213.46
(out)(err)
mancoosi-test-i2000d0u98-34.wcnf O = 317448770
T = 261.07
O = 317448770
T = 261.07
(out)(err)
O = 2567
T = 228.94
(out)(err)
mancoosi-test-i2000d0u98-35.wcnf O = 407608342
T = 242.98
O = 407608342
T = 242.98
(out)(err)
O = 224198740860
T = 70.28
(out)(err)
mancoosi-test-i2000d0u98-36.wcnf O = 332566184
T = 6.19
O = 332566184
T = 6.19
(out)(err)
O = 192402859440
T = 83.28
(out)(err)
mancoosi-test-i2000d0u98-37.wcnf O = 437697880
T = 289.55
O = 437697880
T = 289.55
(out)(err)
O = 254897955323
T = 63.25
(out)(err)
mancoosi-test-i2000d0u98-38.wcnf O = 332620778
T = 83.84
O = 332620778
T = 83.84
(out)(err)
O = 1
T = 149.36
(out)(err)
mancoosi-test-i2000d0u98-39.wcnf O = 392636177
T = 256.11
O = 392636177
T = 256.11
(out)(err)
O = 129440810002
T = 98.07
(out)(err)
mancoosi-test-i2000d0u98-40.wcnf O = 197399502
T = 3.72
O = 197399502
T = 3.72
(out)(err)
O = 1
T = 204.13
(out)(err)
mancoosi-test-i2000d0u98-41.wcnf O = 422780296
T = 16.58
O = 422780296
T = 16.58
(out)(err)
O = 98020156146
T = 217.17
(out)(err)
mancoosi-test-i2000d0u98-42.wcnf O = 317539561
T = 213.09
O = 317539561
T = 213.09
(out)(err)
O = 129605921266
T = 220.99
(out)(err)
mancoosi-test-i2000d0u98-43.wcnf O = 242443033
T = 140.66
O = 242443033
T = 140.66
(out)(err)
O = 128479272192
T = 68.19
(out)(err)
mancoosi-test-i2000d0u98-44.wcnf O = 227380053
T = 57.88
O = 227380053
T = 57.88
(out)(err)
O = 160996486363
T = 157.76
(out)(err)
mancoosi-test-i2000d0u98-45.wcnf O = 227398249
T = 152.62
O = 227398249
T = 152.62
(out)(err)
O = 160019956980
T = 39.03
(out)(err)
mancoosi-test-i2000d0u98-46.wcnf O = 422707588
T = 244.68
O = 422707588
T = 244.68
(out)(err)
O = 129365895340
T = 238.13
(out)(err)
mancoosi-test-i2000d0u98-47.wcnf O = 332566202
T = 98.79
O = 332566202
T = 98.79
(out)(err)
O = 98275771762
T = 147.99
(out)(err)
mancoosi-test-i2000d0u98-48.wcnf O = 377773202
T = 82.34
O = 377773202
T = 82.34
(out)(err)
O = 98305751725
T = 222.94
(out)(err)
mancoosi-test-i2000d0u98-49.wcnf O = 212353539
T = 124.88
O = 212353539
T = 124.88
(out)(err)
O = 97929796878
T = 137.76
(out)(err)
mancoosi-test-i3000d0u98-50.wcnf O = 527911892
T = 287.14
O = 527911892
T = 287.14
(out)(err)
O = 283
T = 184.31
(out)(err)
mancoosi-test-i3000d0u98-51.wcnf O = 618162431
T = 226.96
O = 618162431
T = 226.96
(out)(err)
O = 191785768488
T = 139.74
(out)(err)
mancoosi-test-i3000d0u98-52.wcnf O = 798463185
T = 249.13
O = 798463185
T = 249.13
(out)(err)
O = 1907943
T = 85.64
(out)(err)
mancoosi-test-i3000d0u98-53.wcnf O = 588163614
T = 227.21
O = 588163614
T = 227.21
(out)(err)
O = 143475735873
T = 42.96
(out)(err)
mancoosi-test-i3000d0u98-54.wcnf O = 738429559
T = 273.62
O = 738429559
T = 273.62
(out)(err)
O = 144136906036
T = 145.87
(out)(err)
mancoosi-test-i3000d0u98-55.wcnf O = 542992950
T = 225.46
O = 542992950
T = 225.46
(out)(err)
O = 236610250984
T = 151.54
(out)(err)
mancoosi-test-i3000d0u98-56.wcnf O = 648160920
T = 76.46
O = 648160920
T = 76.46
(out)(err)
O = 2373471
T = 94.09
(out)(err)
mancoosi-test-i3000d0u98-57.wcnf O = 437806859
T = 278.52
O = 437806859
T = 278.52
(out)(err)
O = 19085
T = 91.16
(out)(err)
mancoosi-test-i3000d0u98-58.wcnf O = 648142814
T = 264.97
O = 648142814
T = 264.97
(out)(err)
O = 237467056655
T = 141.49
(out)(err)
mancoosi-test-i3000d0u98-59.wcnf O = 588127263
T = 257.03
O = 588127263
T = 257.03
(out)(err)
O = 97163895044
T = 89.93
(out)(err)
mancoosi-test-i3000d0u98-60.wcnf O = 768373654
T = 259.59
O = 768373654
T = 259.59
(out)(err)
O = 330496566741
T = 193.50
(out)(err)
mancoosi-test-i3000d0u98-61.wcnf O = 678323157
T = 180.47
O = 678323157
T = 180.47
(out)(err)
O = 9737434
T = 209.32
(out)(err)
mancoosi-test-i3000d0u98-62.wcnf O = 542956700
T = 190.08
O = 542956700
T = 190.08
(out)(err)
O = 97960177139
T = 90.35
(out)(err)
mancoosi-test-i3000d0u98-63.wcnf O = 528002753
T = 234.82
O = 528002753
T = 234.82
(out)(err)
O = 143896516802
T = 103.29
(out)(err)
mancoosi-test-i3000d0u98-64.wcnf O = 723257578
T = 213.99
O = 723257578
T = 213.99
(out)(err)
O = 283343235470
T = 222.32
(out)(err)
mancoosi-test-i3000d0u98-65.wcnf O = 738356811
T = 242.57
O = 738356811
T = 242.57
(out)(err)
O = 237421649746
T = 178.25
(out)(err)
mancoosi-test-i3000d0u98-66.wcnf O = 573046158
T = 273.96
O = 573046158
T = 273.96
(out)(err)
O = 470874970235
T = 145.86
(out)(err)
mancoosi-test-i3000d0u98-67.wcnf O = 678214110
T = 127.86
O = 678214110
T = 127.86
(out)(err)
O = 23761774029
T = 95.43
(out)(err)
mancoosi-test-i3000d0u98-68.wcnf O = 573064364
T = 283.63
O = 573064364
T = 283.63
(out)(err)
O = 330211024377
T = 189.02
(out)(err)
mancoosi-test-i3000d0u98-69.wcnf O = 813453413
T = 236.14
O = 813453413
T = 236.14
(out)(err)
O = 2839
T = 99.00
(out)(err)
mancoosi-test-i3000d0u98-70.wcnf O = 588163640
T = 251.71
O = 588163640
T = 251.71
(out)(err)
O = 144061991609
T = 95.53
(out)(err)
mancoosi-test-i3000d0u98-71.wcnf O = 482995744
T = 211.91
O = 482995744
T = 211.91
(out)(err)
O = 236911
T = 86.15
(out)(err)
mancoosi-test-i3000d0u98-72.wcnf O = 633043474
T = 122.00
O = 633043474
T = 122.00
(out)(err)
O = 236956134266
T = 167.86
(out)(err)
mancoosi-test-i3000d0u98-73.wcnf O = 648160983
T = 121.51
O = 648160983
T = 121.51
(out)(err)
O = 377770272684
T = 233.14
(out)(err)
mancoosi-test-i3000d0u98-74.wcnf O = 708376403
T = 3.85
O = 708376403
T = 3.85
(out)(err)
O = 144903316433
T = 100.25
(out)(err)
mancoosi-test-i4000d0u98-75.wcnf O = 963701214
T = 194.43
O = 963701214
T = 194.43
(out)(err)
O = 251907554841
T = 155.09
(out)(err)
mancoosi-test-i4000d0u98-76.wcnf O = 963810321
T = 149.83
O = 963810321
T = 149.83
(out)(err)
O = 621967314147
T = 153.89
(out)(err)
mancoosi-test-i4000d0u98-77.wcnf O = 993917895
T = 208.46
O = 993917895
T = 208.46
(out)(err)
O = 37463006
T = 160.85
(out)(err)
mancoosi-test-i4000d0u98-78.wcnf O = 1144092925
T = 211.40
O = 1144092925
T = 211.40
(out)(err)
O = 37805
T = 91.58
(out)(err)
mancoosi-test-i4000d0u98-79.wcnf O = 978854921
T = 4.53
O = 978854921
T = 4.53
(out)(err)
O = 4367
T = 162.89
(out)(err)
mancoosi-test-i4000d0u98-80.wcnf O = 1053915295
T = 222.74
O = 1053915295
T = 222.74
(out)(err)
O = 254327163
T = 79.46
(out)(err)
mancoosi-test-i4000d0u98-81.wcnf O = 1264360186
T = 223.84
O = 1264360186
T = 223.84
(out)(err)
O = 37572674728
T = 221.12
(out)(err)
mancoosi-test-i4000d0u98-82.wcnf O = 1174164208
T = 281.38
O = 1174164208
T = 281.38
(out)(err)
O = 375606443532
T = 160.61
(out)(err)
mancoosi-test-i4000d0u98-83.wcnf O = 1069032771
T = 54.04
O = 1069032771
T = 54.04
(out)(err)
O = 190103081502
T = 130.86
(out)(err)
mancoosi-test-i4000d0u98-84.wcnf O = 1069069040
T = 240.59
O = 1069069040
T = 240.59
(out)(err)
O = 376087331068
T = 181.82
(out)(err)
mancoosi-test-i4000d0u98-85.wcnf O = 903703949
T = 270.00
O = 903703949
T = 270.00
(out)(err)
O = 313727364494
T = 84.58
(out)(err)
mancoosi-test-i4000d0u98-86.wcnf O = 963773861
T = 92.62
O = 963773861
T = 92.62
(out)(err)
O = 250810922648
T = 50.30
(out)(err)
mancoosi-test-i4000d0u98-87.wcnf O = 1038852305
T = 278.58
O = 1038852305
T = 278.58
(out)(err)
O = 190478891409
T = 158.68
(out)(err)
mancoosi-test-i4000d0u98-88.wcnf O = 768428227
T = 24.49
O = 768428227
T = 24.49
(out)(err)
O = 2
T = 156.19
(out)(err)
mancoosi-test-i4000d0u98-89.wcnf O = 963791998
T = 254.13
O = 963791998
T = 254.13
(out)(err)
O = 374840487510
T = 96.85
(out)(err)
mancoosi-test-i4000d0u98-90.wcnf O = 858624129
T = 213.13
O = 858624129
T = 213.13
(out)(err)
O = 37
T = 87.30
(out)(err)
mancoosi-test-i4000d0u98-91.wcnf O = 1008889969
T = 100.80
O = 1008889969
T = 100.80
(out)(err)
O = 497
T = 82.68
(out)(err)
mancoosi-test-i4000d0u98-92.wcnf O = 723402935
T = 44.31
O = 723402935
T = 44.31
(out)(err)
O = 499019936243
T = 123.79
(out)(err)
mancoosi-test-i4000d0u98-93.wcnf O = 888640890
T = 25.88
O = 888640890
T = 25.88
(out)(err)
O = 18984775
T = 140.68
(out)(err)
mancoosi-test-i4000d0u98-94.wcnf O = 1084041090
T = 259.55
O = 1084041090
T = 259.55
(out)(err)
O = 375501
T = 177.34
(out)(err)
mancoosi-test-i4000d0u98-95.wcnf O = 1068996342
T = 39.64
O = 1068996342
T = 39.64
(out)(err)
O = 375
T = 104.96
(out)(err)
mancoosi-test-i4000d0u98-96.wcnf O = 1099031365
T = 241.93
O = 1099031365
T = 241.93
(out)(err)
O = 43658
T = 188.22
(out)(err)
mancoosi-test-i4000d0u98-97.wcnf O = 1159174032
T = 244.86
O = 1159174032
T = 244.86
(out)(err)
O = 3760
T = 183.84
(out)(err)
mancoosi-test-i4000d0u98-98.wcnf O = 1038834155
T = 227.04
O = 1038834155
T = 227.04
(out)(err)
O = 2523
T = 180.03
(out)(err)
mancoosi-test-i4000d0u98-99.wcnf O = 873650677
T = 39.95
O = 873650677
T = 39.95
(out)(err)
O = 313186298280
T = 194.32
(out)(err)