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 SAT4Jms-ext-i SAT4Jms-int-i optimax-it
CSG140-140-46.wcnf O = 16960
T = 5.64
O = 16960
T = 5.64
(out)(err)
O = 16960
T = 6.56
(out)(err)
O = 16960
T = 49.58
(out)(err)
CSG140-140-6.wcnf O = 52385
T = 4.54
O = 52385
T = 4.73
(out)(err)
O = 52385
T = 4.54
(out)(err)
O = 89960
T = 0.92
(out)(err)
CSG150-150-55.wcnf O = 27533
T = 77.83
O = 27533
T = 77.83
(out)(err)
O = 27533
T = 148.49
(out)(err)
O = 38104
T = 0.71
(out)(err)
CSG40-40-95.wcnf O = 8847
T = 0.09
O = 8847
T = 1.48
(out)(err)
O = 8847
T = 1.31
(out)(err)
O = 8847
T = 0.09
(out)(err)
CSG60-60-88.wcnf O = 7714
T = 0.04
O = 7714
T = 1.64
(out)(err)
O = 7714
T = 1.42
(out)(err)
O = 7714
T = 0.04
(out)(err)
CSGNaive140-140-0.wcnf O = 18185
T = 6.54
O = 18185
T = 6.54
(out)(err)
O = 18185
T = 6.76
(out)(err)
O = 18185
T = 18.66
(out)(err)
CSGNaive140-140-6.wcnf O = 56309
T = 4.74
O = 56309
T = 4.85
(out)(err)
O = 56309
T = 4.74
(out)(err)
O = 92402
T = 0.76
(out)(err)
CSGNaive150-150-55.wcnf O = 30495
T = 136.23
O = 30495
T = 136.23
(out)(err)
O = 30495
T = 173.52
(out)(err)
O = 39432
T = 0.74
(out)(err)
CSGNaive60-60-53.wcnf O = 9829
T = 0.49
O = 9829
T = 1.70
(out)(err)
O = 9829
T = 1.54
(out)(err)
O = 9829
T = 0.49
(out)(err)
CSGNaive70-70-91.wcnf O = 11177
T = 0.11
O = 11177
T = 1.81
(out)(err)
O = 11177
T = 1.59
(out)(err)
O = 11177
T = 0.11
(out)(err)
cat_paths_60_100_0000.txt.wcnf O = 70914
T = 69.27
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 70914
T = 69.27
(out)(err)
cat_paths_60_100_0001.txt.wcnf O = 80293
T = 0.10
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 80293
T = 0.10
(out)(err)
cat_paths_60_100_0002.txt.wcnf O = 64150
T = 33.60
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 64150
T = 33.60
(out)(err)
cat_paths_60_100_0003.txt.wcnf O = 70225
T = 10.17
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 70225
T = 10.17
(out)(err)
cat_paths_60_100_0004.txt.wcnf O = 73874
T = 0.07
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 73874
T = 0.07
(out)(err)
cat_paths_60_100_0005.txt.wcnf O = 59085
T = 15.12
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 59085
T = 15.12
(out)(err)
cat_paths_60_100_0006.txt.wcnf O = 62561
T = 36.76
O = 62561
T = 36.76
(out)(err)
O = 62561
T = 165.52
(out)(err)
O = 63181
T = 6.01
(out)(err)
cat_paths_60_100_0007.txt.wcnf O = 70380
T = 0.11
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 70380
T = 0.11
(out)(err)
cat_paths_60_110_0000.txt.wcnf O = 77325
T = 0.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 77325
T = 0.13
(out)(err)
cat_paths_60_110_0001.txt.wcnf O = 66944
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 66944
T = 0.08
(out)(err)
cat_paths_60_110_0002.txt.wcnf O = 70159
T = 41.49
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 70159
T = 41.49
(out)(err)
cat_paths_60_110_0003.txt.wcnf O = 86492
T = 0.12
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 86492
T = 0.12
(out)(err)
cat_paths_60_110_0004.txt.wcnf O = 65851
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 65851
T = 0.08
(out)(err)
cat_paths_60_110_0005.txt.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 88730
T = 0.08
(out)(err)
cat_paths_60_110_0006.txt.wcnf O = 77461
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 77461
T = 0.08
(out)(err)
cat_paths_60_110_0007.txt.wcnf O = 69737
T = 0.12
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 69737
T = 0.12
(out)(err)
cat_paths_60_120_0000.txt.wcnf O = 86740
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 86740
T = 0.09
(out)(err)
cat_paths_60_120_0001.txt.wcnf O = 76067
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 76067
T = 0.09
(out)(err)
cat_paths_60_120_0002.txt.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 83326
T = 0.09
(out)(err)
cat_paths_60_120_0003.txt.wcnf O = 83488
T = 0.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 83488
T = 0.13
(out)(err)
cat_paths_60_120_0004.txt.wcnf O = 85976
T = 0.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 85976
T = 0.13
(out)(err)
cat_paths_60_120_0005.txt.wcnf O = 90427
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 90427
T = 0.09
(out)(err)
cat_paths_60_120_0006.txt.wcnf O = 76768
T = 0.14
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 76768
T = 0.14
(out)(err)
cat_paths_60_120_0007.txt.wcnf O = 83451
T = 0.12
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 83451
T = 0.12
(out)(err)
cat_paths_60_130_0000.txt.wcnf O = 89648
T = 0.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 89648
T = 0.13
(out)(err)
cat_paths_60_130_0001.txt.wcnf O = 88056
T = 0.14
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 88056
T = 0.14
(out)(err)
cat_paths_60_130_0002.txt.wcnf O = 81339
T = 0.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 81339
T = 0.13
(out)(err)
cat_paths_60_130_0003.txt.wcnf O = 96148
T = 0.12
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 96148
T = 0.12
(out)(err)
cat_paths_60_130_0004.txt.wcnf O = 102226
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 102226
T = 0.09
(out)(err)
cat_paths_60_130_0005.txt.wcnf O = 86984
T = 0.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 86984
T = 0.13
(out)(err)
cat_paths_60_130_0006.txt.wcnf O = 88541
T = 0.07
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 88541
T = 0.07
(out)(err)
cat_paths_60_130_0007.txt.wcnf O = 83752
T = 0.11
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 83752
T = 0.11
(out)(err)
cat_paths_60_140_0000.txt.wcnf O = 113980
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 113980
T = 0.09
(out)(err)
cat_paths_60_140_0001.txt.wcnf O = 99272
T = 296.05
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 99272
T = 296.05
(out)(err)
cat_paths_60_140_0002.txt.wcnf O = 103409
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 103409
T = 0.08
(out)(err)
cat_paths_60_140_0003.txt.wcnf O = 95085
T = 154.06
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 95085
T = 154.06
(out)(err)
cat_paths_60_140_0004.txt.wcnf O = 110133
T = 0.10
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 110133
T = 0.10
(out)(err)
cat_paths_60_140_0005.txt.wcnf O = 114590
T = 0.12
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 114590
T = 0.12
(out)(err)
cat_paths_60_140_0006.txt.wcnf O = 109147
T = 0.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 109147
T = 0.13
(out)(err)
cat_paths_60_140_0007.txt.wcnf O = 97019
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 97019
T = 0.09
(out)(err)
cat_paths_60_150_0000.txt.wcnf O = 93103
T = 0.14
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 93103
T = 0.14
(out)(err)
cat_paths_60_150_0001.txt.wcnf O = 103265
T = 0.12
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 103265
T = 0.12
(out)(err)
cat_paths_60_150_0002.txt.wcnf O = 114979
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 114979
T = 0.08
(out)(err)
cat_paths_60_150_0003.txt.wcnf O = 120783
T = 0.03
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 120783
T = 0.03
(out)(err)
cat_paths_60_150_0004.txt.wcnf O = 106902
T = 0.07
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 106902
T = 0.07
(out)(err)
cat_paths_60_150_0005.txt.wcnf O = 125840
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 125840
T = 0.09
(out)(err)
cat_paths_60_150_0006.txt.wcnf O = 98796
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 98796
T = 0.09
(out)(err)
cat_paths_60_150_0007.txt.wcnf O = 126341
T = 0.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 126341
T = 0.13
(out)(err)
cat_paths_60_160_0000.txt.wcnf O = 119529
T = 0.10
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 119529
T = 0.10
(out)(err)
cat_paths_60_160_0001.txt.wcnf O = 115376
T = 0.11
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 115376
T = 0.11
(out)(err)
cat_paths_60_160_0002.txt.wcnf O = 116762
T = 0.10
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 116762
T = 0.10
(out)(err)
cat_paths_60_160_0003.txt.wcnf O = 117820
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 117820
T = 0.08
(out)(err)
cat_paths_60_160_0004.txt.wcnf O = 114441
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 114441
T = 0.08
(out)(err)
cat_paths_60_160_0005.txt.wcnf O = 135791
T = 0.12
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 135791
T = 0.12
(out)(err)
cat_paths_60_160_0006.txt.wcnf O = 107596
T = 0.14
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 107596
T = 0.14
(out)(err)
cat_paths_60_160_0007.txt.wcnf O = 117905
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 117905
T = 0.08
(out)(err)
cat_paths_60_170_0000.txt.wcnf O = 134546
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 134546
T = 0.08
(out)(err)
cat_paths_60_170_0003.txt.wcnf O = 136876
T = 0.11
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 136876
T = 0.11
(out)(err)
cat_paths_60_170_0004.txt.wcnf O = 106623
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 106623
T = 0.09
(out)(err)
cat_paths_60_170_0005.txt.wcnf O = 129781
T = 0.10
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 129781
T = 0.10
(out)(err)
cat_paths_60_170_0006.txt.wcnf O = 112978
T = 0.10
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 112978
T = 0.10
(out)(err)
cat_paths_60_170_0007.txt.wcnf O = 106476
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 106476
T = 0.08
(out)(err)
cat_paths_60_70_0000.txt.wcnf O = 48609
T = 4.41
O = 48609
T = 4.43
(out)(err)
O = 48609
T = 4.41
(out)(err)
O = 48609
T = 71.39
(out)(err)
cat_paths_60_70_0001.txt.wcnf O = 40870
T = 83.06
O = 40870
T = 83.06
(out)(err)
O = 40870
T = 98.14
(out)(err)
O = 40870
T = 283.03
(out)(err)
cat_paths_60_70_0002.txt.wcnf O = 38495
T = 3.05
O = 38495
T = 4.69
(out)(err)
O = 38495
T = 3.05
(out)(err)
O = 38495
T = 183.02
(out)(err)
cat_paths_60_70_0003.txt.wcnf O = 44555
T = 6.10
O = 44555
T = 6.10
(out)(err)
O = 44555
T = 7.84
(out)(err)
O = 44555
T = 134.93
(out)(err)
cat_paths_60_70_0004.txt.wcnf O = 33405
T = 4.18
O = 33405
T = 8.55
(out)(err)
O = 33405
T = 4.18
(out)(err)
O = 33405
T = 19.45
(out)(err)
cat_paths_60_70_0005.txt.wcnf O = 42222
T = 3.26
O = 42222
T = 5.68
(out)(err)
O = 42222
T = 3.26
(out)(err)
O = 42222
T = 196.28
(out)(err)
cat_paths_60_70_0006.txt.wcnf O = 44103
T = 12.53
O = 44103
T = 12.53
(out)(err)
O = 44103
T = 18.05
(out)(err)
O = 44103
T = 257.28
(out)(err)
cat_paths_60_70_0007.txt.wcnf O = 43384
T = 6.28
O = 43384
T = 6.28
(out)(err)
O = 43384
T = 14.87
(out)(err)
O = 43384
T = 100.72
(out)(err)
cat_paths_60_80_0000.txt.wcnf O = 46604
T = 23.71
O = 46604
T = 23.71
(out)(err)
O = 46604
T = 25.51
(out)(err)
O = 46604
T = 198.75
(out)(err)
cat_paths_60_80_0001.txt.wcnf O = 43891
T = 18.01
O = 43891
T = 18.01
(out)(err)
O = 43891
T = 19.60
(out)(err)
O = 43891
T = 293.33
(out)(err)
cat_paths_60_80_0002.txt.wcnf O = 45128
T = 9.59
O = 45128
T = 9.59
(out)(err)
O = 45128
T = 12.71
(out)(err)
O = 45128
T = 234.99
(out)(err)
cat_paths_60_80_0003.txt.wcnf O = 51870
T = 10.62
O = 51870
T = 22.68
(out)(err)
O = 51870
T = 10.62
(out)(err)
O = 51870
T = 45.50
(out)(err)
cat_paths_60_80_0004.txt.wcnf O = 46183
T = 4.93
O = 46183
T = 4.93
(out)(err)
O = 46183
T = 7.23
(out)(err)
O = 46183
T = 191.59
(out)(err)
cat_paths_60_80_0005.txt.wcnf O = 57352
T = 9.50
O = 57352
T = 12.53
(out)(err)
O = 57352
T = 9.50
(out)(err)
O = 57750
T = 257.16
(out)(err)
cat_paths_60_80_0006.txt.wcnf O = 54851
T = 17.23
O = 54851
T = 26.60
(out)(err)
O = 54851
T = 17.23
(out)(err)
O = 54851
T = 138.41
(out)(err)
cat_paths_60_80_0007.txt.wcnf O = 53183
T = 11.50
O = 53183
T = 18.04
(out)(err)
O = 53183
T = 11.50
(out)(err)
O = 53347
T = 122.00
(out)(err)
cat_paths_60_90_0000.txt.wcnf O = 51257
T = 158.10
O = 51257
T = 158.10
(out)(err)
O = N/A
T = TO
(out)(err)
O = 53676
T = 97.58
(out)(err)
cat_paths_60_90_0001.txt.wcnf O = 80527
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 80527
T = 0.09
(out)(err)
cat_paths_60_90_0002.txt.wcnf O = 66497
T = 27.14
O = 66497
T = 27.14
(out)(err)
O = 66497
T = 41.33
(out)(err)
O = 69436
T = 21.42
(out)(err)
cat_paths_60_90_0003.txt.wcnf O = 47163
T = 141.45
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 47163
T = 141.45
(out)(err)
cat_paths_60_90_0004.txt.wcnf O = 56174
T = 28.86
O = 56174
T = 28.86
(out)(err)
O = N/A
T = TO
(out)(err)
O = 65408
T = 0.13
(out)(err)
cat_paths_60_90_0005.txt.wcnf O = 76635
T = 0.12
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 76635
T = 0.12
(out)(err)
cat_paths_60_90_0006.txt.wcnf O = 47852
T = 195.85
O = 47852
T = 195.85
(out)(err)
O = N/A
T = TO
(out)(err)
O = 48559
T = 23.99
(out)(err)
cat_paths_60_90_0007.txt.wcnf O = 58739
T = 176.77
O = 58739
T = 176.77
(out)(err)
O = N/A
T = TO
(out)(err)
O = 60320
T = 119.84
(out)(err)
cat_sched_60_100_0000.txt.wcnf O = 114652
T = 1.93
O = 114652
T = 2.44
(out)(err)
O = 114652
T = 1.93
(out)(err)
O = 114652
T = 2.28
(out)(err)
cat_sched_60_100_0001.txt.wcnf O = 93703
T = 1.59
O = 93703
T = 1.89
(out)(err)
O = 93703
T = 1.59
(out)(err)
O = 93703
T = 1.83
(out)(err)
cat_sched_60_100_0002.txt.wcnf O = 132213
T = 1.75
O = 132213
T = 2.42
(out)(err)
O = 132213
T = 2.07
(out)(err)
O = 132213
T = 1.75
(out)(err)
cat_sched_60_100_0003.txt.wcnf O = 77536
T = 2.13
O = 77536
T = 2.21
(out)(err)
O = 77536
T = 2.13
(out)(err)
O = 77536
T = 14.36
(out)(err)
cat_sched_60_100_0004.txt.wcnf O = 60696
T = 0.44
O = 60696
T = 1.76
(out)(err)
O = 60696
T = 1.74
(out)(err)
O = 60696
T = 0.44
(out)(err)
cat_sched_60_100_0005.txt.wcnf O = 56308
T = 2.25
O = 56308
T = 2.76
(out)(err)
O = 56308
T = 2.25
(out)(err)
O = 56308
T = 5.60
(out)(err)
cat_sched_60_110_0000.txt.wcnf O = 82948
T = 2.33
O = 82948
T = 2.63
(out)(err)
O = 82948
T = 2.33
(out)(err)
O = 82948
T = 111.39
(out)(err)
cat_sched_60_110_0001.txt.wcnf O = 73693
T = 2.34
O = 73693
T = 2.76
(out)(err)
O = 73693
T = 2.34
(out)(err)
O = 73693
T = 32.35
(out)(err)
cat_sched_60_110_0002.txt.wcnf O = 80642
T = 2.29
O = 80642
T = 2.60
(out)(err)
O = 80642
T = 2.29
(out)(err)
O = 80642
T = 6.92
(out)(err)
cat_sched_60_110_0003.txt.wcnf O = 96555
T = 1.22
O = 96555
T = 2.89
(out)(err)
O = 96555
T = 2.64
(out)(err)
O = 96555
T = 1.22
(out)(err)
cat_sched_60_110_0004.txt.wcnf O = 79464
T = 1.57
O = 79464
T = 2.68
(out)(err)
O = 79464
T = 2.10
(out)(err)
O = 79464
T = 1.57
(out)(err)
cat_sched_60_110_0005.txt.wcnf O = 75228
T = 2.47
O = 75228
T = 2.61
(out)(err)
O = 75228
T = 2.47
(out)(err)
O = 75228
T = 48.81
(out)(err)
cat_sched_60_120_0000.txt.wcnf O = 94786
T = 2.24
O = 94786
T = 2.53
(out)(err)
O = 94786
T = 2.24
(out)(err)
O = 94786
T = 30.82
(out)(err)
cat_sched_60_120_0001.txt.wcnf O = 113216
T = 50.87
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 113216
T = 50.87
(out)(err)
cat_sched_60_120_0002.txt.wcnf O = 78795
T = 3.13
O = 78795
T = 3.13
(out)(err)
O = 78795
T = 3.27
(out)(err)
O = 78795
T = 154.86
(out)(err)
cat_sched_60_120_0003.txt.wcnf O = 101400
T = 2.45
O = 101400
T = 2.45
(out)(err)
O = 101400
T = 2.76
(out)(err)
O = 101400
T = 5.16
(out)(err)
cat_sched_60_120_0004.txt.wcnf O = 82385
T = 2.27
O = 82385
T = 2.82
(out)(err)
O = 82385
T = 2.27
(out)(err)
O = 82385
T = 41.31
(out)(err)
cat_sched_60_120_0005.txt.wcnf O = 170793
T = 2.50
O = 170793
T = 2.81
(out)(err)
O = 170793
T = 2.50
(out)(err)
O = 170793
T = 19.34
(out)(err)
cat_sched_60_130_0000.txt.wcnf O = 108599
T = 2.43
O = 108599
T = 2.43
(out)(err)
O = 108599
T = 2.54
(out)(err)
O = 108599
T = 43.29
(out)(err)
cat_sched_60_130_0001.txt.wcnf O = 71588
T = 2.14
O = 71588
T = 2.44
(out)(err)
O = 71588
T = 2.14
(out)(err)
O = 71588
T = 5.69
(out)(err)
cat_sched_60_130_0002.txt.wcnf O = 81955
T = 19.85
O = 81955
T = 19.85
(out)(err)
O = 81955
T = 41.30
(out)(err)
O = 81955
T = 79.59
(out)(err)
cat_sched_60_130_0003.txt.wcnf O = 161231
T = 2.27
O = 161231
T = 2.65
(out)(err)
O = 161231
T = 2.27
(out)(err)
O = 161231
T = 4.16
(out)(err)
cat_sched_60_130_0004.txt.wcnf O = 81678
T = 2.18
O = 81678
T = 2.47
(out)(err)
O = 81678
T = 2.18
(out)(err)
O = 81678
T = 28.47
(out)(err)
cat_sched_60_130_0005.txt.wcnf O = 137429
T = 2.47
O = 137429
T = 2.77
(out)(err)
O = 137429
T = 2.47
(out)(err)
O = 137429
T = 68.89
(out)(err)
cat_sched_60_140_0000.txt.wcnf O = 114104
T = 3.11
O = 114104
T = 3.11
(out)(err)
O = 114104
T = 3.15
(out)(err)
O = 114104
T = 157.07
(out)(err)
cat_sched_60_140_0001.txt.wcnf O = 122958
T = 3.18
O = 122958
T = 3.18
(out)(err)
O = 122958
T = 4.26
(out)(err)
O = 122958
T = 220.46
(out)(err)
cat_sched_60_140_0002.txt.wcnf O = 61273
T = 28.86
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 61273
T = 28.86
(out)(err)
cat_sched_60_140_0003.txt.wcnf O = 150048
T = 11.46
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 150048
T = 11.46
(out)(err)
cat_sched_60_140_0004.txt.wcnf O = 86193
T = 228.54
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 86193
T = 228.54
(out)(err)
cat_sched_60_140_0005.txt.wcnf O = 127199
T = 2.25
O = 127199
T = 2.46
(out)(err)
O = 127199
T = 2.25
(out)(err)
O = 127199
T = 16.88
(out)(err)
cat_sched_60_150_0000.txt.wcnf O = 137542
T = 1.60
O = 137542
T = 2.22
(out)(err)
O = 137542
T = 1.60
(out)(err)
O = 137542
T = 29.11
(out)(err)
cat_sched_60_150_0001.txt.wcnf O = 87430
T = 4.65
O = 87430
T = 4.74
(out)(err)
O = 87430
T = 4.65
(out)(err)
O = 87430
T = 197.32
(out)(err)
cat_sched_60_150_0002.txt.wcnf O = 50886
T = 2.24
O = 50886
T = 2.24
(out)(err)
O = 50886
T = 2.28
(out)(err)
O = 50886
T = 18.72
(out)(err)
cat_sched_60_150_0003.txt.wcnf O = 85895
T = 21.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 85895
T = 21.08
(out)(err)
cat_sched_60_150_0004.txt.wcnf O = 107684
T = 2.43
O = 107684
T = 2.43
(out)(err)
O = 107684
T = 2.49
(out)(err)
O = 107684
T = 36.29
(out)(err)
cat_sched_60_150_0005.txt.wcnf O = 153808
T = 50.67
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 153808
T = 50.67
(out)(err)
cat_sched_60_160_0000.txt.wcnf O = 42672
T = 2.55
O = 42672
T = 2.80
(out)(err)
O = 42672
T = 2.55
(out)(err)
O = 42672
T = 87.64
(out)(err)
cat_sched_60_160_0001.txt.wcnf O = 72012
T = 10.16
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 72012
T = 10.16
(out)(err)
cat_sched_60_160_0002.txt.wcnf O = 173386
T = 24.35
O = 173386
T = 24.35
(out)(err)
O = 173386
T = 54.77
(out)(err)
O = 173386
T = 295.00
(out)(err)
cat_sched_60_160_0003.txt.wcnf O = 118883
T = 2.45
O = 118883
T = 2.68
(out)(err)
O = 118883
T = 2.45
(out)(err)
O = 118883
T = 142.31
(out)(err)
cat_sched_60_160_0004.txt.wcnf O = 116193
T = 2.16
O = 116193
T = 2.40
(out)(err)
O = 116193
T = 2.16
(out)(err)
O = 116193
T = 14.95
(out)(err)
cat_sched_60_160_0005.txt.wcnf O = 117991
T = 29.81
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 117991
T = 29.81
(out)(err)
cat_sched_60_170_0000.txt.wcnf O = 128737
T = 97.72
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 128737
T = 97.72
(out)(err)
cat_sched_60_170_0001.txt.wcnf O = 62509
T = 24.99
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 62509
T = 24.99
(out)(err)
cat_sched_60_170_0002.txt.wcnf O = 64664
T = 51.36
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 64664
T = 51.36
(out)(err)
cat_sched_60_170_0003.txt.wcnf O = 169415
T = 132.06
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 169415
T = 132.06
(out)(err)
cat_sched_60_170_0004.txt.wcnf O = 132643
T = 287.46
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 132643
T = 287.46
(out)(err)
cat_sched_60_170_0005.txt.wcnf O = 207090
T = 191.59
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 207090
T = 191.59
(out)(err)
cat_sched_60_180_0000.txt.wcnf O = 112247
T = 36.65
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 112247
T = 36.65
(out)(err)
cat_sched_60_180_0001.txt.wcnf O = 154599
T = 9.85
O = 154599
T = 10.72
(out)(err)
O = 154599
T = 9.85
(out)(err)
O = 154741
T = 189.18
(out)(err)
cat_sched_60_180_0002.txt.wcnf O = 95338
T = 73.39
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 95338
T = 73.39
(out)(err)
cat_sched_60_180_0003.txt.wcnf O = 104416
T = 54.70
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 104416
T = 54.70
(out)(err)
cat_sched_60_180_0004.txt.wcnf O = 122528
T = 116.11
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 122528
T = 116.11
(out)(err)
cat_sched_60_180_0005.txt.wcnf O = 156974
T = 181.55
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 156974
T = 181.55
(out)(err)
cat_sched_60_190_0000.txt.wcnf O = 152878
T = 151.01
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 152878
T = 151.01
(out)(err)
cat_sched_60_190_0001.txt.wcnf O = 71734
T = 54.70
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 71734
T = 54.70
(out)(err)
cat_sched_60_190_0002.txt.wcnf O = 90578
T = 257.80
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 90578
T = 257.80
(out)(err)
cat_sched_60_190_0003.txt.wcnf O = 87812
T = 104.01
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 87812
T = 104.01
(out)(err)
cat_sched_60_190_0004.txt.wcnf O = 133679
T = 217.11
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 133679
T = 217.11
(out)(err)
cat_sched_60_190_0005.txt.wcnf O = 163576
T = 220.03
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 163576
T = 220.03
(out)(err)
cat_sched_60_200_0000.txt.wcnf O = 243050
T = 176.49
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 243050
T = 176.49
(out)(err)
cat_sched_60_200_0001.txt.wcnf O = 46823
T = 25.56
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 46823
T = 25.56
(out)(err)
cat_sched_60_200_0002.txt.wcnf O = 148415
T = 0.07
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 148415
T = 0.07
(out)(err)
cat_sched_60_200_0003.txt.wcnf O = 187461
T = 219.77
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 187461
T = 219.77
(out)(err)
cat_sched_60_200_0004.txt.wcnf O = 146974
T = 205.83
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 146974
T = 205.83
(out)(err)
cat_sched_60_200_0005.txt.wcnf O = 134394
T = 24.38
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 134394
T = 24.38
(out)(err)
cat_sched_60_70_0000.txt.wcnf O = 35750
T = 1.03
O = 35750
T = 1.26
(out)(err)
O = 35750
T = 1.03
(out)(err)
O = 35750
T = 1.71
(out)(err)
cat_sched_60_70_0001.txt.wcnf O = 83682
T = 0.34
O = 83682
T = 1.52
(out)(err)
O = 83682
T = 1.33
(out)(err)
O = 83682
T = 0.34
(out)(err)
cat_sched_60_70_0002.txt.wcnf O = 39227
T = 2.51
O = 39227
T = 2.77
(out)(err)
O = 39227
T = 2.51
(out)(err)
O = 39227
T = 6.73
(out)(err)
cat_sched_60_70_0003.txt.wcnf O = 61169
T = 0.12
O = 61169
T = 0.88
(out)(err)
O = 61169
T = 1.19
(out)(err)
O = 61169
T = 0.12
(out)(err)
cat_sched_60_70_0004.txt.wcnf O = 40136
T = 1.03
O = 40136
T = 1.17
(out)(err)
O = 40136
T = 1.44
(out)(err)
O = 40136
T = 1.03
(out)(err)
cat_sched_60_70_0005.txt.wcnf O = 105072
T = 1.47
O = 105072
T = 1.47
(out)(err)
O = 105072
T = 1.66
(out)(err)
O = 105072
T = 2.12
(out)(err)
cat_sched_60_80_0000.txt.wcnf O = 37448
T = 1.29
O = 37448
T = 1.59
(out)(err)
O = 37448
T = 1.29
(out)(err)
O = 37448
T = 2.09
(out)(err)
cat_sched_60_80_0001.txt.wcnf O = 22634
T = 0.08
O = 22634
T = 1.41
(out)(err)
O = 22634
T = 1.05
(out)(err)
O = 22634
T = 0.08
(out)(err)
cat_sched_60_80_0002.txt.wcnf O = 78029
T = 1.93
O = 78029
T = 2.86
(out)(err)
O = 78029
T = 1.93
(out)(err)
O = 78029
T = 2.50
(out)(err)
cat_sched_60_80_0003.txt.wcnf O = 40212
T = 1.96
O = 40212
T = 3.08
(out)(err)
O = 40212
T = 2.84
(out)(err)
O = 40212
T = 1.96
(out)(err)
cat_sched_60_80_0004.txt.wcnf O = 10390
T = 0.91
O = 10390
T = 1.81
(out)(err)
O = 10390
T = 1.79
(out)(err)
O = 10390
T = 0.91
(out)(err)
cat_sched_60_80_0005.txt.wcnf O = 34950
T = 1.64
O = 34950
T = 1.69
(out)(err)
O = 34950
T = 1.64
(out)(err)
O = 34950
T = 2.16
(out)(err)
cat_sched_60_90_0000.txt.wcnf O = 96833
T = 0.32
O = 96833
T = 1.53
(out)(err)
O = 96833
T = 1.44
(out)(err)
O = 96833
T = 0.32
(out)(err)
cat_sched_60_90_0001.txt.wcnf O = 82847
T = 0.25
O = 82847
T = 1.59
(out)(err)
O = 82847
T = 1.56
(out)(err)
O = 82847
T = 0.25
(out)(err)
cat_sched_60_90_0002.txt.wcnf O = 66464
T = 0.76
O = 66464
T = 1.64
(out)(err)
O = 66464
T = 1.49
(out)(err)
O = 66464
T = 0.76
(out)(err)
cat_sched_60_90_0003.txt.wcnf O = 37704
T = 0.20
O = 37704
T = 1.54
(out)(err)
O = 37704
T = 1.47
(out)(err)
O = 37704
T = 0.20
(out)(err)
cat_sched_60_90_0004.txt.wcnf O = 82537
T = 1.12
O = 82537
T = 1.12
(out)(err)
O = 82537
T = 1.50
(out)(err)
O = 82537
T = 8.59
(out)(err)
cat_sched_60_90_0005.txt.wcnf O = 49851
T = 0.96
O = 49851
T = 1.49
(out)(err)
O = 49851
T = 1.77
(out)(err)
O = 49851
T = 0.96
(out)(err)
bwt3cc.wcsp.wcnf O = 177
T = 0.00
O = 177
T = 0.29
(out)(err)
O = 177
T = 0.31
(out)(err)
O = 177
T = 0.00
(out)(err)
bwt4bc.wcsp.wcnf O = 355
T = 0.00
O = 355
T = 0.76
(out)(err)
O = 355
T = 0.81
(out)(err)
O = 355
T = 0.00
(out)(err)
bwt4c.wcsp.wcnf O = 600
T = 0.01
O = 600
T = 0.70
(out)(err)
O = 600
T = 0.64
(out)(err)
O = 600
T = 0.01
(out)(err)
bwt5ac.wcsp.wcnf O = 800
T = 0.05
O = 800
T = 1.75
(out)(err)
O = 800
T = 1.63
(out)(err)
O = 800
T = 0.05
(out)(err)
bwt5c.wcsp.wcnf O = 800
T = 0.03
O = 800
T = 1.24
(out)(err)
O = 800
T = 1.69
(out)(err)
O = 800
T = 0.03
(out)(err)
bwt5cc.wcsp.wcnf O = 866
T = 0.45
O = 866
T = 1.41
(out)(err)
O = 866
T = 1.70
(out)(err)
O = 866
T = 0.45
(out)(err)
bwt6.wcsp.wcnf O = 650
T = 0.03
O = 650
T = 1.46
(out)(err)
O = 650
T = 1.45
(out)(err)
O = 650
T = 0.03
(out)(err)
bwt7.wcsp.wcnf O = 780
T = 0.09
O = 780
T = 1.94
(out)(err)
O = 780
T = 1.88
(out)(err)
O = 780
T = 0.09
(out)(err)
depot01ac.wcsp.wcnf O = 1720
T = 0.00
O = 1720
T = 0.31
(out)(err)
O = 1720
T = 0.25
(out)(err)
O = 1720
T = 0.00
(out)(err)
depot01bc.wcsp.wcnf O = 1965
T = 0.01
O = 1965
T = 0.33
(out)(err)
O = 1965
T = 0.30
(out)(err)
O = 1965
T = 0.01
(out)(err)
depot01c.wcsp.wcnf O = 1720
T = 0.00
O = 1720
T = 0.30
(out)(err)
O = 1720
T = 0.30
(out)(err)
O = 1720
T = 0.00
(out)(err)
depot01cc.wcsp.wcnf O = 2142
T = 0.16
O = 2142
T = 0.33
(out)(err)
O = 2142
T = 0.27
(out)(err)
O = 2142
T = 0.16
(out)(err)
driverlog01c.wcsp.wcnf O = 1145
T = 0.00
O = 1145
T = 0.31
(out)(err)
O = 1145
T = 0.31
(out)(err)
O = 1145
T = 0.00
(out)(err)
driverlog01cc.wcsp.wcnf O = 1117
T = 0.00
O = 1117
T = 0.33
(out)(err)
O = 1117
T = 0.31
(out)(err)
O = 1117
T = 0.00
(out)(err)
driverlog02bc.wcsp.wcnf O = 2085
T = 2.55
O = 2085
T = 2.55
(out)(err)
O = 2085
T = 3.79
(out)(err)
O = 2085
T = 7.77
(out)(err)
driverlog02c.wcsp.wcnf O = 2010
T = 2.40
O = 2010
T = 2.62
(out)(err)
O = 2010
T = 4.15
(out)(err)
O = 2010
T = 2.40
(out)(err)
driverlog02cc.wcsp.wcnf O = 2428
T = 2.16
O = 2428
T = 2.16
(out)(err)
O = 2428
T = 2.29
(out)(err)
O = 2522
T = 253.03
(out)(err)
driverlog04ac.wcsp.wcnf O = 1790
T = 2.11
O = 1790
T = 2.34
(out)(err)
O = 1790
T = 3.17
(out)(err)
O = 1790
T = 2.11
(out)(err)
driverlog04bc.wcsp.wcnf O = 1921
T = 2.32
O = 1921
T = 2.36
(out)(err)
O = 1921
T = 2.32
(out)(err)
O = 1921
T = 5.28
(out)(err)
driverlog04cc.wcsp.wcnf O = 2932
T = 2.56
O = 2932
T = 2.57
(out)(err)
O = 2932
T = 2.56
(out)(err)
O = 3384
T = 0.07
(out)(err)
driverlog05ac.wcsp.wcnf O = 1350
T = 3.18
O = 1350
T = 3.23
(out)(err)
O = 1350
T = 3.18
(out)(err)
O = 1350
T = 4.47
(out)(err)
driverlog05bc.wcsp.wcnf O = 1344
T = 2.85
O = 1344
T = 2.85
(out)(err)
O = 1344
T = 3.03
(out)(err)
O = 1344
T = 9.03
(out)(err)
driverlog05c.wcsp.wcnf O = 1350
T = 2.54
O = 1350
T = 3.16
(out)(err)
O = 1350
T = 2.54
(out)(err)
O = 1350
T = 3.29
(out)(err)
driverlog08ac.wcsp.wcnf O = 2220
T = 2.31
O = 2220
T = 2.31
(out)(err)
O = 2220
T = 2.59
(out)(err)
O = 2220
T = 11.98
(out)(err)
driverlog08c.wcsp.wcnf O = 2220
T = 2.55
O = 2220
T = 2.65
(out)(err)
O = 2220
T = 2.55
(out)(err)
O = 2220
T = 11.95
(out)(err)
driverlog08cc.wcsp.wcnf O = 4052
T = 2.96
O = 4052
T = 3.27
(out)(err)
O = 4052
T = 2.96
(out)(err)
O = 4995
T = 0.10
(out)(err)
driverlog09.wcsp.wcnf O = 960
T = 1.66
O = 960
T = 2.93
(out)(err)
O = 960
T = 2.70
(out)(err)
O = 960
T = 1.66
(out)(err)
driverlogs03.wcsp.wcnf O = 1225
T = 0.33
O = 1225
T = 2.62
(out)(err)
O = 1225
T = 2.70
(out)(err)
O = 1225
T = 0.33
(out)(err)
driverlogs06.wcsp.wcnf O = 1055
T = 0.19
O = 1055
T = 2.24
(out)(err)
O = 1055
T = 1.95
(out)(err)
O = 1055
T = 0.19
(out)(err)
logistics01bc.wcsp.wcnf O = 8035
T = 0.10
O = 8035
T = 1.06
(out)(err)
O = 8035
T = 0.84
(out)(err)
O = 8035
T = 0.10
(out)(err)
logistics01c.wcsp.wcnf O = 8865
T = 0.07
O = 8865
T = 0.77
(out)(err)
O = 8865
T = 0.99
(out)(err)
O = 8865
T = 0.07
(out)(err)
logistics01cc.wcsp.wcnf O = 4282
T = 0.30
O = 4282
T = 0.94
(out)(err)
O = 4282
T = 1.08
(out)(err)
O = 4282
T = 0.30
(out)(err)
mprime01ac.wcsp.wcnf O = 250
T = 0.06
O = 250
T = 1.79
(out)(err)
O = 250
T = 1.79
(out)(err)
O = 250
T = 0.06
(out)(err)
mprime01bc.wcsp.wcnf O = 284
T = 0.50
O = 284
T = 1.91
(out)(err)
O = 284
T = 1.74
(out)(err)
O = 284
T = 0.50
(out)(err)
mprime01cc.wcsp.wcnf O = 603
T = 0.87
O = 603
T = 1.47
(out)(err)
O = 603
T = 1.69
(out)(err)
O = 603
T = 0.87
(out)(err)
mprime03ac.wcsp.wcnf O = 320
T = 0.00
O = 320
T = 0.30
(out)(err)
O = 320
T = 0.29
(out)(err)
O = 320
T = 0.00
(out)(err)
mprime03bc.wcsp.wcnf O = 380
T = 0.00
O = 380
T = 0.28
(out)(err)
O = 380
T = 0.28
(out)(err)
O = 380
T = 0.00
(out)(err)
mprime03c.wcsp.wcnf O = 320
T = 0.00
O = 320
T = 0.31
(out)(err)
O = 320
T = 0.29
(out)(err)
O = 320
T = 0.00
(out)(err)
mprime04bc.wcsp.wcnf O = 600
T = 0.06
O = 600
T = 1.63
(out)(err)
O = 600
T = 1.85
(out)(err)
O = 600
T = 0.06
(out)(err)
mprime04c.wcsp.wcnf O = 590
T = 0.04
O = 590
T = 1.78
(out)(err)
O = 590
T = 1.84
(out)(err)
O = 590
T = 0.04
(out)(err)
mprime04cc.wcsp.wcnf O = 931
T = 0.08
O = 931
T = 1.26
(out)(err)
O = 931
T = 1.47
(out)(err)
O = 931
T = 0.08
(out)(err)
rovers02ac.wcsp.wcnf O = 1660
T = 0.08
O = 1660
T = 1.06
(out)(err)
O = 1660
T = 1.05
(out)(err)
O = 1660
T = 0.08
(out)(err)
rovers02c.wcsp.wcnf O = 1660
T = 0.06
O = 1660
T = 1.04
(out)(err)
O = 1660
T = 0.98
(out)(err)
O = 1660
T = 0.06
(out)(err)
rovers02cc.wcsp.wcnf O = 1668
T = 0.82
O = 1668
T = 1.10
(out)(err)
O = 1668
T = 0.98
(out)(err)
O = 1668
T = 0.82
(out)(err)
satellite01ac.wcsp.wcnf O = 1530
T = 0.15
O = 1530
T = 1.09
(out)(err)
O = 1530
T = 0.97
(out)(err)
O = 1530
T = 0.15
(out)(err)
satellite01bc.wcsp.wcnf O = 1827
T = 0.25
O = 1827
T = 1.28
(out)(err)
O = 1827
T = 1.07
(out)(err)
O = 1827
T = 0.25
(out)(err)
satellite01cc.wcsp.wcnf O = 1530
T = 0.16
O = 1530
T = 0.83
(out)(err)
O = 1530
T = 0.96
(out)(err)
O = 1530
T = 0.16
(out)(err)
satellite02ac.wcsp.wcnf O = 1611
T = 3.38
O = 1611
T = 3.38
(out)(err)
O = 1611
T = 3.69
(out)(err)
O = 1611
T = 9.29
(out)(err)
satellite02bc.wcsp.wcnf O = 2289
T = 4.60
O = 2289
T = 5.00
(out)(err)
O = 2289
T = 4.60
(out)(err)
O = 2289
T = 26.83
(out)(err)
zenotravel02ac.wcsp.wcnf O = 2485
T = 0.01
O = 2485
T = 1.03
(out)(err)
O = 2485
T = 0.98
(out)(err)
O = 2485
T = 0.01
(out)(err)
zenotravel02bc.wcsp.wcnf O = 2335
T = 0.01
O = 2335
T = 1.10
(out)(err)
O = 2335
T = 1.03
(out)(err)
O = 2335
T = 0.01
(out)(err)
zenotravel02c.wcsp.wcnf O = 2485
T = 0.01
O = 2485
T = 1.05
(out)(err)
O = 2485
T = 0.96
(out)(err)
O = 2485
T = 0.01
(out)(err)
zenotravel02cc.wcsp.wcnf O = 742
T = 0.04
O = 742
T = 0.81
(out)(err)
O = 742
T = 0.85
(out)(err)
O = 742
T = 0.04
(out)(err)
zenotravel04bc.wcsp.wcnf O = 4110
T = 0.39
O = 4110
T = 1.88
(out)(err)
O = 4110
T = 1.78
(out)(err)
O = 4110
T = 0.39
(out)(err)
zenotravel04c.wcsp.wcnf O = 4270
T = 0.17
O = 4270
T = 1.86
(out)(err)
O = 4270
T = 1.51
(out)(err)
O = 4270
T = 0.17
(out)(err)
zenotravel04cc.wcsp.wcnf O = 1599
T = 1.69
O = 1599
T = 1.69
(out)(err)
O = 1599
T = 1.85
(out)(err)
O = 1599
T = 4.30
(out)(err)
cap101.wcsp.wcnf O = 10209650
T = 13.30
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 10209650
T = 13.30
(out)(err)
cap102.wcsp.wcnf O = 9681952
T = 52.42
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 9681952
T = 52.42
(out)(err)
cap111.wcsp.wcnf O = 22625591
T = 0.01
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 22625591
T = 0.01
(out)(err)
cap112.wcsp.wcnf O = 22675591
T = 0.01
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 22675591
T = 0.01
(out)(err)
cap121.wcsp.wcnf O = 22625591
T = 0.01
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 22625591
T = 0.01
(out)(err)
cap122.wcsp.wcnf O = 22675591
T = 0.01
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 22675591
T = 0.01
(out)(err)
cap131.wcsp.wcnf O = 22625591
T = 0.02
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 22625591
T = 0.02
(out)(err)
cap132.wcsp.wcnf O = 22675591
T = 0.02
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 22675591
T = 0.02
(out)(err)
cap61.wcsp.wcnf O = 10926308
T = 2.31
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 10926308
T = 2.31
(out)(err)
cap62.wcsp.wcnf O = 11014951
T = 2.51
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 11014951
T = 2.51
(out)(err)
cap71.wcsp.wcnf O = 10926308
T = 1.80
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 10926308
T = 1.80
(out)(err)
cap72.wcsp.wcnf O = 11014951
T = 2.47
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 11014951
T = 2.47
(out)(err)
cap81.wcsp.wcnf O = 10209650
T = 14.38
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 10209650
T = 14.38
(out)(err)
cap82.wcsp.wcnf O = 9681952
T = 55.26
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 9681952
T = 55.26
(out)(err)
cap91.wcsp.wcnf O = 10209650
T = 13.63
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 10209650
T = 13.63
(out)(err)
cap92.wcsp.wcnf O = 9681952
T = 52.00
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 9681952
T = 52.00
(out)(err)
warehouse0.wcsp.wcnf O = 328
T = 0.65
O = 328
T = 0.69
(out)(err)
O = 328
T = 0.77
(out)(err)
O = 328
T = 0.65
(out)(err)
warehouse1.wcsp.wcnf O = 730997
T = 86.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 730997
T = 86.13
(out)(err)
normalized-mps-v2-20-10-bm23.opb.msat.wcnf O = 34
T = 5.12
O = 34
T = 5.71
(out)(err)
O = 34
T = 5.76
(out)(err)
O = 34
T = 5.12
(out)(err)
normalized-mps-v2-20-10-cracpb1.opb.msat.wcnf O = 45034
T = 21.22
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 45034
T = 21.22
(out)(err)
normalized-mps-v2-20-10-l152lav.opb.msat.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
normalized-mps-v2-20-10-lp4l.opb.msat.wcnf O = 4184
T = 1.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 4184
T = 1.08
(out)(err)
normalized-mps-v2-20-10-lseu.opb.msat.wcnf O = 1755
T = 0.06
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1755
T = 0.06
(out)(err)
normalized-mps-v2-20-10-mod008.opb.msat.wcnf O = 559
T = 4.92
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 559
T = 4.92
(out)(err)
normalized-mps-v2-20-10-mod010.opb.msat.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
normalized-mps-v2-20-10-p0033.opb.msat.wcnf O = 3089
T = 0.72
O = 3089
T = 1.15
(out)(err)
O = 3089
T = 1.09
(out)(err)
O = 3089
T = 0.72
(out)(err)
normalized-mps-v2-20-10-p0040.opb.msat.wcnf O = 62027
T = 3.95
O = 62027
T = 3.95
(out)(err)
O = 62027
T = 4.48
(out)(err)
O = 63311
T = 2.09
(out)(err)
normalized-mps-v2-20-10-p0201.opb.msat.wcnf O = 1684
T = 9.60
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1684
T = 9.60
(out)(err)
normalized-mps-v2-20-10-p0548.opb.msat.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
normalized-mps-v2-20-10-sentoy.opb.msat.wcnf O = 3733
T = 3.16
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 3733
T = 3.16
(out)(err)
random-net-100-2_network-10.net.wcnf O = 104596
T = 140.90
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 104596
T = 140.90
(out)(err)
random-net-100-2_network-3.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 110001
T = 80.36
(out)(err)
random-net-100-2_network-5.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-100-2_network-6.net.wcnf O = 113504
T = 284.75
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 113504
T = 284.75
(out)(err)
random-net-100-2_network-8.net.wcnf O = 203247
T = 0.10
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 203247
T = 0.10
(out)(err)
random-net-100-2_network-9.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 113292
T = 35.12
(out)(err)
random-net-200-1_network-1.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 183178
T = 26.21
(out)(err)
random-net-200-1_network-10.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-200-1_network-3.net.wcnf O = 404735
T = 0.07
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 404735
T = 0.07
(out)(err)
random-net-200-1_network-4.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-200-1_network-5.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-200-1_network-6.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 192824
T = 72.76
(out)(err)
random-net-200-1_network-7.net.wcnf O = 196443
T = 16.34
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 196443
T = 16.34
(out)(err)
random-net-200-1_network-8.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-200-1_network-9.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-240-1_network-1.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 242058
T = 149.30
(out)(err)
random-net-240-1_network-10.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 242078
T = 88.90
(out)(err)
random-net-240-1_network-2.net.wcnf O = 446933
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 446933
T = 0.09
(out)(err)
random-net-240-1_network-3.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-240-1_network-4.net.wcnf O = 438424
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 438424
T = 0.08
(out)(err)
random-net-240-1_network-5.net.wcnf O = 465492
T = 0.11
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 465492
T = 0.11
(out)(err)
random-net-240-1_network-6.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 252086
T = 117.75
(out)(err)
random-net-240-1_network-7.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-240-1_network-8.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 452422
T = 0.10
(out)(err)
random-net-240-1_network-9.net.wcnf O = 450558
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 450558
T = 0.08
(out)(err)
random-net-280-1_network-10.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-280-1_network-2.net.wcnf O = 526007
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 526007
T = 0.08
(out)(err)
random-net-280-1_network-3.net.wcnf O = 516348
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 516348
T = 0.09
(out)(err)
random-net-280-1_network-4.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-280-1_network-5.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-280-1_network-6.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 509062
T = 0.08
(out)(err)
random-net-280-1_network-7.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 531358
T = 0.10
(out)(err)
random-net-280-1_network-8.net.wcnf O = 574041
T = 0.13
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 574041
T = 0.13
(out)(err)
random-net-280-1_network-9.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-300-1_network-1.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 610452
T = 0.11
(out)(err)
random-net-300-1_network-10.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-300-1_network-2.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 548960
T = 0.12
(out)(err)
random-net-300-1_network-3.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 294336
T = 99.57
(out)(err)
random-net-300-1_network-4.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 580258
T = 0.10
(out)(err)
random-net-300-1_network-5.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 534630
T = 0.09
(out)(err)
random-net-300-1_network-6.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-300-1_network-7.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-300-1_network-8.net.wcnf O = 524778
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 524778
T = 0.09
(out)(err)
random-net-300-1_network-9.net.wcnf O = 539975
T = 0.09
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 539975
T = 0.09
(out)(err)
random-net-50-2_network-1.net.wcnf O = 52029
T = 2.60
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 52029
T = 2.60
(out)(err)
random-net-50-2_network-10.net.wcnf O = 50793
T = 7.73
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 50793
T = 7.73
(out)(err)
random-net-50-2_network-2.net.wcnf O = 53792
T = 8.34
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 53792
T = 8.34
(out)(err)
random-net-50-2_network-3.net.wcnf O = 51361
T = 45.63
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 51361
T = 45.63
(out)(err)
random-net-50-2_network-4.net.wcnf O = 51388
T = 2.25
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 51388
T = 2.25
(out)(err)
random-net-50-2_network-5.net.wcnf O = 57553
T = 26.42
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 57553
T = 26.42
(out)(err)
random-net-50-2_network-6.net.wcnf O = 115892
T = 0.08
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 115892
T = 0.08
(out)(err)
random-net-50-2_network-7.net.wcnf O = 54454
T = 3.62
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 54454
T = 3.62
(out)(err)
random-net-50-2_network-8.net.wcnf O = 59349
T = 0.96
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 59349
T = 0.96
(out)(err)
random-net-50-2_network-9.net.wcnf O = 57258
T = 6.96
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 57258
T = 6.96
(out)(err)
random-net-60-2_network-1.net.wcnf O = 60912
T = 6.32
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 60912
T = 6.32
(out)(err)
random-net-60-2_network-10.net.wcnf O = 62284
T = 24.26
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 62284
T = 24.26
(out)(err)
random-net-60-2_network-2.net.wcnf O = 76511
T = 12.36
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 76511
T = 12.36
(out)(err)
random-net-60-2_network-3.net.wcnf O = 62916
T = 143.83
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 62916
T = 143.83
(out)(err)
random-net-60-2_network-4.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 60755
T = 40.58
(out)(err)
random-net-60-2_network-5.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 77757
T = 102.91
(out)(err)
random-net-60-2_network-6.net.wcnf O = 64321
T = 14.66
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 64321
T = 14.66
(out)(err)
random-net-60-2_network-7.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 62526
T = 54.16
(out)(err)
random-net-60-2_network-8.net.wcnf O = 55639
T = 13.42
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 55639
T = 13.42
(out)(err)
random-net-60-2_network-9.net.wcnf O = 64417
T = 27.07
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 64417
T = 27.07
(out)(err)
random-net-80-2_network-1.net.wcnf O = 78355
T = 111.81
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 78355
T = 111.81
(out)(err)
random-net-80-2_network-10.net.wcnf O = 87397
T = 21.66
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 87397
T = 21.66
(out)(err)
random-net-80-2_network-2.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 87699
T = 49.17
(out)(err)
random-net-80-2_network-3.net.wcnf O = 85379
T = 231.16
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 85379
T = 231.16
(out)(err)
random-net-80-2_network-4.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 91980
T = 19.96
(out)(err)
random-net-80-2_network-5.net.wcnf O = 88891
T = 15.11
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 88891
T = 15.11
(out)(err)
random-net-80-2_network-6.net.wcnf O = N/A
T = TO
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
random-net-80-2_network-7.net.wcnf O = 90468
T = 17.38
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 90468
T = 17.38
(out)(err)
random-net-80-2_network-8.net.wcnf O = 164103
T = 0.11
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 164103
T = 0.11
(out)(err)
random-net-80-2_network-9.net.wcnf O = 81119
T = 5.69
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 81119
T = 5.69
(out)(err)