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
file_rwpms_wcnf_L2_V150_C4000_H150_0.wcnf O = 4231
T = 6.18
O = 4619
T = 4.70
(out)(err)
O = 4231
T = 6.18
(out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_1.wcnf O = 26218
T = 10.11
O = N/A
T = TO
(out)(err)
O = 26218
T = 10.11
(out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_2.wcnf O = 4235
T = 1.73
O = 4857
T = 4.31
(out)(err)
O = 4235
T = 1.73
(out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_3.wcnf O = 4037
T = 10.37
O = 4841
T = 2.01
(out)(err)
O = 4037
T = 10.37
(out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_4.wcnf O = 4031
T = 10.21
O = 4873
T = 7.83
(out)(err)
O = 4031
T = 10.21
(out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_5.wcnf O = 4144
T = 11.20
O = 4930
T = 7.56
(out)(err)
O = 4144
T = 11.20
(out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_6.wcnf O = 4149
T = 8.59
O = 4934
T = 3.07
(out)(err)
O = 4149
T = 8.59
(out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_7.wcnf O = 4043
T = 9.80
O = 4789
T = 7.56
(out)(err)
O = 4043
T = 9.80
(out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_8.wcnf O = 4078
T = 10.09
O = 4896
T = 5.93
(out)(err)
O = 4078
T = 10.09
(out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_9.wcnf O = 4328
T = 8.67
O = 4963
T = 3.91
(out)(err)
O = 4328
T = 8.67
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_0.wcnf O = 4572
T = 7.86
O = 5484
T = 3.74
(out)(err)
O = 4572
T = 7.86
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_1.wcnf O = 4967
T = 17.12
O = 5669
T = 4.45
(out)(err)
O = 4967
T = 17.12
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_2.wcnf O = 4961
T = 16.77
O = 5845
T = 5.92
(out)(err)
O = 4961
T = 16.77
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_3.wcnf O = 4614
T = 8.93
O = 5572
T = 4.24
(out)(err)
O = 4614
T = 8.93
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_4.wcnf O = 4794
T = 14.08
O = 5473
T = 5.19
(out)(err)
O = 4794
T = 14.08
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_5.wcnf O = 4687
T = 15.17
O = 5640
T = 2.74
(out)(err)
O = 4687
T = 15.17
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_6.wcnf O = 4605
T = 12.20
O = 5589
T = 5.88
(out)(err)
O = 4605
T = 12.20
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_7.wcnf O = 4710
T = 11.48
O = 5624
T = 3.27
(out)(err)
O = 4710
T = 11.48
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_8.wcnf O = 4945
T = 13.03
O = 5552
T = 9.15
(out)(err)
O = 4945
T = 13.03
(out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_9.wcnf O = 5023
T = 8.32
O = 5477
T = 1.84
(out)(err)
O = 5023
T = 8.32
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_0.wcnf O = 5362
T = 8.06
O = 6138
T = 4.23
(out)(err)
O = 5362
T = 8.06
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_1.wcnf O = 5338
T = 13.27
O = 6414
T = 4.50
(out)(err)
O = 5338
T = 13.27
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_2.wcnf O = 5312
T = 11.04
O = 6217
T = 7.33
(out)(err)
O = 5312
T = 11.04
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_3.wcnf O = 5507
T = 8.61
O = 6537
T = 3.78
(out)(err)
O = 5507
T = 8.61
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_4.wcnf O = 5451
T = 6.13
O = 6448
T = 3.78
(out)(err)
O = 5451
T = 6.13
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_5.wcnf O = 5308
T = 14.23
O = 6133
T = 4.81
(out)(err)
O = 5308
T = 14.23
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_6.wcnf O = 5428
T = 11.12
O = 6142
T = 4.35
(out)(err)
O = 5428
T = 11.12
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_7.wcnf O = 5468
T = 9.87
O = 6142
T = 6.24
(out)(err)
O = 5468
T = 9.87
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_8.wcnf O = 5339
T = 8.52
O = 6046
T = 2.90
(out)(err)
O = 5339
T = 8.52
(out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_9.wcnf O = 5376
T = 9.37
O = 6368
T = 2.52
(out)(err)
O = 5376
T = 9.37
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_0.wcnf O = 626
T = 10.30
O = 758
T = 5.89
(out)(err)
O = 626
T = 10.30
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_1.wcnf O = 745
T = 9.25
O = 968
T = 6.00
(out)(err)
O = 745
T = 9.25
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_2.wcnf O = 629
T = 6.77
O = 746
T = 2.36
(out)(err)
O = 629
T = 6.77
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_3.wcnf O = 723
T = 7.90
O = 903
T = 1.85
(out)(err)
O = 723
T = 7.90
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_4.wcnf O = 737
T = 8.67
O = 907
T = 5.23
(out)(err)
O = 737
T = 8.67
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_5.wcnf O = 668
T = 9.10
O = 723
T = 5.25
(out)(err)
O = 668
T = 9.10
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_6.wcnf O = 641
T = 9.52
O = 801
T = 2.41
(out)(err)
O = 641
T = 9.52
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_7.wcnf O = 688
T = 10.71
O = 807
T = 1.42
(out)(err)
O = 688
T = 10.71
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_8.wcnf O = 577
T = 7.18
O = 739
T = 3.47
(out)(err)
O = 577
T = 7.18
(out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_9.wcnf O = 714
T = 9.81
O = 823
T = 4.47
(out)(err)
O = 714
T = 9.81
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_0.wcnf O = 1121
T = 7.73
O = 1381
T = 1.37
(out)(err)
O = 1121
T = 7.73
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_1.wcnf O = 1142
T = 10.05
O = 1340
T = 5.83
(out)(err)
O = 1142
T = 10.05
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_2.wcnf O = 1252
T = 7.69
O = 1655
T = 6.46
(out)(err)
O = 1252
T = 7.69
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_3.wcnf O = 1295
T = 9.33
O = 1500
T = 3.86
(out)(err)
O = 1295
T = 9.33
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_4.wcnf O = 1261
T = 7.17
O = 1620
T = 5.38
(out)(err)
O = 1261
T = 7.17
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_5.wcnf O = 1047
T = 8.78
O = 1292
T = 3.85
(out)(err)
O = 1047
T = 8.78
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_6.wcnf O = 1175
T = 8.20
O = 1414
T = 6.74
(out)(err)
O = 1175
T = 8.20
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_7.wcnf O = 1145
T = 7.39
O = 1364
T = 5.52
(out)(err)
O = 1145
T = 7.39
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_8.wcnf O = 1135
T = 7.94
O = 1432
T = 7.54
(out)(err)
O = 1135
T = 7.94
(out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_9.wcnf O = 1232
T = 8.68
O = 1462
T = 2.08
(out)(err)
O = 1232
T = 8.68
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_0.wcnf O = 1842
T = 7.40
O = 2283
T = 2.66
(out)(err)
O = 1842
T = 7.40
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_1.wcnf O = 1699
T = 4.86
O = 2239
T = 5.15
(out)(err)
O = 1699
T = 4.86
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_2.wcnf O = 1730
T = 9.23
O = 2166
T = 1.75
(out)(err)
O = 1730
T = 9.23
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_3.wcnf O = 1885
T = 9.38
O = 2214
T = 3.35
(out)(err)
O = 1885
T = 9.38
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_4.wcnf O = 2043
T = 40.96
O = 2417
T = 4.62
(out)(err)
O = 2043
T = 40.96
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_5.wcnf O = 1818
T = 9.08
O = 2091
T = 5.07
(out)(err)
O = 1818
T = 9.08
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_6.wcnf O = 1832
T = 13.33
O = 2159
T = 1.34
(out)(err)
O = 1832
T = 13.33
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_7.wcnf O = 1780
T = 11.09
O = 2184
T = 5.57
(out)(err)
O = 1780
T = 11.09
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_8.wcnf O = 1726
T = 11.76
O = 2131
T = 7.40
(out)(err)
O = 1726
T = 11.76
(out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_9.wcnf O = 1807
T = 6.85
O = 2262
T = 4.34
(out)(err)
O = 1807
T = 6.85
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_0.wcnf O = 2414
T = 10.19
O = 2934
T = 3.11
(out)(err)
O = 2414
T = 10.19
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_1.wcnf O = 2398
T = 4.96
O = 2814
T = 4.99
(out)(err)
O = 2398
T = 4.96
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_2.wcnf O = 2113
T = 10.58
O = 2686
T = 3.09
(out)(err)
O = 2113
T = 10.58
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_3.wcnf O = 2339
T = 11.28
O = 2885
T = 2.46
(out)(err)
O = 2339
T = 11.28
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_4.wcnf O = 2390
T = 12.99
O = 2933
T = 3.13
(out)(err)
O = 2390
T = 12.99
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_5.wcnf O = 2332
T = 9.12
O = 3028
T = 4.56
(out)(err)
O = 2332
T = 9.12
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_6.wcnf O = 2488
T = 8.84
O = 2978
T = 4.33
(out)(err)
O = 2488
T = 8.84
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_7.wcnf O = 2241
T = 8.19
O = 2611
T = 3.78
(out)(err)
O = 2241
T = 8.19
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_8.wcnf O = 2353
T = 9.25
O = 2832
T = 6.44
(out)(err)
O = 2353
T = 9.25
(out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_9.wcnf O = 2560
T = 9.65
O = 3031
T = 3.72
(out)(err)
O = 2560
T = 9.65
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_0.wcnf O = 2885
T = 9.50
O = 3290
T = 4.82
(out)(err)
O = 2885
T = 9.50
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_1.wcnf O = 2918
T = 9.40
O = 3316
T = 2.42
(out)(err)
O = 2918
T = 9.40
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_2.wcnf O = 2878
T = 8.66
O = 3345
T = 4.77
(out)(err)
O = 2878
T = 8.66
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_3.wcnf O = 3045
T = 11.60
O = 3501
T = 7.90
(out)(err)
O = 3045
T = 11.60
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_4.wcnf O = 3021
T = 9.08
O = 3511
T = 7.38
(out)(err)
O = 3021
T = 9.08
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_5.wcnf O = 2812
T = 1.47
O = 3369
T = 6.06
(out)(err)
O = 2812
T = 1.47
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_6.wcnf O = 2838
T = 8.86
O = 3369
T = 3.19
(out)(err)
O = 2838
T = 8.86
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_7.wcnf O = 2815
T = 9.15
O = 3506
T = 5.80
(out)(err)
O = 2815
T = 9.15
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_8.wcnf O = 3025
T = 10.24
O = 3609
T = 5.68
(out)(err)
O = 3025
T = 10.24
(out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_9.wcnf O = 2952
T = 11.71
O = 3433
T = 2.92
(out)(err)
O = 2952
T = 11.71
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_0.wcnf O = 3634
T = 13.03
O = 4247
T = 6.20
(out)(err)
O = 3634
T = 13.03
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_1.wcnf O = 3662
T = 12.44
O = 4317
T = 4.87
(out)(err)
O = 3662
T = 12.44
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_2.wcnf O = 3827
T = 10.03
O = 4348
T = 7.12
(out)(err)
O = 3827
T = 10.03
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_3.wcnf O = 3512
T = 16.68
O = 4016
T = 4.99
(out)(err)
O = 3512
T = 16.68
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_4.wcnf O = 3355
T = 8.63
O = 4090
T = 4.49
(out)(err)
O = 3355
T = 8.63
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_5.wcnf O = 3450
T = 6.89
O = 4028
T = 4.55
(out)(err)
O = 3450
T = 6.89
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_6.wcnf O = 3654
T = 11.34
O = 4310
T = 5.60
(out)(err)
O = 3654
T = 11.34
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_7.wcnf O = 3617
T = 6.96
O = 4116
T = 3.29
(out)(err)
O = 3617
T = 6.96
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_8.wcnf O = 3525
T = 10.41
O = 4108
T = 5.25
(out)(err)
O = 3525
T = 10.41
(out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_9.wcnf O = 3240
T = 7.20
O = 4171
T = 3.29
(out)(err)
O = 3240
T = 7.20
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf O = 28
T = 4.56
O = 31
T = 9.85
(out)(err)
O = 28
T = 4.56
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_1.wcnf O = 15
T = 2.60
O = 15
T = 156.21
(out)(err)
O = 15
T = 2.60
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_2.wcnf O = 25
T = 6.55
O = 180
T = 5.31
(out)(err)
O = 25
T = 6.55
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_3.wcnf O = 25
T = 5.33
O = 183
T = 4.16
(out)(err)
O = 25
T = 5.33
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_4.wcnf O = 30
T = 2.83
O = 30
T = 180.60
(out)(err)
O = 30
T = 2.83
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_5.wcnf O = 27
T = 4.12
O = 152
T = 5.72
(out)(err)
O = 27
T = 4.12
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_6.wcnf O = 26
T = 5.53
O = 159
T = 5.77
(out)(err)
O = 26
T = 5.53
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_7.wcnf O = 29
T = 3.07
O = 138
T = 5.64
(out)(err)
O = 29
T = 3.07
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_8.wcnf O = 19
T = 3.76
O = 29
T = 10.34
(out)(err)
O = 19
T = 3.76
(out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_9.wcnf O = 30
T = 4.98
O = 142
T = 2.70
(out)(err)
O = 30
T = 4.98
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_0.wcnf O = 54
T = 6.14
O = 162
T = 2.96
(out)(err)
O = 54
T = 6.14
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_1.wcnf O = 58
T = 5.33
O = 260
T = 2.32
(out)(err)
O = 58
T = 5.33
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_2.wcnf O = 59
T = 5.18
O = 247
T = 4.94
(out)(err)
O = 59
T = 5.18
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_3.wcnf O = 48
T = 5.01
O = 214
T = 6.36
(out)(err)
O = 48
T = 5.01
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_4.wcnf O = 42
T = 4.60
O = 279
T = 4.13
(out)(err)
O = 42
T = 4.60
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_5.wcnf O = 46
T = 4.59
O = 151
T = 5.43
(out)(err)
O = 46
T = 4.59
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_6.wcnf O = 51
T = 5.39
O = 84
T = 5.07
(out)(err)
O = 51
T = 5.39
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_7.wcnf O = 63
T = 5.49
O = 200
T = 4.78
(out)(err)
O = 63
T = 5.49
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_8.wcnf O = 64
T = 4.50
O = 226
T = 4.77
(out)(err)
O = 64
T = 4.50
(out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_9.wcnf O = 45
T = 0.67
O = 226
T = 4.21
(out)(err)
O = 45
T = 0.67
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_0.wcnf O = 95
T = 4.64
O = 231
T = 4.27
(out)(err)
O = 95
T = 4.64
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_1.wcnf O = 81
T = 5.26
O = 274
T = 4.85
(out)(err)
O = 81
T = 5.26
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_2.wcnf O = 77
T = 5.76
O = 188
T = 4.92
(out)(err)
O = 77
T = 5.76
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_3.wcnf O = 81
T = 6.56
O = 264
T = 5.53
(out)(err)
O = 81
T = 6.56
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_4.wcnf O = 75
T = 4.97
O = 303
T = 5.06
(out)(err)
O = 75
T = 4.97
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_5.wcnf O = 80
T = 5.09
O = 285
T = 4.31
(out)(err)
O = 80
T = 5.09
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_6.wcnf O = 74
T = 3.90
O = 287
T = 5.22
(out)(err)
O = 74
T = 3.90
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_7.wcnf O = 99
T = 4.79
O = 315
T = 4.58
(out)(err)
O = 99
T = 4.79
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_8.wcnf O = 90
T = 4.45
O = 138
T = 7.57
(out)(err)
O = 90
T = 4.45
(out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_9.wcnf O = 95
T = 5.10
O = 146
T = 10.43
(out)(err)
O = 95
T = 5.10
(out)(err)