src/2.log

   1 deserializing ...
   2 **********************
   3 Polarity time: 0.003698
   4 Preprocess time: 0.011524
   5 Decompose Order: 0.000017
   6 Encoding Graph Time: 0.037881
   7 Elapse Encode time: 0.997790
   8 Is problem UNSAT after encoding: 0
   9 CNF Encode time: 0.000001
  10 SAT Solving time: 22.486690
  11 Result Computed in SAT solver:  SAT
  12 CSOLVER solve time: 23.484500
  13 Mutating 1 settings
  14 &&&&&&&&Mutating&&&&&&&
  15 Param ELEMENTOPTSETS = 1         range=[0,1]
  16 &&&&&&&&&&&&&&&&&&&&&&&
  17 **********************
  18 Polarity time: 0.004408
  19 Preprocess time: 0.015162
  20 Decompose Order: 0.000007
  21 Encoding Graph Time: 0.075089
  22 Elapse Encode time: 0.170877
  23 Is problem UNSAT after encoding: 0
  24 CNF Encode time: 0.000000
  25 SAT Solving time: 83.681346
  26 Result Computed in SAT solver:  SAT
  27 CSOLVER solve time: 83.852230
  28 Param PREPROCESS = 1     range=[0,1]
  29 Param ELEMENTOPTSETS = 1         range=[0,1]
  30 Param ELEMENTOPT = 1     range=[0,1]
  31 Param PROXYVARIABLE = 1          range=[1,5]
  32 Received score 83852230129.000000
  33 Mutating 1 settings
  34 &&&&&&&&Mutating&&&&&&&
  35 Param PREPROCESS = 0     range=[0,1]
  36 &&&&&&&&&&&&&&&&&&&&&&&
  37 **********************
  38 Polarity time: 0.004306
  39 Preprocess time: 0.000012
  40 Decompose Order: 0.000003
  41 Encoding Graph Time: 0.041191
  42 Elapse Encode time: 0.993668
  43 Is problem UNSAT after encoding: 0
  44 CNF Encode time: 0.000000
  45 SAT Solving time: 87.561080
  46 Result Computed in SAT solver:  SAT
  47 CSOLVER solve time: 88.554759
  48 Param PREPROCESS = 0     range=[0,1]
  49 Param ELEMENTOPTSETS = 0         range=[0,1]
  50 Param ELEMENTOPT = 1     range=[0,1]
  51 Param PROXYVARIABLE = 1          range=[1,5]
  52 Received score 88554759182.000000
  53 Mutating 1 settings
  54 &&&&&&&&Mutating&&&&&&&
  55 Param ELEMENTOPT = 0     range=[0,1]
  56 &&&&&&&&&&&&&&&&&&&&&&&
  57 **********************
  58 Polarity time: 0.004242
  59 Preprocess time: 0.014907
  60 Decompose Order: 0.000006
  61 Encoding Graph Time: 0.005495
  62 Elapse Encode time: 3.395448
  63 Is problem UNSAT after encoding: 0
  64 CNF Encode time: 0.000000
  65 SAT Solving time: 59.817873
  66 Result Computed in SAT solver:  SAT
  67 CSOLVER solve time: 63.213332
  68 Param PREPROCESS = 1     range=[0,1]
  69 Param ELEMENTOPTSETS = 0         range=[0,1]
  70 Param ELEMENTOPT = 0     range=[0,1]
  71 Param PROXYVARIABLE = 1          range=[1,5]
  72 Received score 63213332241.000000
  73 Mutating 1 settings
  74 &&&&&&&&Mutating&&&&&&&
  75 Param PROXYVARIABLE = 5          range=[1,5]
  76 &&&&&&&&&&&&&&&&&&&&&&&
  77 **********************
  78 Polarity time: 0.004321
  79 Preprocess time: 0.015034
  80 Decompose Order: 0.000006
  81 Encoding Graph Time: 0.041278
  82 Elapse Encode time: 1.011671
  83 Is problem UNSAT after encoding: 0
  84 CNF Encode time: 0.000000
  85 SAT Solving time: 89.444982
  86 Result Computed in SAT solver:  SAT
  87 CSOLVER solve time: 90.456664
  88 Param PREPROCESS = 1     range=[0,1]
  89 Param ELEMENTOPTSETS = 0         range=[0,1]
  90 Param ELEMENTOPT = 1     range=[0,1]
  91 Param PROXYVARIABLE = 5          range=[1,5]
  92 Received score 90456664442.000000
  93 Mutating 1 settings
  94 &&&&&&&&Mutating&&&&&&&
  95 Param PREPROCESS = 0     range=[0,1]
  96 &&&&&&&&&&&&&&&&&&&&&&&
  97 **********************
  98 Polarity time: 0.003616
  99 Preprocess time: 0.000013
 100 Decompose Order: 0.000004
 101 Encoding Graph Time: 0.036958
 102 Elapse Encode time: 0.991289
 103 Is problem UNSAT after encoding: 0
 104 CNF Encode time: 0.000000
 105 SAT Solving time: 30.786825
 106 Result Computed in SAT solver:  SAT
 107 CSOLVER solve time: 31.778125
 108 Param PREPROCESS = 0     range=[0,1]
 109 Param ELEMENTOPTSETS = 0         range=[0,1]
 110 Param ELEMENTOPT = 1     range=[0,1]
 111 Param PROXYVARIABLE = 1          range=[1,5]
 112 Received score 31778124877.000000
 113 Mutating 1 settings
 114 &&&&&&&&Mutating&&&&&&&
 115 Param PREPROCESS = 1     range=[0,1]
 116 &&&&&&&&&&&&&&&&&&&&&&&
 117 **********************
 118 Polarity time: 0.004231
 119 Preprocess time: 0.014832
 120 Decompose Order: 0.000007
 121 Encoding Graph Time: 0.039483
 122 Elapse Encode time: 1.005092
 123 Is problem UNSAT after encoding: 0
 124 CNF Encode time: 0.000000
 125 SAT Solving time: 31.087874
 126 Result Computed in SAT solver:  SAT
 127 CSOLVER solve time: 32.092977
 128 Param PREPROCESS = 1     range=[0,1]
 129 Param ELEMENTOPTSETS = 0         range=[0,1]
 130 Param ELEMENTOPT = 1     range=[0,1]
 131 Param PROXYVARIABLE = 1          range=[1,5]
 132 Received score 32092977155.000000
 133 Mutating 1 settings
 134 &&&&&&&&Mutating&&&&&&&
 135 Param PROXYVARIABLE = 3          range=[1,5]
 136 &&&&&&&&&&&&&&&&&&&&&&&
 137 **********************
 138 Polarity time: 0.004257
 139 Preprocess time: 0.014958
 140 Decompose Order: 0.000007
 141 Encoding Graph Time: 0.041401
 142 Elapse Encode time: 1.008422
 143 Is problem UNSAT after encoding: 0
 144 CNF Encode time: 0.000000
 145 SAT Solving time: 30.392583
 146 Result Computed in SAT solver:  SAT
 147 CSOLVER solve time: 31.401015
 148 Param PREPROCESS = 1     range=[0,1]
 149 Param ELEMENTOPTSETS = 0         range=[0,1]
 150 Param ELEMENTOPT = 1     range=[0,1]
 151 Param PROXYVARIABLE = 3          range=[1,5]
 152 Received score 31401015378.000000
 153 Mutating 1 settings
 154 &&&&&&&&Mutating&&&&&&&
 155 Param ELEMENTOPT = 0     range=[0,1]
 156 &&&&&&&&&&&&&&&&&&&&&&&
 157 **********************
 158 Polarity time: 0.004297
 159 Preprocess time: 0.014887
 160 Decompose Order: 0.000007
 161 Encoding Graph Time: 0.005476
 162 Elapse Encode time: 3.399174
 163 Is problem UNSAT after encoding: 0
 164 CNF Encode time: 0.000000
 165 SAT Solving time: 105.910181
 166 Result Computed in SAT solver:  SAT
 167 CSOLVER solve time: 109.309367
 168 Param PREPROCESS = 1     range=[0,1]
 169 Param ELEMENTOPTSETS = 0         range=[0,1]
 170 Param ELEMENTOPT = 0     range=[0,1]
 171 Param PROXYVARIABLE = 3          range=[1,5]
 172 Received score 109309366995.000000
 173 Mutating 1 settings
 174 &&&&&&&&Mutating&&&&&&&
 175 Param PROXYVARIABLE = 5          range=[1,5]
 176 &&&&&&&&&&&&&&&&&&&&&&&
 177 **********************
 178 Polarity time: 0.004377
 179 Preprocess time: 0.015036
 180 Decompose Order: 0.000007
 181 Encoding Graph Time: 0.041241
 182 Elapse Encode time: 1.013063
 183 Is problem UNSAT after encoding: 0
 184 CNF Encode time: 0.000000
 185 SAT Solving time: 40.816514
 186 Result Computed in SAT solver:  SAT
 187 CSOLVER solve time: 41.829587
 188 Param PREPROCESS = 1     range=[0,1]
 189 Param ELEMENTOPTSETS = 0         range=[0,1]
 190 Param ELEMENTOPT = 1     range=[0,1]
 191 Param PROXYVARIABLE = 5          range=[1,5]
 192 Received score 41829587127.000000
 193 Mutating 1 settings
 194 &&&&&&&&Mutating&&&&&&&
 195 Param ELEMENTOPT = 0     range=[0,1]
 196 &&&&&&&&&&&&&&&&&&&&&&&
 197 **********************
 198 Polarity time: 0.004338
 199 Preprocess time: 0.015042
 200 Decompose Order: 0.000006
 201 Encoding Graph Time: 0.005625
 202 Elapse Encode time: 3.407410
 203 Is problem UNSAT after encoding: 0
 204 CNF Encode time: 0.000000
 205 SAT Solving time: 83.632609
 206 Result Computed in SAT solver:  SAT
 207 CSOLVER solve time: 87.040030
 208 Param PREPROCESS = 1     range=[0,1]
 209 Param ELEMENTOPTSETS = 0         range=[0,1]
 210 Param ELEMENTOPT = 0     range=[0,1]
 211 Param PROXYVARIABLE = 5          range=[1,5]
 212 Received score 87040029909.000000
 213 Mutating 1 settings
 214 &&&&&&&&Mutating&&&&&&&
 215 Param ELEMENTOPTSETS = 1         range=[0,1]
 216 &&&&&&&&&&&&&&&&&&&&&&&
 217 **********************
 218 Polarity time: 0.004251
 219 Preprocess time: 0.014971
 220 Decompose Order: 0.000007
 221 Encoding Graph Time: 0.074759
 222 Elapse Encode time: 0.169985
 223 Is problem UNSAT after encoding: 0
 224 CNF Encode time: 0.000000
 225 SAT Solving time: 83.095377
 226 Result Computed in SAT solver:  SAT
 227 CSOLVER solve time: 83.265372
 228 Param PREPROCESS = 1     range=[0,1]
 229 Param ELEMENTOPTSETS = 1         range=[0,1]
 230 Param ELEMENTOPT = 1     range=[0,1]
 231 Param PROXYVARIABLE = 5          range=[1,5]
 232 Received score 83265371895.000000
 233 Mutating 1 settings
 234 &&&&&&&&Mutating&&&&&&&
 235 Param PREPROCESS = 0     range=[0,1]
 236 &&&&&&&&&&&&&&&&&&&&&&&
 237 **********************
 238 Polarity time: 0.003756
 239 Preprocess time: 0.000011
 240 Decompose Order: 0.000004
 241 Encoding Graph Time: 0.038465
 242 Elapse Encode time: 0.991921
 243 Is problem UNSAT after encoding: 0
 244 CNF Encode time: 0.000000
 245 SAT Solving time: 41.302063
 246 Result Computed in SAT solver:  SAT
 247 CSOLVER solve time: 42.293995
 248 Param PREPROCESS = 0     range=[0,1]
 249 Param ELEMENTOPTSETS = 0         range=[0,1]
 250 Param ELEMENTOPT = 1     range=[0,1]
 251 Param PROXYVARIABLE = 5          range=[1,5]
 252 Received score 42293995203.000000
 253 Mutating 1 settings
 254 &&&&&&&&Mutating&&&&&&&
 255 Param ELEMENTOPTSETS = 1         range=[0,1]
 256 &&&&&&&&&&&&&&&&&&&&&&&
 257 **********************
 258 Polarity time: 0.004323
 259 Preprocess time: 0.000015
 260 Decompose Order: 0.000003
 261 Encoding Graph Time: 0.074547
 262 Elapse Encode time: 0.157879
 263 Is problem UNSAT after encoding: 0
 264 CNF Encode time: 0.000000
 265 SAT Solving time: 81.915438
 266 Result Computed in SAT solver:  SAT
 267 CSOLVER solve time: 82.073324
 268 Param PREPROCESS = 0     range=[0,1]
 269 Param ELEMENTOPTSETS = 1         range=[0,1]
 270 Param ELEMENTOPT = 1     range=[0,1]
 271 Param PROXYVARIABLE = 5          range=[1,5]
 272 Received score 82073324225.000000
 273 Mutating 1 settings
 274 &&&&&&&&Mutating&&&&&&&
 275 Param PROXYVARIABLE = 1          range=[1,5]
 276 &&&&&&&&&&&&&&&&&&&&&&&
 277 **********************
 278 Polarity time: 0.004248
 279 Preprocess time: 0.000014
 280 Decompose Order: 0.000004
 281 Encoding Graph Time: 0.041180
 282 Elapse Encode time: 0.995260
 283 Is problem UNSAT after encoding: 0
 284 CNF Encode time: 0.000000
 285 SAT Solving time: 26.421098
 286 Result Computed in SAT solver:  SAT
 287 CSOLVER solve time: 27.416369
 288 Param PREPROCESS = 0     range=[0,1]
 289 Param ELEMENTOPTSETS = 0         range=[0,1]
 290 Param ELEMENTOPT = 1     range=[0,1]
 291 Param PROXYVARIABLE = 1          range=[1,5]
 292 Received score 27416368661.000000
 293 Mutating 1 settings
 294 &&&&&&&&Mutating&&&&&&&
 295 Param ELEMENTOPT = 0     range=[0,1]
 296 &&&&&&&&&&&&&&&&&&&&&&&
 297 **********************
 298 Polarity time: 0.004342
 299 Preprocess time: 0.000014
 300 Decompose Order: 0.000003
 301 Encoding Graph Time: 0.005481
 302 Elapse Encode time: 3.371583
 303 Is problem UNSAT after encoding: 0
 304 CNF Encode time: 0.000000
 305 SAT Solving time: 85.153587
 306 Result Computed in SAT solver:  SAT
 307 CSOLVER solve time: 88.525182
 308 Param PREPROCESS = 0     range=[0,1]
 309 Param ELEMENTOPTSETS = 0         range=[0,1]
 310 Param ELEMENTOPT = 0     range=[0,1]
 311 Param PROXYVARIABLE = 1          range=[1,5]
 312 Received score 88525181902.000000
 313 Mutating 1 settings
 314 &&&&&&&&Mutating&&&&&&&
 315 Param ELEMENTOPT = 0     range=[0,1]
 316 &&&&&&&&&&&&&&&&&&&&&&&
 317 **********************
 318 Polarity time: 0.004275
 319 Preprocess time: 0.000013
 320 Decompose Order: 0.000003
 321 Encoding Graph Time: 0.005308
 322 Elapse Encode time: 3.380358
 323 Is problem UNSAT after encoding: 0
 324 CNF Encode time: 0.000000
 325 SAT Solving time: 87.043549
 326 Result Computed in SAT solver:  SAT
 327 CSOLVER solve time: 90.423918
 328 Param PREPROCESS = 0     range=[0,1]
 329 Param ELEMENTOPTSETS = 0         range=[0,1]
 330 Param ELEMENTOPT = 0     range=[0,1]
 331 Param PROXYVARIABLE = 1          range=[1,5]
 332 Received score 90423918219.000000
 333 Mutating 1 settings
 334 &&&&&&&&Mutating&&&&&&&
 335 Param PROXYVARIABLE = 2          range=[1,5]
 336 &&&&&&&&&&&&&&&&&&&&&&&
 337 **********************
 338 Polarity time: 0.004281
 339 Preprocess time: 0.000014
 340 Decompose Order: 0.000003
 341 Encoding Graph Time: 0.041230
 342 Elapse Encode time: 0.991263
 343 Is problem UNSAT after encoding: 0
 344 CNF Encode time: 0.000000
 345 SAT Solving time: 52.397527
 346 Result Computed in SAT solver:  SAT
 347 CSOLVER solve time: 53.388801
 348 Param PREPROCESS = 0     range=[0,1]
 349 Param ELEMENTOPTSETS = 0         range=[0,1]
 350 Param ELEMENTOPT = 1     range=[0,1]
 351 Param PROXYVARIABLE = 2          range=[1,5]
 352 Received score 53388800680.000000
 353 Mutating 1 settings
 354 &&&&&&&&Mutating&&&&&&&
 355 Param ELEMENTOPTSETS = 1         range=[0,1]
 356 &&&&&&&&&&&&&&&&&&&&&&&
 357 **********************
 358 Polarity time: 0.004273
 359 Preprocess time: 0.000013
 360 Decompose Order: 0.000004
 361 Encoding Graph Time: 0.074555
 362 Elapse Encode time: 0.154938
 363 Is problem UNSAT after encoding: 0
 364 CNF Encode time: 0.000000
 365 SAT Solving time: 83.008266
 366 Result Computed in SAT solver:  SAT
 367 CSOLVER solve time: 83.163213
 368 Param PREPROCESS = 0     range=[0,1]
 369 Param ELEMENTOPTSETS = 1         range=[0,1]
 370 Param ELEMENTOPT = 1     range=[0,1]
 371 Param PROXYVARIABLE = 1          range=[1,5]
 372 Received score 83163213105.000000
 373 Mutating 1 settings
 374 &&&&&&&&Mutating&&&&&&&
 375 Param PREPROCESS = 1     range=[0,1]
 376 &&&&&&&&&&&&&&&&&&&&&&&
 377 **********************
 378 Polarity time: 0.003818
 379 Preprocess time: 0.011169
 380 Decompose Order: 0.000006
 381 Encoding Graph Time: 0.070034
 382 Elapse Encode time: 0.159874
 383 Is problem UNSAT after encoding: 0
 384 CNF Encode time: 0.000000
 385 SAT Solving time: 82.624972
 386 Result Computed in SAT solver:  SAT
 387 CSOLVER solve time: 82.784855
 388 Param PREPROCESS = 1     range=[0,1]
 389 Param ELEMENTOPTSETS = 1         range=[0,1]
 390 Param ELEMENTOPT = 1     range=[0,1]
 391 Param PROXYVARIABLE = 1          range=[1,5]
 392 Received score 82784854843.000000
 393 Mutating 1 settings
 394 &&&&&&&&Mutating&&&&&&&
 395 Param ELEMENTOPTSETS = 0         range=[0,1]
 396 &&&&&&&&&&&&&&&&&&&&&&&
 397 **********************
 398 Polarity time: 0.004343
 399 Preprocess time: 0.015029
 400 Decompose Order: 0.000007
 401 Encoding Graph Time: 0.041378
 402 Elapse Encode time: 1.007336
 403 Is problem UNSAT after encoding: 0
 404 CNF Encode time: 0.000000
 405 SAT Solving time: 31.199024
 406 Result Computed in SAT solver:  SAT
 407 CSOLVER solve time: 32.206371
 408 Param PREPROCESS = 1     range=[0,1]
 409 Param ELEMENTOPTSETS = 0         range=[0,1]
 410 Param ELEMENTOPT = 1     range=[0,1]
 411 Param PROXYVARIABLE = 1          range=[1,5]
 412 Received score 32206370553.000000
 413 Mutating 1 settings
 414 &&&&&&&&Mutating&&&&&&&
 415 Param PREPROCESS = 0     range=[0,1]
 416 &&&&&&&&&&&&&&&&&&&&&&&
 417 **********************
 418 Polarity time: 0.004382
 419 Preprocess time: 0.000015
 420 Decompose Order: 0.000003
 421 Encoding Graph Time: 0.041151
 422 Elapse Encode time: 0.993579
 423 Is problem UNSAT after encoding: 0
 424 CNF Encode time: 0.000000
 425 SAT Solving time: 20.294117
 426 Result Computed in SAT solver:  SAT
 427 CSOLVER solve time: 21.287706
 428 Param PREPROCESS = 0     range=[0,1]
 429 Param ELEMENTOPTSETS = 0         range=[0,1]
 430 Param ELEMENTOPT = 1     range=[0,1]
 431 Param PROXYVARIABLE = 1          range=[1,5]
 432 Received score 21287706291.000000
 433 Mutating 1 settings
 434 &&&&&&&&Mutating&&&&&&&
 435 Param ELEMENTOPTSETS = 1         range=[0,1]
 436 &&&&&&&&&&&&&&&&&&&&&&&
 437 **********************
 438 Polarity time: 0.003636
 439 Preprocess time: 0.000013
 440 Decompose Order: 0.000003
 441 Encoding Graph Time: 0.070066
 442 Elapse Encode time: 0.148509
 443 Is problem UNSAT after encoding: 0
 444 CNF Encode time: 0.000000
 445 SAT Solving time: 83.965949
 446 Result Computed in SAT solver:  SAT
 447 CSOLVER solve time: 84.114467
 448 Param PREPROCESS = 0     range=[0,1]
 449 Param ELEMENTOPTSETS = 1         range=[0,1]
 450 Param ELEMENTOPT = 1     range=[0,1]
 451 Param PROXYVARIABLE = 1          range=[1,5]
 452 Received score 84114467261.000000
 453 Mutating 1 settings
 454 &&&&&&&&Mutating&&&&&&&
 455 Param PREPROCESS = 1     range=[0,1]
 456 &&&&&&&&&&&&&&&&&&&&&&&
 457 **********************
 458 Polarity time: 0.003609
 459 Preprocess time: 0.011215
 460 Decompose Order: 0.000007
 461 Encoding Graph Time: 0.037147
 462 Elapse Encode time: 0.998892
 463 Is problem UNSAT after encoding: 0
 464 CNF Encode time: 0.000000
 465 SAT Solving time: 30.748693
 466 Result Computed in SAT solver:  SAT
 467 CSOLVER solve time: 31.747596
 468 Param PREPROCESS = 1     range=[0,1]
 469 Param ELEMENTOPTSETS = 0         range=[0,1]
 470 Param ELEMENTOPT = 1     range=[0,1]
 471 Param PROXYVARIABLE = 1          range=[1,5]
 472 Received score 31747596132.000000
 473 Mutating 1 settings
 474 &&&&&&&&Mutating&&&&&&&
 475 Param ELEMENTOPTSETS = 1         range=[0,1]
 476 &&&&&&&&&&&&&&&&&&&&&&&
 477 **********************
 478 Polarity time: 0.004389
 479 Preprocess time: 0.015054
 480 Decompose Order: 0.000007
 481 Encoding Graph Time: 0.074696
 482 Elapse Encode time: 0.170195
 483 Is problem UNSAT after encoding: 0
 484 CNF Encode time: 0.000000
 485 SAT Solving time: 82.414739
 486 Result Computed in SAT solver:  SAT
 487 CSOLVER solve time: 82.584943
 488 Param PREPROCESS = 1     range=[0,1]
 489 Param ELEMENTOPTSETS = 1         range=[0,1]
 490 Param ELEMENTOPT = 1     range=[0,1]
 491 Param PROXYVARIABLE = 1          range=[1,5]
 492 Received score 82584943418.000000
 493 Mutating 1 settings
 494 &&&&&&&&Mutating&&&&&&&
 495 Param ELEMENTOPT = 0     range=[0,1]
 496 &&&&&&&&&&&&&&&&&&&&&&&
 497 **********************
 498 Polarity time: 0.004320
 499 Preprocess time: 0.014481
 500 Decompose Order: 0.000007
 501 Encoding Graph Time: 0.004594
 502 Elapse Encode time: 3.396318
 503 Is problem UNSAT after encoding: 0
 504 CNF Encode time: 0.000000
 505 SAT Solving time: 85.187796
 506 Result Computed in SAT solver:  SAT
 507 CSOLVER solve time: 88.584126
 508 Param PREPROCESS = 1     range=[0,1]
 509 Param ELEMENTOPTSETS = 0         range=[0,1]
 510 Param ELEMENTOPT = 0     range=[0,1]
 511 Param PROXYVARIABLE = 1          range=[1,5]
 512 Received score 88584125805.000000
 513 Mutating 1 settings
 514 &&&&&&&&Mutating&&&&&&&
 515 Param ELEMENTOPT = 0     range=[0,1]
 516 &&&&&&&&&&&&&&&&&&&&&&&
 517 **********************
 518 Polarity time: 0.004375
 519 Preprocess time: 0.015001
 520 Decompose Order: 0.000006
 521 Encoding Graph Time: 0.005633
 522 Elapse Encode time: 3.389372
 523 Is problem UNSAT after encoding: 0
 524 CNF Encode time: 0.000000
 525 SAT Solving time: 87.848146
 526 Result Computed in SAT solver:  SAT
 527 CSOLVER solve time: 91.237530
 528 Param PREPROCESS = 1     range=[0,1]
 529 Param ELEMENTOPTSETS = 0         range=[0,1]
 530 Param ELEMENTOPT = 0     range=[0,1]
 531 Param PROXYVARIABLE = 1          range=[1,5]
 532 Received score 91237529526.000000
 533 Mutating 1 settings
 534 &&&&&&&&Mutating&&&&&&&
 535 Param PREPROCESS = 0     range=[0,1]
 536 &&&&&&&&&&&&&&&&&&&&&&&
 537 **********************
 538 Polarity time: 0.004391
 539 Preprocess time: 0.000014
 540 Decompose Order: 0.000004
 541 Encoding Graph Time: 0.037852
 542 Elapse Encode time: 0.992423
 543 Is problem UNSAT after encoding: 0
 544 CNF Encode time: 0.000000
 545 SAT Solving time: 61.716614
 546 Result Computed in SAT solver:  SAT
 547 CSOLVER solve time: 62.709048
 548 Param PREPROCESS = 0     range=[0,1]
 549 Param ELEMENTOPTSETS = 0         range=[0,1]
 550 Param ELEMENTOPT = 1     range=[0,1]
 551 Param PROXYVARIABLE = 1          range=[1,5]
 552 Received score 62709047878.000000
 553 Mutating 1 settings
 554 &&&&&&&&Mutating&&&&&&&
 555 Param PREPROCESS = 0     range=[0,1]
 556 &&&&&&&&&&&&&&&&&&&&&&&
 557 **********************
 558 Polarity time: 0.004286
 559 Preprocess time: 0.000015
 560 Decompose Order: 0.000003
 561 Encoding Graph Time: 0.043198
 562 Elapse Encode time: 0.995987
 563 Is problem UNSAT after encoding: 0
 564 CNF Encode time: 0.000000
 565 SAT Solving time: 5.946959
 566 Result Computed in SAT solver:  SAT
 567 CSOLVER solve time: 6.942956
 568 Param PREPROCESS = 0     range=[0,1]
 569 Param ELEMENTOPTSETS = 0         range=[0,1]
 570 Param ELEMENTOPT = 1     range=[0,1]
 571 Param PROXYVARIABLE = 1          range=[1,5]
 572 Received score 6942956251.000000
 573 Mutating 1 settings
 574 &&&&&&&&Mutating&&&&&&&
 575 Param ELEMENTOPT = 0     range=[0,1]
 576 &&&&&&&&&&&&&&&&&&&&&&&
 577 **********************
 578 Polarity time: 0.004261
 579 Preprocess time: 0.000013
 580 Decompose Order: 0.000004
 581 Encoding Graph Time: 0.005362
 582 Elapse Encode time: 3.384706
 583 Is problem UNSAT after encoding: 0
 584 CNF Encode time: 0.000000
 585 SAT Solving time: 112.144277
 586 Result Computed in SAT solver:  SAT
 587 CSOLVER solve time: 115.528994
 588 Param PREPROCESS = 0     range=[0,1]
 589 Param ELEMENTOPTSETS = 0         range=[0,1]
 590 Param ELEMENTOPT = 0     range=[0,1]
 591 Param PROXYVARIABLE = 1          range=[1,5]
 592 Received score 115528994215.000000
 593 Mutating 1 settings
 594 &&&&&&&&Mutating&&&&&&&
 595 Param PREPROCESS = 1     range=[0,1]
 596 &&&&&&&&&&&&&&&&&&&&&&&
 597 **********************
 598 Polarity time: 0.004353
 599 Preprocess time: 0.015062
 600 Decompose Order: 0.000006
 601 Encoding Graph Time: 0.041410
 602 Elapse Encode time: 1.007912
 603 Is problem UNSAT after encoding: 0
 604 CNF Encode time: 0.000000
 605 SAT Solving time: 30.765756
 606 Result Computed in SAT solver:  SAT
 607 CSOLVER solve time: 31.773680
 608 Param PREPROCESS = 1     range=[0,1]
 609 Param ELEMENTOPTSETS = 0         range=[0,1]
 610 Param ELEMENTOPT = 1     range=[0,1]
 611 Param PROXYVARIABLE = 1          range=[1,5]
 612 Received score 31773679622.000000
 613 Mutating 1 settings
 614 &&&&&&&&Mutating&&&&&&&
 615 Param PROXYVARIABLE = 2          range=[1,5]
 616 &&&&&&&&&&&&&&&&&&&&&&&
 617 **********************
 618 Polarity time: 0.004336
 619 Preprocess time: 0.000013
 620 Decompose Order: 0.000003
 621 Encoding Graph Time: 0.041225
 622 Elapse Encode time: 0.995415
 623 Is problem UNSAT after encoding: 0
 624 CNF Encode time: 0.000000
 625 SAT Solving time: 8.564521
 626 Result Computed in SAT solver:  SAT
 627 CSOLVER solve time: 9.559946
 628 Param PREPROCESS = 0     range=[0,1]
 629 Param ELEMENTOPTSETS = 0         range=[0,1]
 630 Param ELEMENTOPT = 1     range=[0,1]
 631 Param PROXYVARIABLE = 2          range=[1,5]
 632 Received score 9559946211.000000
 633 Mutating 1 settings
 634 &&&&&&&&Mutating&&&&&&&
 635 Param ELEMENTOPT = 0     range=[0,1]
 636 &&&&&&&&&&&&&&&&&&&&&&&
 637 **********************
 638 Polarity time: 0.004269
 639 Preprocess time: 0.000015
 640 Decompose Order: 0.000003
 641 Encoding Graph Time: 0.005307
 642 Elapse Encode time: 3.382184
 643 Is problem UNSAT after encoding: 0
 644 CNF Encode time: 0.000000
 645 SAT Solving time: 89.076015
 646 Result Computed in SAT solver:  SAT
 647 CSOLVER solve time: 92.458210
 648 Param PREPROCESS = 0     range=[0,1]
 649 Param ELEMENTOPTSETS = 0         range=[0,1]
 650 Param ELEMENTOPT = 0     range=[0,1]
 651 Param PROXYVARIABLE = 2          range=[1,5]
 652 Received score 92458209983.000000
 653 Mutating 1 settings
 654 &&&&&&&&Mutating&&&&&&&
 655 Param PROXYVARIABLE = 4          range=[1,5]
 656 &&&&&&&&&&&&&&&&&&&&&&&
 657 **********************
 658 Polarity time: 0.003616
 659 Preprocess time: 0.000015
 660 Decompose Order: 0.000004
 661 Encoding Graph Time: 0.037030
 662 Elapse Encode time: 0.988529
 663 Is problem UNSAT after encoding: 0
 664 CNF Encode time: 0.000000
 665 SAT Solving time: 30.816409
 666 Result Computed in SAT solver:  SAT
 667 CSOLVER solve time: 31.804950
 668 Param PREPROCESS = 0     range=[0,1]
 669 Param ELEMENTOPTSETS = 0         range=[0,1]
 670 Param ELEMENTOPT = 1     range=[0,1]
 671 Param PROXYVARIABLE = 4          range=[1,5]
 672 Received score 31804949698.000000
 673 Mutating 1 settings
 674 &&&&&&&&Mutating&&&&&&&
 675 Param ELEMENTOPT = 0     range=[0,1]
 676 &&&&&&&&&&&&&&&&&&&&&&&
 677 **********************
 678 Polarity time: 0.003637
 679 Preprocess time: 0.000016
 680 Decompose Order: 0.000003
 681 Encoding Graph Time: 0.004500
 682 Elapse Encode time: 3.381605
 683 Is problem UNSAT after encoding: 0
 684 CNF Encode time: 0.000000
 685 SAT Solving time: 105.624640
 686 Result Computed in SAT solver:  SAT
 687 CSOLVER solve time: 109.006257
 688 Param PREPROCESS = 0     range=[0,1]
 689 Param ELEMENTOPTSETS = 0         range=[0,1]
 690 Param ELEMENTOPT = 0     range=[0,1]
 691 Param PROXYVARIABLE = 2          range=[1,5]
 692 Received score 109006257268.000000
 693 Mutating 1 settings
 694 &&&&&&&&Mutating&&&&&&&
 695 Param ELEMENTOPTSETS = 1         range=[0,1]
 696 &&&&&&&&&&&&&&&&&&&&&&&
 697 **********************
 698 Polarity time: 0.003609
 699 Preprocess time: 0.000015
 700 Decompose Order: 0.000003
 701 Encoding Graph Time: 0.070066
 702 Elapse Encode time: 0.148246
 703 Is problem UNSAT after encoding: 0
 704 CNF Encode time: 0.000000
 705 SAT Solving time: 83.017586
 706 Result Computed in SAT solver:  SAT
 707 CSOLVER solve time: 83.165841
 708 Param PREPROCESS = 0     range=[0,1]
 709 Param ELEMENTOPTSETS = 1         range=[0,1]
 710 Param ELEMENTOPT = 1     range=[0,1]
 711 Param PROXYVARIABLE = 2          range=[1,5]
 712 Received score 83165841166.000000
 713 Mutating 1 settings
 714 &&&&&&&&Mutating&&&&&&&
 715 Param PREPROCESS = 1     range=[0,1]
 716 &&&&&&&&&&&&&&&&&&&&&&&
 717 **********************
 718 Polarity time: 0.003793
 719 Preprocess time: 0.011294
 720 Decompose Order: 0.000007
 721 Encoding Graph Time: 0.037214
 722 Elapse Encode time: 1.004501
 723 Is problem UNSAT after encoding: 0
 724 CNF Encode time: 0.000000
 725 SAT Solving time: 40.405115
 726 Result Computed in SAT solver:  SAT
 727 CSOLVER solve time: 41.409626
 728 Param PREPROCESS = 1     range=[0,1]
 729 Param ELEMENTOPTSETS = 0         range=[0,1]
 730 Param ELEMENTOPT = 1     range=[0,1]
 731 Param PROXYVARIABLE = 2          range=[1,5]
 732 Received score 41409625928.000000
 733 Mutating 1 settings
 734 &&&&&&&&Mutating&&&&&&&
 735 Param ELEMENTOPTSETS = 1         range=[0,1]
 736 &&&&&&&&&&&&&&&&&&&&&&&
 737 **********************
 738 Polarity time: 0.003628
 739 Preprocess time: 0.000016
 740 Decompose Order: 0.000004
 741 Encoding Graph Time: 0.070005
 742 Elapse Encode time: 0.148406
 743 Is problem UNSAT after encoding: 0
 744 CNF Encode time: 0.000000
 745 SAT Solving time: 82.673455
 746 Result Computed in SAT solver:  SAT
 747 CSOLVER solve time: 82.821879
 748 Param PREPROCESS = 0     range=[0,1]
 749 Param ELEMENTOPTSETS = 1         range=[0,1]
 750 Param ELEMENTOPT = 1     range=[0,1]
 751 Param PROXYVARIABLE = 2          range=[1,5]
 752 Received score 82821878812.000000
 753 Mutating 1 settings
 754 &&&&&&&&Mutating&&&&&&&
 755 Param ELEMENTOPTSETS = 1         range=[0,1]
 756 &&&&&&&&&&&&&&&&&&&&&&&
 757 **********************
 758 Polarity time: 0.003589
 759 Preprocess time: 0.000015
 760 Decompose Order: 0.000004
 761 Encoding Graph Time: 0.069845
 762 Elapse Encode time: 0.148089
 763 Is problem UNSAT after encoding: 0
 764 CNF Encode time: 0.000000
 765 SAT Solving time: 82.260363
 766 Result Computed in SAT solver:  SAT
 767 CSOLVER solve time: 82.408461
 768 Param PREPROCESS = 0     range=[0,1]
 769 Param ELEMENTOPTSETS = 1         range=[0,1]
 770 Param ELEMENTOPT = 1     range=[0,1]
 771 Param PROXYVARIABLE = 2          range=[1,5]
 772 Received score 82408461414.000000
 773 Mutating 1 settings
 774 &&&&&&&&Mutating&&&&&&&
 775 Param PREPROCESS = 1     range=[0,1]
 776 &&&&&&&&&&&&&&&&&&&&&&&
 777 **********************
 778 Polarity time: 0.003662
 779 Preprocess time: 0.011214
 780 Decompose Order: 0.000008
 781 Encoding Graph Time: 0.037162
 782 Elapse Encode time: 1.000221
 783 Is problem UNSAT after encoding: 0
 784 CNF Encode time: 0.000000
 785 SAT Solving time: 63.581372
 786 Result Computed in SAT solver:  SAT
 787 CSOLVER solve time: 64.581604
 788 Param PREPROCESS = 1     range=[0,1]
 789 Param ELEMENTOPTSETS = 0         range=[0,1]
 790 Param ELEMENTOPT = 1     range=[0,1]
 791 Param PROXYVARIABLE = 2          range=[1,5]
 792 Received score 64581603603.000000
 793 Mutating 1 settings
 794 &&&&&&&&Mutating&&&&&&&
 795 Param ELEMENTOPTSETS = 1         range=[0,1]
 796 &&&&&&&&&&&&&&&&&&&&&&&
 797 **********************
 798 Polarity time: 0.003630
 799 Preprocess time: 0.000014
 800 Decompose Order: 0.000004
 801 Encoding Graph Time: 0.072271
 802 Elapse Encode time: 0.150898
 803 Is problem UNSAT after encoding: 0
 804 CNF Encode time: 0.000000
 805 SAT Solving time: 82.865470
 806 Result Computed in SAT solver:  SAT
 807 CSOLVER solve time: 83.016377
 808 Param PREPROCESS = 0     range=[0,1]
 809 Param ELEMENTOPTSETS = 1         range=[0,1]
 810 Param ELEMENTOPT = 1     range=[0,1]
 811 Param PROXYVARIABLE = 2          range=[1,5]
 812 Received score 83016377277.000000
 813 Mutating 1 settings
 814 &&&&&&&&Mutating&&&&&&&
 815 Param ELEMENTOPTSETS = 1         range=[0,1]
 816 &&&&&&&&&&&&&&&&&&&&&&&
 817 **********************
 818 Polarity time: 0.003621
 819 Preprocess time: 0.000015
 820 Decompose Order: 0.000004
 821 Encoding Graph Time: 0.069953
 822 Elapse Encode time: 0.148476
 823 Is problem UNSAT after encoding: 0
 824 CNF Encode time: 0.000000
 825 SAT Solving time: 84.333331
 826 Result Computed in SAT solver:  SAT
 827 CSOLVER solve time: 84.481840
 828 Param PREPROCESS = 0     range=[0,1]
 829 Param ELEMENTOPTSETS = 1         range=[0,1]
 830 Param ELEMENTOPT = 1     range=[0,1]
 831 Param PROXYVARIABLE = 2          range=[1,5]
 832 Received score 84481839508.000000
 833 Mutating 1 settings
 834 &&&&&&&&Mutating&&&&&&&
 835 Param PROXYVARIABLE = 3          range=[1,5]
 836 &&&&&&&&&&&&&&&&&&&&&&&
 837 **********************
 838 Polarity time: 0.003643
 839 Preprocess time: 0.000014
 840 Decompose Order: 0.000003
 841 Encoding Graph Time: 0.036907
 842 Elapse Encode time: 0.985214
 843 Is problem UNSAT after encoding: 0
 844 CNF Encode time: 0.000000
 845 SAT Solving time: 31.198388
 846 Result Computed in SAT solver:  SAT
 847 CSOLVER solve time: 32.183612
 848 Param PREPROCESS = 0     range=[0,1]
 849 Param ELEMENTOPTSETS = 0         range=[0,1]
 850 Param ELEMENTOPT = 1     range=[0,1]
 851 Param PROXYVARIABLE = 3          range=[1,5]
 852 Received score 32183612381.000000
 853 Mutating 1 settings
 854 &&&&&&&&Mutating&&&&&&&
 855 Param PROXYVARIABLE = 1          range=[1,5]
 856 &&&&&&&&&&&&&&&&&&&&&&&
 857 **********************
 858 Polarity time: 0.003617
 859 Preprocess time: 0.000014
 860 Decompose Order: 0.000003
 861 Encoding Graph Time: 0.037008
 862 Elapse Encode time: 0.990691
 863 Is problem UNSAT after encoding: 0
 864 CNF Encode time: 0.000000
 865 SAT Solving time: 8.581465
 866 Result Computed in SAT solver:  SAT
 867 CSOLVER solve time: 9.572166
 868 Param PREPROCESS = 0     range=[0,1]
 869 Param ELEMENTOPTSETS = 0         range=[0,1]
 870 Param ELEMENTOPT = 1     range=[0,1]
 871 Param PROXYVARIABLE = 1          range=[1,5]
 872 Received score 9572165776.000000
 873 Mutating 1 settings
 874 &&&&&&&&Mutating&&&&&&&
 875 Param ELEMENTOPTSETS = 1         range=[0,1]
 876 &&&&&&&&&&&&&&&&&&&&&&&
 877 **********************
 878 Polarity time: 0.003619
 879 Preprocess time: 0.000013
 880 Decompose Order: 0.000003
 881 Encoding Graph Time: 0.069792
 882 Elapse Encode time: 0.148374
 883 Is problem UNSAT after encoding: 0
 884 CNF Encode time: 0.000000
 885 SAT Solving time: 82.737560
 886 Result Computed in SAT solver:  SAT
 887 CSOLVER solve time: 82.885944
 888 Param PREPROCESS = 0     range=[0,1]
 889 Param ELEMENTOPTSETS = 1         range=[0,1]
 890 Param ELEMENTOPT = 1     range=[0,1]
 891 Param PROXYVARIABLE = 1          range=[1,5]
 892 Received score 82885943714.000000
 893 Mutating 1 settings
 894 &&&&&&&&Mutating&&&&&&&
 895 Param ELEMENTOPT = 0     range=[0,1]
 896 &&&&&&&&&&&&&&&&&&&&&&&
 897 **********************
 898 Polarity time: 0.003604
 899 Preprocess time: 0.000013
 900 Decompose Order: 0.000003
 901 Encoding Graph Time: 0.004465
 902 Elapse Encode time: 3.380603
 903 Is problem UNSAT after encoding: 0
 904 CNF Encode time: 0.000000
 905 SAT Solving time: 87.755807
 906 Result Computed in SAT solver:  SAT
 907 CSOLVER solve time: 91.136419
 908 Param PREPROCESS = 0     range=[0,1]
 909 Param ELEMENTOPTSETS = 0         range=[0,1]
 910 Param ELEMENTOPT = 0     range=[0,1]
 911 Param PROXYVARIABLE = 1          range=[1,5]
 912 Received score 91136419414.000000
 913 Mutating 1 settings
 914 &&&&&&&&Mutating&&&&&&&
 915 Param PREPROCESS = 1     range=[0,1]
 916 &&&&&&&&&&&&&&&&&&&&&&&
 917 **********************
 918 Polarity time: 0.003638
 919 Preprocess time: 0.011222
 920 Decompose Order: 0.000006
 921 Encoding Graph Time: 0.037182
 922 Elapse Encode time: 1.000609
 923 Is problem UNSAT after encoding: 0
 924 CNF Encode time: 0.000000
 925 SAT Solving time: 33.460618
 926 Result Computed in SAT solver:  SAT
 927 CSOLVER solve time: 34.461239
 928 Param PREPROCESS = 1     range=[0,1]
 929 Param ELEMENTOPTSETS = 0         range=[0,1]
 930 Param ELEMENTOPT = 1     range=[0,1]
 931 Param PROXYVARIABLE = 1          range=[1,5]
 932 Received score 34461238672.000000
 933 Mutating 1 settings
 934 &&&&&&&&Mutating&&&&&&&
 935 Param PREPROCESS = 1     range=[0,1]
 936 &&&&&&&&&&&&&&&&&&&&&&&
 937 **********************
 938 Polarity time: 0.003627
 939 Preprocess time: 0.011277
 940 Decompose Order: 0.000006
 941 Encoding Graph Time: 0.037141
 942 Elapse Encode time: 1.000240
 943 Is problem UNSAT after encoding: 0
 944 CNF Encode time: 0.000000
 945 SAT Solving time: 62.286329
 946 Result Computed in SAT solver:  SAT
 947 CSOLVER solve time: 63.286580
 948 Param PREPROCESS = 1     range=[0,1]
 949 Param ELEMENTOPTSETS = 0         range=[0,1]
 950 Param ELEMENTOPT = 1     range=[0,1]
 951 Param PROXYVARIABLE = 1          range=[1,5]
 952 Received score 63286579834.000000
 953 Mutating 1 settings
 954 &&&&&&&&Mutating&&&&&&&
 955 Param PROXYVARIABLE = 4          range=[1,5]
 956 &&&&&&&&&&&&&&&&&&&&&&&
 957 **********************
 958 Polarity time: 0.003603
 959 Preprocess time: 0.000013
 960 Decompose Order: 0.000004
 961 Encoding Graph Time: 0.036952
 962 Elapse Encode time: 0.989766
 963 Is problem UNSAT after encoding: 0
 964 CNF Encode time: 0.000000
 965 SAT Solving time: 41.587196
 966 Result Computed in SAT solver:  SAT
 967 CSOLVER solve time: 42.576994
 968 Param PREPROCESS = 0     range=[0,1]
 969 Param ELEMENTOPTSETS = 0         range=[0,1]
 970 Param ELEMENTOPT = 1     range=[0,1]
 971 Param PROXYVARIABLE = 4          range=[1,5]
 972 Received score 42576994380.000000
 973 Mutating 1 settings
 974 &&&&&&&&Mutating&&&&&&&
 975 Param PREPROCESS = 1     range=[0,1]
 976 &&&&&&&&&&&&&&&&&&&&&&&
 977 **********************
 978 Polarity time: 0.003607
 979 Preprocess time: 0.011245
 980 Decompose Order: 0.000007
 981 Encoding Graph Time: 0.037129
 982 Elapse Encode time: 0.999497
 983 Is problem UNSAT after encoding: 0
 984 CNF Encode time: 0.000000
 985 SAT Solving time: 8.630406
 986 Result Computed in SAT solver:  SAT
 987 CSOLVER solve time: 9.629913
 988 Param PREPROCESS = 1     range=[0,1]
 989 Param ELEMENTOPTSETS = 0         range=[0,1]
 990 Param ELEMENTOPT = 1     range=[0,1]
 991 Param PROXYVARIABLE = 1          range=[1,5]
 992 Received score 9629913404.000000
 993 Mutating 1 settings
 994 &&&&&&&&Mutating&&&&&&&
 995 Param ELEMENTOPTSETS = 1         range=[0,1]
 996 &&&&&&&&&&&&&&&&&&&&&&&
 997 **********************
 998 Polarity time: 0.003554
 999 Preprocess time: 0.011257
1000 Decompose Order: 0.000006
1001 Encoding Graph Time: 0.070039
1002 Elapse Encode time: 0.159810
1003 Is problem UNSAT after encoding: 0
1004 CNF Encode time: 0.000000
1005 SAT Solving time: 83.135095
1006 Result Computed in SAT solver:  SAT
1007 CSOLVER solve time: 83.294914
1008 Param PREPROCESS = 1     range=[0,1]
1009 Param ELEMENTOPTSETS = 1         range=[0,1]
1010 Param ELEMENTOPT = 1     range=[0,1]
1011 Param PROXYVARIABLE = 1          range=[1,5]
1012 Received score 83294914257.000000
1013 Mutating 1 settings
1014 &&&&&&&&Mutating&&&&&&&
1015 Param ELEMENTOPT = 0     range=[0,1]
1016 &&&&&&&&&&&&&&&&&&&&&&&
1017 **********************
1018 Polarity time: 0.003584
1019 Preprocess time: 0.011227
1020 Decompose Order: 0.000007
1021 Encoding Graph Time: 0.004614
1022 Elapse Encode time: 3.385892
1023 Is problem UNSAT after encoding: 0
1024 CNF Encode time: 0.000000
1025 SAT Solving time: 49.465540
1026 Result Computed in SAT solver:  SAT
1027 CSOLVER solve time: 52.851444
1028 Param PREPROCESS = 1     range=[0,1]
1029 Param ELEMENTOPTSETS = 0         range=[0,1]
1030 Param ELEMENTOPT = 0     range=[0,1]
1031 Param PROXYVARIABLE = 1          range=[1,5]
1032 Received score 52851443742.000000
1033 Mutating 1 settings
1034 &&&&&&&&Mutating&&&&&&&
1035 Param PROXYVARIABLE = 3          range=[1,5]
1036 &&&&&&&&&&&&&&&&&&&&&&&
1037 **********************
1038 Polarity time: 0.003613
1039 Preprocess time: 0.011217
1040 Decompose Order: 0.000006
1041 Encoding Graph Time: 0.037257
1042 Elapse Encode time: 1.000259
1043 Is problem UNSAT after encoding: 0
1044 CNF Encode time: 0.000000
1045 SAT Solving time: 30.583907
1046 Result Computed in SAT solver:  SAT
1047 CSOLVER solve time: 31.584177
1048 Param PREPROCESS = 1     range=[0,1]
1049 Param ELEMENTOPTSETS = 0         range=[0,1]
1050 Param ELEMENTOPT = 1     range=[0,1]
1051 Param PROXYVARIABLE = 3          range=[1,5]
1052 Received score 31584177331.000000
1053 Mutating 1 settings
1054 &&&&&&&&Mutating&&&&&&&
1055 Param PROXYVARIABLE = 2          range=[1,5]
1056 &&&&&&&&&&&&&&&&&&&&&&&
1057 **********************
1058 Polarity time: 0.003614
1059 Preprocess time: 0.011239
1060 Decompose Order: 0.000006
1061 Encoding Graph Time: 0.037056
1062 Elapse Encode time: 0.997787
1063 Is problem UNSAT after encoding: 0
1064 CNF Encode time: 0.000000
1065 SAT Solving time: 20.157703
1066 Result Computed in SAT solver:  SAT
1067 CSOLVER solve time: 21.155500
1068 Param PREPROCESS = 1     range=[0,1]
1069 Param ELEMENTOPTSETS = 0         range=[0,1]
1070 Param ELEMENTOPT = 1     range=[0,1]
1071 Param PROXYVARIABLE = 2          range=[1,5]
1072 Received score 21155500433.000000
1073 Mutating 1 settings
1074 &&&&&&&&Mutating&&&&&&&
1075 Param PREPROCESS = 0     range=[0,1]
1076 &&&&&&&&&&&&&&&&&&&&&&&
1077 **********************
1078 Polarity time: 0.003621
1079 Preprocess time: 0.000013
1080 Decompose Order: 0.000004
1081 Encoding Graph Time: 0.036958
1082 Elapse Encode time: 0.988231
1083 Is problem UNSAT after encoding: 0
1084 CNF Encode time: 0.000000
1085 SAT Solving time: 8.732493
1086 Result Computed in SAT solver:  SAT
1087 CSOLVER solve time: 9.720734
1088 Param PREPROCESS = 0     range=[0,1]
1089 Param ELEMENTOPTSETS = 0         range=[0,1]
1090 Param ELEMENTOPT = 1     range=[0,1]
1091 Param PROXYVARIABLE = 2          range=[1,5]
1092 Received score 9720733973.000000
1093 Mutating 1 settings
1094 &&&&&&&&Mutating&&&&&&&
1095 Param ELEMENTOPTSETS = 1         range=[0,1]
1096 &&&&&&&&&&&&&&&&&&&&&&&
1097 **********************
1098 Polarity time: 0.003620
1099 Preprocess time: 0.000015
1100 Decompose Order: 0.000029
1101 Encoding Graph Time: 0.069906
1102 Elapse Encode time: 0.148470
1103 Is problem UNSAT after encoding: 0
1104 CNF Encode time: 0.000000
1105 SAT Solving time: 82.287290
1106 Result Computed in SAT solver:  SAT
1107 CSOLVER solve time: 82.435769
1108 Param PREPROCESS = 0     range=[0,1]
1109 Param ELEMENTOPTSETS = 1         range=[0,1]
1110 Param ELEMENTOPT = 1     range=[0,1]
1111 Param PROXYVARIABLE = 2          range=[1,5]
1112 Received score 82435769331.000000
1113 Mutating 1 settings
1114 &&&&&&&&Mutating&&&&&&&
1115 Param PREPROCESS = 1     range=[0,1]
1116 &&&&&&&&&&&&&&&&&&&&&&&
1117 **********************
1118 Polarity time: 0.003585
1119 Preprocess time: 0.011204
1120 Decompose Order: 0.000007
1121 Encoding Graph Time: 0.037049
1122 Elapse Encode time: 0.997449
1123 Is problem UNSAT after encoding: 0
1124 CNF Encode time: 0.000000
1125 SAT Solving time: 33.548497
1126 Result Computed in SAT solver:  SAT
1127 CSOLVER solve time: 34.545956
1128 Param PREPROCESS = 1     range=[0,1]
1129 Param ELEMENTOPTSETS = 0         range=[0,1]
1130 Param ELEMENTOPT = 1     range=[0,1]
1131 Param PROXYVARIABLE = 2          range=[1,5]
1132 Received score 34545955994.000000
1133 Mutating 1 settings
1134 &&&&&&&&Mutating&&&&&&&
1135 Param PROXYVARIABLE = 1          range=[1,5]
1136 &&&&&&&&&&&&&&&&&&&&&&&
1137 **********************
1138 Polarity time: 0.003584
1139 Preprocess time: 0.011194
1140 Decompose Order: 0.000006
1141 Encoding Graph Time: 0.037103
1142 Elapse Encode time: 0.996823
1143 Is problem UNSAT after encoding: 0
1144 CNF Encode time: 0.000000
1145 SAT Solving time: 68.995219
1146 Result Computed in SAT solver:  SAT
1147 CSOLVER solve time: 69.992053
1148 Param PREPROCESS = 1     range=[0,1]
1149 Param ELEMENTOPTSETS = 0         range=[0,1]
1150 Param ELEMENTOPT = 1     range=[0,1]
1151 Param PROXYVARIABLE = 1          range=[1,5]
1152 Received score 69992053363.000000
1153 Mutating 1 settings
1154 &&&&&&&&Mutating&&&&&&&
1155 Param PROXYVARIABLE = 5          range=[1,5]
1156 &&&&&&&&&&&&&&&&&&&&&&&
1157 **********************
1158 Polarity time: 0.003595
1159 Preprocess time: 0.011199
1160 Decompose Order: 0.000006
1161 Encoding Graph Time: 0.037157
1162 Elapse Encode time: 0.998137
1163 Is problem UNSAT after encoding: 0
1164 CNF Encode time: 0.000000
1165 SAT Solving time: 41.424740
1166 Result Computed in SAT solver:  SAT
1167 CSOLVER solve time: 42.422888
1168 Param PREPROCESS = 1     range=[0,1]
1169 Param ELEMENTOPTSETS = 0         range=[0,1]
1170 Param ELEMENTOPT = 1     range=[0,1]
1171 Param PROXYVARIABLE = 5          range=[1,5]
1172 Received score 42422888244.000000
1173 Mutating 1 settings
1174 &&&&&&&&Mutating&&&&&&&
1175 Param PROXYVARIABLE = 1          range=[1,5]
1176 &&&&&&&&&&&&&&&&&&&&&&&
1177 **********************
1178 Polarity time: 0.004368
1179 Preprocess time: 0.015122
1180 Decompose Order: 0.000006
1181 Encoding Graph Time: 0.041379
1182 Elapse Encode time: 1.006678
1183 Is problem UNSAT after encoding: 0
1184 CNF Encode time: 0.000000
1185 SAT Solving time: 33.812083
1186 Result Computed in SAT solver:  SAT
1187 CSOLVER solve time: 34.818771
1188 Param PREPROCESS = 1     range=[0,1]
1189 Param ELEMENTOPTSETS = 0         range=[0,1]
1190 Param ELEMENTOPT = 1     range=[0,1]
1191 Param PROXYVARIABLE = 1          range=[1,5]
1192 Received score 34818770810.000000
1193 Mutating 1 settings
1194 &&&&&&&&Mutating&&&&&&&
1195 Param PROXYVARIABLE = 3          range=[1,5]
1196 &&&&&&&&&&&&&&&&&&&&&&&
1197 **********************
1198 Polarity time: 0.003610
1199 Preprocess time: 0.011172
1200 Decompose Order: 0.000007
1201 Encoding Graph Time: 0.037203
1202 Elapse Encode time: 0.997866
1203 Is problem UNSAT after encoding: 0
1204 CNF Encode time: 0.000000
1205 SAT Solving time: 27.557825
1206 Result Computed in SAT solver:  SAT
1207 CSOLVER solve time: 28.555701
1208 Param PREPROCESS = 1     range=[0,1]
1209 Param ELEMENTOPTSETS = 0         range=[0,1]
1210 Param ELEMENTOPT = 1     range=[0,1]
1211 Param PROXYVARIABLE = 3          range=[1,5]
1212 Received score 28555701251.000000
1213 Mutating 1 settings
1214 &&&&&&&&Mutating&&&&&&&
1215 Param PROXYVARIABLE = 5          range=[1,5]
1216 &&&&&&&&&&&&&&&&&&&&&&&
1217 **********************
1218 Polarity time: 0.004360
1219 Preprocess time: 0.015019
1220 Decompose Order: 0.000006
1221 Encoding Graph Time: 0.038774
1222 Elapse Encode time: 1.004089
1223 Is problem UNSAT after encoding: 0
1224 CNF Encode time: 0.000000
1225 SAT Solving time: 63.353451
1226 Result Computed in SAT solver:  SAT
1227 CSOLVER solve time: 64.357551
1228 Param PREPROCESS = 1     range=[0,1]
1229 Param ELEMENTOPTSETS = 0         range=[0,1]
1230 Param ELEMENTOPT = 1     range=[0,1]
1231 Param PROXYVARIABLE = 5          range=[1,5]
1232 Received score 64357550500.000000
1233 Mutating 1 settings
1234 &&&&&&&&Mutating&&&&&&&
1235 Param ELEMENTOPTSETS = 1         range=[0,1]
1236 &&&&&&&&&&&&&&&&&&&&&&&
1237 **********************
1238 Polarity time: 0.004250
1239 Preprocess time: 0.014777
1240 Decompose Order: 0.000006
1241 Encoding Graph Time: 0.074700
1242 Elapse Encode time: 0.169764
1243 Is problem UNSAT after encoding: 0
1244 CNF Encode time: 0.000000
1245 SAT Solving time: 86.908366
1246 Result Computed in SAT solver:  SAT
1247 CSOLVER solve time: 87.078139
1248 Param PREPROCESS = 1     range=[0,1]
1249 Param ELEMENTOPTSETS = 1         range=[0,1]
1250 Param ELEMENTOPT = 1     range=[0,1]
1251 Param PROXYVARIABLE = 3          range=[1,5]
1252 Received score 87078139342.000000
1253 Mutating 1 settings
1254 &&&&&&&&Mutating&&&&&&&
1255 Param ELEMENTOPTSETS = 1         range=[0,1]
1256 &&&&&&&&&&&&&&&&&&&&&&&
1257 **********************
1258 Polarity time: 0.004352
1259 Preprocess time: 0.014943
1260 Decompose Order: 0.000006
1261 Encoding Graph Time: 0.074774
1262 Elapse Encode time: 0.169911
1263 Is problem UNSAT after encoding: 0
1264 CNF Encode time: 0.000000
1265 SAT Solving time: 86.319313
1266 Result Computed in SAT solver:  SAT
1267 CSOLVER solve time: 86.489234
1268 Param PREPROCESS = 1     range=[0,1]
1269 Param ELEMENTOPTSETS = 1         range=[0,1]
1270 Param ELEMENTOPT = 1     range=[0,1]
1271 Param PROXYVARIABLE = 3          range=[1,5]
1272 Received score 86489233627.000000
1273 Mutating 1 settings
1274 &&&&&&&&Mutating&&&&&&&
1275 Param ELEMENTOPTSETS = 1         range=[0,1]
1276 &&&&&&&&&&&&&&&&&&&&&&&
1277 **********************
1278 Polarity time: 0.003597
1279 Preprocess time: 0.011123
1280 Decompose Order: 0.000007
1281 Encoding Graph Time: 0.070011
1282 Elapse Encode time: 0.159512
1283 Is problem UNSAT after encoding: 0
1284 CNF Encode time: 0.000000
1285 SAT Solving time: 82.454700
1286 Result Computed in SAT solver:  SAT
1287 CSOLVER solve time: 82.614221
1288 Param PREPROCESS = 1     range=[0,1]
1289 Param ELEMENTOPTSETS = 1         range=[0,1]
1290 Param ELEMENTOPT = 1     range=[0,1]
1291 Param PROXYVARIABLE = 3          range=[1,5]
1292 Received score 82614221500.000000
1293 Mutating 1 settings
1294 &&&&&&&&Mutating&&&&&&&
1295 Param PROXYVARIABLE = 5          range=[1,5]
1296 &&&&&&&&&&&&&&&&&&&&&&&
1297 **********************
1298 Polarity time: 0.003651
1299 Preprocess time: 0.011092
1300 Decompose Order: 0.000006
1301 Encoding Graph Time: 0.037092
1302 Elapse Encode time: 1.000286
1303 Is problem UNSAT after encoding: 0
1304 CNF Encode time: 0.000000
1305 SAT Solving time: 71.853457
1306 Result Computed in SAT solver:  SAT
1307 CSOLVER solve time: 72.853754
1308 Param PREPROCESS = 1     range=[0,1]
1309 Param ELEMENTOPTSETS = 0         range=[0,1]
1310 Param ELEMENTOPT = 1     range=[0,1]
1311 Param PROXYVARIABLE = 5          range=[1,5]
1312 Received score 72853753763.000000
1313 Mutating 1 settings
1314 &&&&&&&&Mutating&&&&&&&
1315 Param ELEMENTOPTSETS = 1         range=[0,1]
1316 &&&&&&&&&&&&&&&&&&&&&&&
1317 **********************
1318 Polarity time: 0.003643
1319 Preprocess time: 0.011101
1320 Decompose Order: 0.000006
1321 Encoding Graph Time: 0.070230
1322 Elapse Encode time: 0.159777
1323 Is problem UNSAT after encoding: 0
1324 CNF Encode time: 0.000000
1325 SAT Solving time: 84.719625
1326 Result Computed in SAT solver:  SAT
1327 CSOLVER solve time: 84.879412
1328 Param PREPROCESS = 1     range=[0,1]
1329 Param ELEMENTOPTSETS = 1         range=[0,1]
1330 Param ELEMENTOPT = 1     range=[0,1]
1331 Param PROXYVARIABLE = 3          range=[1,5]
1332 Received score 84879411582.000000
1333 Mutating 1 settings
1334 &&&&&&&&Mutating&&&&&&&
1335 Param PROXYVARIABLE = 5          range=[1,5]
1336 &&&&&&&&&&&&&&&&&&&&&&&
1337 **********************
1338 Polarity time: 0.003634
1339 Preprocess time: 0.011164
1340 Decompose Order: 0.000007
1341 Encoding Graph Time: 0.037201
1342 Elapse Encode time: 0.997829
1343 Is problem UNSAT after encoding: 0
1344 CNF Encode time: 0.000000
1345 SAT Solving time: 51.114738
1346 Result Computed in SAT solver:  SAT
1347 CSOLVER solve time: 52.112578
1348 Param PREPROCESS = 1     range=[0,1]
1349 Param ELEMENTOPTSETS = 0         range=[0,1]
1350 Param ELEMENTOPT = 1     range=[0,1]
1351 Param PROXYVARIABLE = 5          range=[1,5]
1352 Received score 52112578141.000000
1353 Mutating 1 settings
1354 &&&&&&&&Mutating&&&&&&&
1355 Param ELEMENTOPT = 0     range=[0,1]
1356 &&&&&&&&&&&&&&&&&&&&&&&
1357 **********************
1358 Polarity time: 0.003674
1359 Preprocess time: 0.011182
1360 Decompose Order: 0.000007
1361 Encoding Graph Time: 0.004689
1362 Elapse Encode time: 3.383206
1363 Is problem UNSAT after encoding: 0
1364 CNF Encode time: 0.000000
1365 SAT Solving time: 114.611367
1366 Result Computed in SAT solver:  SAT
1367 CSOLVER solve time: 117.994583
1368 Param PREPROCESS = 1     range=[0,1]
1369 Param ELEMENTOPTSETS = 0         range=[0,1]
1370 Param ELEMENTOPT = 0     range=[0,1]
1371 Param PROXYVARIABLE = 3          range=[1,5]
1372 Received score 117994582967.000000
1373 Mutating 1 settings
1374 &&&&&&&&Mutating&&&&&&&
1375 Param PREPROCESS = 0     range=[0,1]
1376 &&&&&&&&&&&&&&&&&&&&&&&
1377 **********************
1378 Polarity time: 0.003620
1379 Preprocess time: 0.000014
1380 Decompose Order: 0.000004
1381 Encoding Graph Time: 0.036837
1382 Elapse Encode time: 0.985972
1383 Is problem UNSAT after encoding: 0
1384 CNF Encode time: 0.000000
1385 SAT Solving time: 46.478543
1386 Result Computed in SAT solver:  SAT
1387 CSOLVER solve time: 47.464525
1388 Param PREPROCESS = 0     range=[0,1]
1389 Param ELEMENTOPTSETS = 0         range=[0,1]
1390 Param ELEMENTOPT = 1     range=[0,1]
1391 Param PROXYVARIABLE = 3          range=[1,5]
1392 Received score 47464524931.000000
1393 Mutating 1 settings
1394 &&&&&&&&Mutating&&&&&&&
1395 Param PREPROCESS = 0     range=[0,1]
1396 &&&&&&&&&&&&&&&&&&&&&&&
1397 **********************
1398 Polarity time: 0.003605
1399 Preprocess time: 0.000016
1400 Decompose Order: 0.000003
1401 Encoding Graph Time: 0.036873
1402 Elapse Encode time: 0.986315
1403 Is problem UNSAT after encoding: 0
1404 CNF Encode time: 0.000000
1405 SAT Solving time: 40.200536
1406 Result Computed in SAT solver:  SAT
1407 CSOLVER solve time: 41.186862
1408 Param PREPROCESS = 0     range=[0,1]
1409 Param ELEMENTOPTSETS = 0         range=[0,1]
1410 Param ELEMENTOPT = 1     range=[0,1]
1411 Param PROXYVARIABLE = 3          range=[1,5]
1412 Received score 41186862150.000000
1413 Mutating 1 settings
1414 &&&&&&&&Mutating&&&&&&&
1415 Param ELEMENTOPTSETS = 1         range=[0,1]
1416 &&&&&&&&&&&&&&&&&&&&&&&
1417 **********************
1418 Polarity time: 0.003663
1419 Preprocess time: 0.011276
1420 Decompose Order: 0.000007
1421 Encoding Graph Time: 0.070148
1422 Elapse Encode time: 0.159843
1423 Is problem UNSAT after encoding: 0
1424 CNF Encode time: 0.000000
1425 SAT Solving time: 82.375232
1426 Result Computed in SAT solver:  SAT
1427 CSOLVER solve time: 82.535086
1428 Param PREPROCESS = 1     range=[0,1]
1429 Param ELEMENTOPTSETS = 1         range=[0,1]
1430 Param ELEMENTOPT = 1     range=[0,1]
1431 Param PROXYVARIABLE = 3          range=[1,5]
1432 Received score 82535085668.000000
1433 Mutating 1 settings
1434 &&&&&&&&Mutating&&&&&&&
1435 Param PROXYVARIABLE = 4          range=[1,5]
1436 &&&&&&&&&&&&&&&&&&&&&&&
1437 **********************
1438 Polarity time: 0.003602
1439 Preprocess time: 0.011101
1440 Decompose Order: 0.000006
1441 Encoding Graph Time: 0.037077
1442 Elapse Encode time: 0.999875
1443 Is problem UNSAT after encoding: 0
1444 CNF Encode time: 0.000000
1445 SAT Solving time: 14.009753
1446 Result Computed in SAT solver:  SAT
1447 CSOLVER solve time: 15.009639
1448 Param PREPROCESS = 1     range=[0,1]
1449 Param ELEMENTOPTSETS = 0         range=[0,1]
1450 Param ELEMENTOPT = 1     range=[0,1]
1451 Param PROXYVARIABLE = 4          range=[1,5]
1452 Received score 15009639361.000000
1453 Mutating 1 settings
1454 &&&&&&&&Mutating&&&&&&&
1455 Param ELEMENTOPT = 0     range=[0,1]
1456 &&&&&&&&&&&&&&&&&&&&&&&
1457 **********************
1458 Polarity time: 0.003622
1459 Preprocess time: 0.011201
1460 Decompose Order: 0.000006
1461 Encoding Graph Time: 0.004631
1462 Elapse Encode time: 3.384540
1463 Is problem UNSAT after encoding: 0
1464 CNF Encode time: 0.000000
1465 SAT Solving time: 75.543617
1466 Result Computed in SAT solver:  SAT
1467 CSOLVER solve time: 78.928167
1468 Param PREPROCESS = 1     range=[0,1]
1469 Param ELEMENTOPTSETS = 0         range=[0,1]
1470 Param ELEMENTOPT = 0     range=[0,1]
1471 Param PROXYVARIABLE = 4          range=[1,5]
1472 Received score 78928166995.000000
1473 Mutating 1 settings
1474 &&&&&&&&Mutating&&&&&&&
1475 Param ELEMENTOPTSETS = 1         range=[0,1]
1476 &&&&&&&&&&&&&&&&&&&&&&&
1477 **********************
1478 Polarity time: 0.003579
1479 Preprocess time: 0.011312
1480 Decompose Order: 0.000008
1481 Encoding Graph Time: 0.070124
1482 Elapse Encode time: 0.159894
1483 Is problem UNSAT after encoding: 0
1484 CNF Encode time: 0.000000
1485 SAT Solving time: 82.061831
1486 Result Computed in SAT solver:  SAT
1487 CSOLVER solve time: 82.221734
1488 Param PREPROCESS = 1     range=[0,1]
1489 Param ELEMENTOPTSETS = 1         range=[0,1]
1490 Param ELEMENTOPT = 1     range=[0,1]
1491 Param PROXYVARIABLE = 4          range=[1,5]
1492 Received score 82221734235.000000
1493 Mutating 1 settings
1494 &&&&&&&&Mutating&&&&&&&
1495 Param ELEMENTOPTSETS = 1         range=[0,1]
1496 &&&&&&&&&&&&&&&&&&&&&&&
1497 **********************
1498 Polarity time: 0.003551
1499 Preprocess time: 0.011259
1500 Decompose Order: 0.000007
1501 Encoding Graph Time: 0.070051
1502 Elapse Encode time: 0.159558
1503 Is problem UNSAT after encoding: 0
1504 CNF Encode time: 0.000000
1505 SAT Solving time: 82.256872
1506 Result Computed in SAT solver:  SAT
1507 CSOLVER solve time: 82.416439
1508 Param PREPROCESS = 1     range=[0,1]
1509 Param ELEMENTOPTSETS = 1         range=[0,1]
1510 Param ELEMENTOPT = 1     range=[0,1]
1511 Param PROXYVARIABLE = 4          range=[1,5]
1512 Received score 82416439048.000000
1513 Mutating 1 settings
1514 &&&&&&&&Mutating&&&&&&&
1515 Param ELEMENTOPT = 0     range=[0,1]
1516 &&&&&&&&&&&&&&&&&&&&&&&
1517 **********************
1518 Polarity time: 0.003593
1519 Preprocess time: 0.011235
1520 Decompose Order: 0.000007
1521 Encoding Graph Time: 0.004582
1522 Elapse Encode time: 3.389657
1523 Is problem UNSAT after encoding: 0
1524 CNF Encode time: 0.000000
1525 SAT Solving time: 16.307972
1526 Result Computed in SAT solver:  SAT
1527 CSOLVER solve time: 19.697641
1528 Param PREPROCESS = 1     range=[0,1]
1529 Param ELEMENTOPTSETS = 0         range=[0,1]
1530 Param ELEMENTOPT = 0     range=[0,1]
1531 Param PROXYVARIABLE = 4          range=[1,5]
1532 Received score 19697640893.000000
1533 Mutating 1 settings
1534 &&&&&&&&Mutating&&&&&&&
1535 Param ELEMENTOPT = 0     range=[0,1]
1536 &&&&&&&&&&&&&&&&&&&&&&&
1537 **********************
1538 Polarity time: 0.003576
1539 Preprocess time: 0.011259
1540 Decompose Order: 0.000006
1541 Encoding Graph Time: 0.004639
1542 Elapse Encode time: 3.385306
1543 Is problem UNSAT after encoding: 0
1544 CNF Encode time: 0.000000
1545 SAT Solving time: 16.035999
1546 Result Computed in SAT solver:  SAT
1547 CSOLVER solve time: 19.421316
1548 Param PREPROCESS = 1     range=[0,1]
1549 Param ELEMENTOPTSETS = 0         range=[0,1]
1550 Param ELEMENTOPT = 0     range=[0,1]
1551 Param PROXYVARIABLE = 4          range=[1,5]
1552 Received score 19421316493.000000
1553 Mutating 1 settings
1554 &&&&&&&&Mutating&&&&&&&
1555 Param PROXYVARIABLE = 5          range=[1,5]
1556 &&&&&&&&&&&&&&&&&&&&&&&
1557 **********************
1558 Polarity time: 0.003565
1559 Preprocess time: 0.011196
1560 Decompose Order: 0.000007
1561 Encoding Graph Time: 0.004553
1562 Elapse Encode time: 3.386017
1563 Is problem UNSAT after encoding: 0
1564 CNF Encode time: 0.000000
1565 SAT Solving time: 32.369498
1566 Result Computed in SAT solver:  SAT
1567 CSOLVER solve time: 35.755526
1568 Param PREPROCESS = 1     range=[0,1]
1569 Param ELEMENTOPTSETS = 0         range=[0,1]
1570 Param ELEMENTOPT = 0     range=[0,1]
1571 Param PROXYVARIABLE = 5          range=[1,5]
1572 Received score 35755525576.000000
1573 Mutating 1 settings
1574 &&&&&&&&Mutating&&&&&&&
1575 Param PREPROCESS = 0     range=[0,1]
1576 &&&&&&&&&&&&&&&&&&&&&&&
1577 **********************
1578 Polarity time: 0.003605
1579 Preprocess time: 0.000016
1580 Decompose Order: 0.000004
1581 Encoding Graph Time: 0.004501
1582 Elapse Encode time: 3.374840
1583 Is problem UNSAT after encoding: 0
1584 CNF Encode time: 0.000000
1585 SAT Solving time: 108.432511
1586 Result Computed in SAT solver:  SAT
1587 CSOLVER solve time: 111.807363
1588 Param PREPROCESS = 0     range=[0,1]
1589 Param ELEMENTOPTSETS = 0         range=[0,1]
1590 Param ELEMENTOPT = 0     range=[0,1]
1591 Param PROXYVARIABLE = 4          range=[1,5]
1592 Received score 111807362878.000000
1593 Mutating 1 settings
1594 &&&&&&&&Mutating&&&&&&&
1595 Param PREPROCESS = 0     range=[0,1]
1596 &&&&&&&&&&&&&&&&&&&&&&&
1597 **********************
1598 Polarity time: 0.003596
1599 Preprocess time: 0.000015
1600 Decompose Order: 0.000003
1601 Encoding Graph Time: 0.004528
1602 Elapse Encode time: 3.372506
1603 Is problem UNSAT after encoding: 0
1604 CNF Encode time: 0.000000
1605 SAT Solving time: 61.460759
1606 Result Computed in SAT solver:  SAT
1607 CSOLVER solve time: 64.833276
1608 Param PREPROCESS = 0     range=[0,1]
1609 Param ELEMENTOPTSETS = 0         range=[0,1]
1610 Param ELEMENTOPT = 0     range=[0,1]
1611 Param PROXYVARIABLE = 4          range=[1,5]
1612 Received score 64833276115.000000
1613 Mutating 1 settings
1614 &&&&&&&&Mutating&&&&&&&
1615 Param ELEMENTOPT = 1     range=[0,1]
1616 &&&&&&&&&&&&&&&&&&&&&&&
1617 **********************
1618 Polarity time: 0.003583
1619 Preprocess time: 0.011129
1620 Decompose Order: 0.000006
1621 Encoding Graph Time: 0.037114
1622 Elapse Encode time: 0.997624
1623 Is problem UNSAT after encoding: 0
1624 CNF Encode time: 0.000000
1625 SAT Solving time: 26.648506
1626 Result Computed in SAT solver:  SAT
1627 CSOLVER solve time: 27.646141
1628 Param PREPROCESS = 1     range=[0,1]
1629 Param ELEMENTOPTSETS = 0         range=[0,1]
1630 Param ELEMENTOPT = 1     range=[0,1]
1631 Param PROXYVARIABLE = 4          range=[1,5]
1632 Received score 27646140703.000000
1633 Mutating 1 settings
1634 &&&&&&&&Mutating&&&&&&&
1635 Param ELEMENTOPT = 1     range=[0,1]
1636 &&&&&&&&&&&&&&&&&&&&&&&
1637 **********************
1638 Polarity time: 0.003623
1639 Preprocess time: 0.011095
1640 Decompose Order: 0.000006
1641 Encoding Graph Time: 0.037181
1642 Elapse Encode time: 1.000318
1643 Is problem UNSAT after encoding: 0
1644 CNF Encode time: 0.000000
1645 SAT Solving time: 71.175752
1646 Result Computed in SAT solver:  SAT
1647 CSOLVER solve time: 72.176080
1648 Param PREPROCESS = 1     range=[0,1]
1649 Param ELEMENTOPTSETS = 0         range=[0,1]
1650 Param ELEMENTOPT = 1     range=[0,1]
1651 Param PROXYVARIABLE = 4          range=[1,5]
1652 Received score 72176079940.000000
1653 Mutating 1 settings
1654 &&&&&&&&Mutating&&&&&&&
1655 Param ELEMENTOPTSETS = 1         range=[0,1]
1656 &&&&&&&&&&&&&&&&&&&&&&&
1657 **********************
1658 Polarity time: 0.003619
1659 Preprocess time: 0.011116
1660 Decompose Order: 0.000006
1661 Encoding Graph Time: 0.004639
1662 Elapse Encode time: 3.385965
1663 Is problem UNSAT after encoding: 0
1664 CNF Encode time: 0.000000
1665 SAT Solving time: 16.013478
1666 Result Computed in SAT solver:  SAT
1667 CSOLVER solve time: 19.399454
1668 Param PREPROCESS = 1     range=[0,1]
1669 Param ELEMENTOPTSETS = 1         range=[0,1]
1670 Param ELEMENTOPT = 0     range=[0,1]
1671 Param PROXYVARIABLE = 4          range=[1,5]
1672 Received score 19399453559.000000
1673 Mutating 1 settings
1674 &&&&&&&&Mutating&&&&&&&
1675 Param ELEMENTOPT = 1     range=[0,1]
1676 &&&&&&&&&&&&&&&&&&&&&&&
1677 **********************
1678 Polarity time: 0.003562
1679 Preprocess time: 0.011236
1680 Decompose Order: 0.000006
1681 Encoding Graph Time: 0.070376
1682 Elapse Encode time: 0.160124
1683 Is problem UNSAT after encoding: 0
1684 CNF Encode time: 0.000000
1685 SAT Solving time: 83.829085
1686 Result Computed in SAT solver:  SAT
1687 CSOLVER solve time: 83.989220
1688 Param PREPROCESS = 1     range=[0,1]
1689 Param ELEMENTOPTSETS = 1         range=[0,1]
1690 Param ELEMENTOPT = 1     range=[0,1]
1691 Param PROXYVARIABLE = 4          range=[1,5]
1692 Received score 83989219554.000000
1693 Mutating 1 settings
1694 &&&&&&&&Mutating&&&&&&&
1695 Param PREPROCESS = 0     range=[0,1]
1696 &&&&&&&&&&&&&&&&&&&&&&&
1697 **********************
1698 Polarity time: 0.003630
1699 Preprocess time: 0.000014
1700 Decompose Order: 0.000004
1701 Encoding Graph Time: 0.004486
1702 Elapse Encode time: 3.382889
1703 Is problem UNSAT after encoding: 0
1704 CNF Encode time: 0.000000
1705 SAT Solving time: 15.896570
1706 Result Computed in SAT solver:  SAT
1707 CSOLVER solve time: 19.279470
1708 Param PREPROCESS = 0     range=[0,1]
1709 Param ELEMENTOPTSETS = 1         range=[0,1]
1710 Param ELEMENTOPT = 0     range=[0,1]
1711 Param PROXYVARIABLE = 4          range=[1,5]
1712 Received score 19279470399.000000
1713 Mutating 1 settings
1714 &&&&&&&&Mutating&&&&&&&
1715 Param ELEMENTOPT = 1     range=[0,1]
1716 &&&&&&&&&&&&&&&&&&&&&&&
1717 **********************
1718 Polarity time: 0.003534
1719 Preprocess time: 0.000015
1720 Decompose Order: 0.000003
1721 Encoding Graph Time: 0.069747
1722 Elapse Encode time: 0.148181
1723 Is problem UNSAT after encoding: 0
1724 CNF Encode time: 0.000000
1725 SAT Solving time: 82.512962
1726 Result Computed in SAT solver:  SAT
1727 CSOLVER solve time: 82.661153
1728 Param PREPROCESS = 0     range=[0,1]
1729 Param ELEMENTOPTSETS = 1         range=[0,1]
1730 Param ELEMENTOPT = 1     range=[0,1]
1731 Param PROXYVARIABLE = 4          range=[1,5]
1732 Received score 82661152628.000000
1733 Mutating 1 settings
1734 &&&&&&&&Mutating&&&&&&&
1735 Param PREPROCESS = 1     range=[0,1]
1736 &&&&&&&&&&&&&&&&&&&&&&&
1737 **********************
1738 Polarity time: 0.003597
1739 Preprocess time: 0.011241
1740 Decompose Order: 0.000006
1741 Encoding Graph Time: 0.004552
1742 Elapse Encode time: 3.390503
1743 Is problem UNSAT after encoding: 0
1744 CNF Encode time: 0.000000
1745 SAT Solving time: 16.391724
1746 Result Computed in SAT solver:  SAT
1747 CSOLVER solve time: 19.782237
1748 Param PREPROCESS = 1     range=[0,1]
1749 Param ELEMENTOPTSETS = 1         range=[0,1]
1750 Param ELEMENTOPT = 0     range=[0,1]
1751 Param PROXYVARIABLE = 4          range=[1,5]
1752 Received score 19782237090.000000
1753 Mutating 1 settings
1754 &&&&&&&&Mutating&&&&&&&
1755 Param ELEMENTOPT = 1     range=[0,1]
1756 &&&&&&&&&&&&&&&&&&&&&&&
1757 **********************
1758 Polarity time: 0.003606
1759 Preprocess time: 0.011243
1760 Decompose Order: 0.000006
1761 Encoding Graph Time: 0.069991
1762 Elapse Encode time: 0.159843
1763 Is problem UNSAT after encoding: 0
1764 CNF Encode time: 0.000000
1765 SAT Solving time: 82.459144
1766 Result Computed in SAT solver:  SAT
1767 CSOLVER solve time: 82.618996
1768 Param PREPROCESS = 1     range=[0,1]
1769 Param ELEMENTOPTSETS = 1         range=[0,1]
1770 Param ELEMENTOPT = 1     range=[0,1]
1771 Param PROXYVARIABLE = 4          range=[1,5]
1772 Received score 82618995928.000000
1773 Mutating 1 settings
1774 &&&&&&&&Mutating&&&&&&&
1775 Param ELEMENTOPT = 1     range=[0,1]
1776 &&&&&&&&&&&&&&&&&&&&&&&
1777 **********************
1778 Polarity time: 0.003619
1779 Preprocess time: 0.011217
1780 Decompose Order: 0.000007
1781 Encoding Graph Time: 0.069986
1782 Elapse Encode time: 0.159895
1783 Is problem UNSAT after encoding: 0
1784 CNF Encode time: 0.000000
1785 SAT Solving time: 82.789035
1786 Result Computed in SAT solver:  SAT
1787 CSOLVER solve time: 82.948966
1788 Param PREPROCESS = 1     range=[0,1]
1789 Param ELEMENTOPTSETS = 1         range=[0,1]
1790 Param ELEMENTOPT = 1     range=[0,1]
1791 Param PROXYVARIABLE = 4          range=[1,5]
1792 Received score 82948965952.000000
1793 Mutating 1 settings
1794 &&&&&&&&Mutating&&&&&&&
1795 Param PREPROCESS = 0     range=[0,1]
1796 &&&&&&&&&&&&&&&&&&&&&&&
1797 **********************
1798 Polarity time: 0.003641
1799 Preprocess time: 0.000014
1800 Decompose Order: 0.000004
1801 Encoding Graph Time: 0.004493
1802 Elapse Encode time: 3.379458
1803 Is problem UNSAT after encoding: 0
1804 CNF Encode time: 0.000000
1805 SAT Solving time: 16.152344
1806 Result Computed in SAT solver:  SAT
1807 CSOLVER solve time: 19.531813
1808 Param PREPROCESS = 0     range=[0,1]
1809 Param ELEMENTOPTSETS = 1         range=[0,1]
1810 Param ELEMENTOPT = 0     range=[0,1]
1811 Param PROXYVARIABLE = 4          range=[1,5]
1812 Received score 19531813164.000000
1813 Mutating 1 settings
1814 &&&&&&&&Mutating&&&&&&&
1815 Param PROXYVARIABLE = 3          range=[1,5]
1816 &&&&&&&&&&&&&&&&&&&&&&&
1817 **********************
1818 Polarity time: 0.003615
1819 Preprocess time: 0.000014
1820 Decompose Order: 0.000003
1821 Encoding Graph Time: 0.004428
1822 Elapse Encode time: 3.388834
1823 Is problem UNSAT after encoding: 0
1824 CNF Encode time: 0.000000
1825 SAT Solving time: 94.074652
1826 Result Computed in SAT solver:  SAT
1827 CSOLVER solve time: 97.463497
1828 Param PREPROCESS = 0     range=[0,1]
1829 Param ELEMENTOPTSETS = 1         range=[0,1]
1830 Param ELEMENTOPT = 0     range=[0,1]
1831 Param PROXYVARIABLE = 3          range=[1,5]
1832 Received score 97463497348.000000
1833 Mutating 1 settings
1834 &&&&&&&&Mutating&&&&&&&
1835 Param PROXYVARIABLE = 2          range=[1,5]
1836 &&&&&&&&&&&&&&&&&&&&&&&
1837 **********************
1838 Polarity time: 0.003597
1839 Preprocess time: 0.000014
1840 Decompose Order: 0.000003
1841 Encoding Graph Time: 0.004440
1842 Elapse Encode time: 3.379140
1843 Is problem UNSAT after encoding: 0
1844 CNF Encode time: 0.000000
1845 SAT Solving time: 71.074409
1846 Result Computed in SAT solver:  SAT
1847 CSOLVER solve time: 74.453559
1848 Param PREPROCESS = 0     range=[0,1]
1849 Param ELEMENTOPTSETS = 1         range=[0,1]
1850 Param ELEMENTOPT = 0     range=[0,1]
1851 Param PROXYVARIABLE = 2          range=[1,5]
1852 Received score 74453559426.000000
1853 Mutating 1 settings
1854 &&&&&&&&Mutating&&&&&&&
1855 Param ELEMENTOPTSETS = 0         range=[0,1]
1856 &&&&&&&&&&&&&&&&&&&&&&&
1857 **********************
1858 Polarity time: 0.004336
1859 Preprocess time: 0.000022
1860 Decompose Order: 0.000004
1861 Encoding Graph Time: 0.005427
1862 Elapse Encode time: 3.380403
1863 Is problem UNSAT after encoding: 0
1864 CNF Encode time: 0.000000
1865 SAT Solving time: 86.655901
1866 Result Computed in SAT solver:  SAT
1867 CSOLVER solve time: 90.036315
1868 Param PREPROCESS = 0     range=[0,1]
1869 Param ELEMENTOPTSETS = 0         range=[0,1]
1870 Param ELEMENTOPT = 0     range=[0,1]
1871 Param PROXYVARIABLE = 4          range=[1,5]
1872 Received score 90036314667.000000
1873 Mutating 1 settings
1874 &&&&&&&&Mutating&&&&&&&
1875 Param ELEMENTOPT = 1     range=[0,1]
1876 &&&&&&&&&&&&&&&&&&&&&&&
1877 **********************
1878 Polarity time: 0.004355
1879 Preprocess time: 0.000016
1880 Decompose Order: 0.000003
1881 Encoding Graph Time: 0.074442
1882 Elapse Encode time: 0.154603
1883 Is problem UNSAT after encoding: 0
1884 CNF Encode time: 0.000000
1885 SAT Solving time: 82.257309
1886 Result Computed in SAT solver:  SAT
1887 CSOLVER solve time: 82.411922
1888 Param PREPROCESS = 0     range=[0,1]
1889 Param ELEMENTOPTSETS = 1         range=[0,1]
1890 Param ELEMENTOPT = 1     range=[0,1]
1891 Param PROXYVARIABLE = 4          range=[1,5]
1892 Received score 82411922080.000000
1893 Mutating 1 settings
1894 &&&&&&&&Mutating&&&&&&&
1895 Param PROXYVARIABLE = 2          range=[1,5]
1896 &&&&&&&&&&&&&&&&&&&&&&&
1897 **********************
1898 Polarity time: 0.004289
1899 Preprocess time: 0.000014
1900 Decompose Order: 0.000003
1901 Encoding Graph Time: 0.005336
1902 Elapse Encode time: 3.391593
1903 Is problem UNSAT after encoding: 0
1904 CNF Encode time: 0.000000
1905 SAT Solving time: 87.475675
1906 Result Computed in SAT solver:  SAT
1907 CSOLVER solve time: 90.867278
1908 Param PREPROCESS = 0     range=[0,1]
1909 Param ELEMENTOPTSETS = 1         range=[0,1]
1910 Param ELEMENTOPT = 0     range=[0,1]
1911 Param PROXYVARIABLE = 2          range=[1,5]
1912 Received score 90867278483.000000
1913 Mutating 1 settings
1914 &&&&&&&&Mutating&&&&&&&
1915 Param PREPROCESS = 1     range=[0,1]
1916 &&&&&&&&&&&&&&&&&&&&&&&
1917 **********************
1918 Polarity time: 0.003639
1919 Preprocess time: 0.011204
1920 Decompose Order: 0.000006
1921 Encoding Graph Time: 0.004632
1922 Elapse Encode time: 3.383923
1923 Is problem UNSAT after encoding: 0
1924 CNF Encode time: 0.000000
1925 SAT Solving time: 16.068230
1926 Result Computed in SAT solver:  SAT
1927 CSOLVER solve time: 19.452165
1928 Param PREPROCESS = 1     range=[0,1]
1929 Param ELEMENTOPTSETS = 1         range=[0,1]
1930 Param ELEMENTOPT = 0     range=[0,1]
1931 Param PROXYVARIABLE = 4          range=[1,5]
1932 Received score 19452165317.000000
1933 Mutating 1 settings
1934 &&&&&&&&Mutating&&&&&&&
1935 Param ELEMENTOPTSETS = 0         range=[0,1]
1936 &&&&&&&&&&&&&&&&&&&&&&&
1937 **********************
1938 Polarity time: 0.004319
1939 Preprocess time: 0.014972
1940 Decompose Order: 0.000007
1941 Encoding Graph Time: 0.005565
1942 Elapse Encode time: 3.398950
1943 Is problem UNSAT after encoding: 0
1944 CNF Encode time: 0.000000
1945 SAT Solving time: 59.972419
1946 Result Computed in SAT solver:  SAT
1947 CSOLVER solve time: 63.371381
1948 Param PREPROCESS = 1     range=[0,1]
1949 Param ELEMENTOPTSETS = 0         range=[0,1]
1950 Param ELEMENTOPT = 0     range=[0,1]
1951 Param PROXYVARIABLE = 4          range=[1,5]
1952 Received score 63371380931.000000
1953 Mutating 1 settings
1954 &&&&&&&&Mutating&&&&&&&
1955 Param PROXYVARIABLE = 3          range=[1,5]
1956 &&&&&&&&&&&&&&&&&&&&&&&
1957 **********************
1958 Polarity time: 0.004375
1959 Preprocess time: 0.015001
1960 Decompose Order: 0.000006
1961 Encoding Graph Time: 0.005624
1962 Elapse Encode time: 3.401645
1963 Is problem UNSAT after encoding: 0
1964 CNF Encode time: 0.000000
1965 SAT Solving time: 72.692053
1966 Result Computed in SAT solver:  SAT
1967 CSOLVER solve time: 76.093709
1968 Param PREPROCESS = 1     range=[0,1]
1969 Param ELEMENTOPTSETS = 1         range=[0,1]
1970 Param ELEMENTOPT = 0     range=[0,1]
1971 Param PROXYVARIABLE = 3          range=[1,5]
1972 Received score 76093708689.000000
1973 Mutating 1 settings
1974 &&&&&&&&Mutating&&&&&&&
1975 Param PREPROCESS = 0     range=[0,1]
1976 &&&&&&&&&&&&&&&&&&&&&&&
1977 **********************
1978 Polarity time: 0.004366
1979 Preprocess time: 0.000014
1980 Decompose Order: 0.000004
1981 Encoding Graph Time: 0.005468
1982 Elapse Encode time: 3.380701
1983 Is problem UNSAT after encoding: 0
1984 CNF Encode time: 0.000000
1985 SAT Solving time: 15.878807
1986 Result Computed in SAT solver:  SAT
1987 CSOLVER solve time: 19.259520
1988 Param PREPROCESS = 0     range=[0,1]
1989 Param ELEMENTOPTSETS = 1         range=[0,1]
1990 Param ELEMENTOPT = 0     range=[0,1]
1991 Param PROXYVARIABLE = 4          range=[1,5]
1992 Received score 19259520074.000000
1993 Mutating 1 settings
1994 &&&&&&&&Mutating&&&&&&&
1995 Param PREPROCESS = 1     range=[0,1]
1996 &&&&&&&&&&&&&&&&&&&&&&&
1997 **********************
1998 Polarity time: 0.004352
1999 Preprocess time: 0.015053
2000 Decompose Order: 0.000006
2001 Encoding Graph Time: 0.005608
2002 Elapse Encode time: 3.403785
2003 Is problem UNSAT after encoding: 0
2004 CNF Encode time: 0.000000
2005 SAT Solving time: 71.899633
2006 Result Computed in SAT solver:  SAT
2007 CSOLVER solve time: 75.303430
2008 Param PREPROCESS = 1     range=[0,1]
2009 Param ELEMENTOPTSETS = 1         range=[0,1]
2010 Param ELEMENTOPT = 0     range=[0,1]
2011 Param PROXYVARIABLE = 4          range=[1,5]
2012 Received score 75303429567.000000
2013 Best tuner:
2014 Param PREPROCESS = 0     range=[0,1]
2015 Param ELEMENTOPTSETS = 0         range=[0,1]
2016 Param ELEMENTOPT = 1     range=[0,1]
2017 Param PROXYVARIABLE = 1          range=[1,5]
2018 Received score 6942956251.000000