src/1.log

   1 deserializing ...
   2 **********************
   3 Polarity time: 0.004035
   4 Preprocess time: 0.013218
   5 Decompose Order: 0.000012
   6 Encoding Graph Time: 0.041886
   7 Elapse Encode time: 1.090344
   8 Is problem UNSAT after encoding: 0
   9 CNF Encode time: 0.000001
  10 SAT Solving time: 172.826413
  11 Result Computed in SAT solver:  SAT
  12 CSOLVER solve time: 173.916775
  13 Mutating 1 settings
  14 &&&&&&&&Mutating&&&&&&&
  15 Param ELEMENTOPTSETS = 1         range=[0,1]
  16 &&&&&&&&&&&&&&&&&&&&&&&
  17 **********************
  18 Polarity time: 0.003925
  19 Preprocess time: 0.012769
  20 Decompose Order: 0.000007
  21 Encoding Graph Time: 0.077234
  22 Elapse Encode time: 0.175357
  23 Is problem UNSAT after encoding: 0
  24 CNF Encode time: 0.000000
  25 SAT Solving time: 173.880185
  26 Result Computed in SAT solver:  SAT
  27 CSOLVER solve time: 174.055553
  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 174055552888.000000
  33 Mutating 1 settings
  34 &&&&&&&&Mutating&&&&&&&
  35 Param PREPROCESS = 0     range=[0,1]
  36 &&&&&&&&&&&&&&&&&&&&&&&
  37 **********************
  38 Polarity time: 0.003697
  39 Preprocess time: 0.000014
  40 Decompose Order: 0.000004
  41 Encoding Graph Time: 0.078022
  42 Elapse Encode time: 0.162977
  43 Is problem UNSAT after encoding: 0
  44 CNF Encode time: 0.000000
  45 SAT Solving time: 169.950790
  46 Result Computed in SAT solver:  SAT
  47 CSOLVER solve time: 170.113780
  48 Param PREPROCESS = 0     range=[0,1]
  49 Param ELEMENTOPTSETS = 1         range=[0,1]
  50 Param ELEMENTOPT = 1     range=[0,1]
  51 Param PROXYVARIABLE = 1          range=[1,5]
  52 Received score 170113779509.000000
  53 Mutating 1 settings
  54 &&&&&&&&Mutating&&&&&&&
  55 Param ELEMENTOPT = 0     range=[0,1]
  56 &&&&&&&&&&&&&&&&&&&&&&&
  57 **********************
  58 Polarity time: 0.003722
  59 Preprocess time: 0.000013
  60 Decompose Order: 0.000003
  61 Encoding Graph Time: 0.004957
  62 Elapse Encode time: 3.665021
  63 Is problem UNSAT after encoding: 0
  64 CNF Encode time: 0.000000
  65 SAT Solving time: 185.708077
  66 Result Computed in SAT solver:  SAT
  67 CSOLVER solve time: 189.373110
  68 Param PREPROCESS = 0     range=[0,1]
  69 Param ELEMENTOPTSETS = 1         range=[0,1]
  70 Param ELEMENTOPT = 0     range=[0,1]
  71 Param PROXYVARIABLE = 1          range=[1,5]
  72 Received score 189373110441.000000
  73 Mutating 1 settings
  74 &&&&&&&&Mutating&&&&&&&
  75 Param PROXYVARIABLE = 5          range=[1,5]
  76 &&&&&&&&&&&&&&&&&&&&&&&
  77 **********************
  78 Polarity time: 0.003696
  79 Preprocess time: 0.000014
  80 Decompose Order: 0.000003
  81 Encoding Graph Time: 0.004988
  82 Elapse Encode time: 3.656909
  83 Is problem UNSAT after encoding: 0
  84 CNF Encode time: 0.000000
  85 SAT Solving time: 223.981770
  86 Result Computed in SAT solver:  SAT
  87 CSOLVER solve time: 227.638691
  88 Param PREPROCESS = 0     range=[0,1]
  89 Param ELEMENTOPTSETS = 1         range=[0,1]
  90 Param ELEMENTOPT = 0     range=[0,1]
  91 Param PROXYVARIABLE = 5          range=[1,5]
  92 Received score 227638691365.000000
  93 Mutating 1 settings
  94 &&&&&&&&Mutating&&&&&&&
  95 Param PREPROCESS = 1     range=[0,1]
  96 &&&&&&&&&&&&&&&&&&&&&&&
  97 **********************
  98 Polarity time: 0.003746
  99 Preprocess time: 0.012362
 100 Decompose Order: 0.000006
 101 Encoding Graph Time: 0.005093
 102 Elapse Encode time: 3.673204
 103 Is problem UNSAT after encoding: 0
 104 CNF Encode time: 0.000000
 105 SAT Solving time: 204.648955
 106 Result Computed in SAT solver:  SAT
 107 CSOLVER solve time: 208.322172
 108 Param PREPROCESS = 1     range=[0,1]
 109 Param ELEMENTOPTSETS = 1         range=[0,1]
 110 Param ELEMENTOPT = 0     range=[0,1]
 111 Param PROXYVARIABLE = 1          range=[1,5]
 112 Received score 208322171971.000000
 113 Mutating 1 settings
 114 &&&&&&&&Mutating&&&&&&&
 115 Param PREPROCESS = 0     range=[0,1]
 116 &&&&&&&&&&&&&&&&&&&&&&&
 117 **********************
 118 Polarity time: 0.003783
 119 Preprocess time: 0.000014
 120 Decompose Order: 0.000003
 121 Encoding Graph Time: 0.005070
 122 Elapse Encode time: 3.660124
 123 Is problem UNSAT after encoding: 0
 124 CNF Encode time: 0.000000
 125 SAT Solving time: 168.955967
 126 Result Computed in SAT solver:  SAT
 127 CSOLVER solve time: 172.616103
 128 Param PREPROCESS = 0     range=[0,1]
 129 Param ELEMENTOPTSETS = 1         range=[0,1]
 130 Param ELEMENTOPT = 0     range=[0,1]
 131 Param PROXYVARIABLE = 1          range=[1,5]
 132 Received score 172616103387.000000
 133 Mutating 1 settings
 134 &&&&&&&&Mutating&&&&&&&
 135 Param PROXYVARIABLE = 3          range=[1,5]
 136 &&&&&&&&&&&&&&&&&&&&&&&
 137 **********************
 138 Polarity time: 0.003876
 139 Preprocess time: 0.000014
 140 Decompose Order: 0.000033
 141 Encoding Graph Time: 0.005254
 142 Elapse Encode time: 3.743260
 143 Is problem UNSAT after encoding: 0
 144 CNF Encode time: 0.000000
 145 SAT Solving time: 204.470081
 146 Result Computed in SAT solver:  SAT
 147 CSOLVER solve time: 208.213356
 148 Param PREPROCESS = 0     range=[0,1]
 149 Param ELEMENTOPTSETS = 1         range=[0,1]
 150 Param ELEMENTOPT = 0     range=[0,1]
 151 Param PROXYVARIABLE = 3          range=[1,5]
 152 Received score 208213356243.000000
 153 Mutating 1 settings
 154 &&&&&&&&Mutating&&&&&&&
 155 Param ELEMENTOPT = 1     range=[0,1]
 156 &&&&&&&&&&&&&&&&&&&&&&&
 157 **********************
 158 Polarity time: 0.004094
 159 Preprocess time: 0.000013
 160 Decompose Order: 0.000004
 161 Encoding Graph Time: 0.080160
 162 Elapse Encode time: 0.165375
 163 Is problem UNSAT after encoding: 0
 164 CNF Encode time: 0.000000
 165 SAT Solving time: 160.109910
 166 Result Computed in SAT solver:  SAT
 167 CSOLVER solve time: 160.275297
 168 Param PREPROCESS = 0     range=[0,1]
 169 Param ELEMENTOPTSETS = 1         range=[0,1]
 170 Param ELEMENTOPT = 1     range=[0,1]
 171 Param PROXYVARIABLE = 3          range=[1,5]
 172 Received score 160275296708.000000
 173 Mutating 1 settings
 174 &&&&&&&&Mutating&&&&&&&
 175 Param PROXYVARIABLE = 5          range=[1,5]
 176 &&&&&&&&&&&&&&&&&&&&&&&
 177 **********************
 178 Polarity time: 0.004059
 179 Preprocess time: 0.000014
 180 Decompose Order: 0.000003
 181 Encoding Graph Time: 0.078355
 182 Elapse Encode time: 0.163761
 183 Is problem UNSAT after encoding: 0
 184 CNF Encode time: 0.000000
 185 SAT Solving time: 156.193350
 186 Result Computed in SAT solver:  SAT
 187 CSOLVER solve time: 156.357122
 188 Param PREPROCESS = 0     range=[0,1]
 189 Param ELEMENTOPTSETS = 1         range=[0,1]
 190 Param ELEMENTOPT = 1     range=[0,1]
 191 Param PROXYVARIABLE = 5          range=[1,5]
 192 Received score 156357122315.000000
 193 Mutating 1 settings
 194 &&&&&&&&Mutating&&&&&&&
 195 Param ELEMENTOPT = 0     range=[0,1]
 196 &&&&&&&&&&&&&&&&&&&&&&&
 197 **********************
 198 Polarity time: 0.004075
 199 Preprocess time: 0.000012
 200 Decompose Order: 0.000003
 201 Encoding Graph Time: 0.005185
 202 Elapse Encode time: 3.663215
 203 Is problem UNSAT after encoding: 0
 204 CNF Encode time: 0.000000
 205 SAT Solving time: 203.557549
 206 Result Computed in SAT solver:  SAT
 207 CSOLVER solve time: 207.220776
 208 Param PREPROCESS = 0     range=[0,1]
 209 Param ELEMENTOPTSETS = 1         range=[0,1]
 210 Param ELEMENTOPT = 0     range=[0,1]
 211 Param PROXYVARIABLE = 5          range=[1,5]
 212 Received score 207220776365.000000
 213 Mutating 1 settings
 214 &&&&&&&&Mutating&&&&&&&
 215 Param ELEMENTOPTSETS = 0         range=[0,1]
 216 &&&&&&&&&&&&&&&&&&&&&&&
 217 **********************
 218 Polarity time: 0.003905
 219 Preprocess time: 0.000010
 220 Decompose Order: 0.000003
 221 Encoding Graph Time: 0.005012
 222 Elapse Encode time: 3.644834
 223 Is problem UNSAT after encoding: 0
 224 CNF Encode time: 0.000000
 225 SAT Solving time: 212.951258
 226 Result Computed in SAT solver:  SAT
 227 CSOLVER solve time: 216.596105
 228 Param PREPROCESS = 0     range=[0,1]
 229 Param ELEMENTOPTSETS = 0         range=[0,1]
 230 Param ELEMENTOPT = 0     range=[0,1]
 231 Param PROXYVARIABLE = 5          range=[1,5]
 232 Received score 216596104827.000000
 233 Mutating 1 settings
 234 &&&&&&&&Mutating&&&&&&&
 235 Param PREPROCESS = 1     range=[0,1]
 236 &&&&&&&&&&&&&&&&&&&&&&&
 237 **********************
 238 Polarity time: 0.003877
 239 Preprocess time: 0.012756
 240 Decompose Order: 0.000007
 241 Encoding Graph Time: 0.005143
 242 Elapse Encode time: 3.682618
 243 Is problem UNSAT after encoding: 0
 244 CNF Encode time: 0.000000
 245 SAT Solving time: 209.801021
 246 Result Computed in SAT solver:  SAT
 247 CSOLVER solve time: 213.483652
 248 Param PREPROCESS = 1     range=[0,1]
 249 Param ELEMENTOPTSETS = 0         range=[0,1]
 250 Param ELEMENTOPT = 0     range=[0,1]
 251 Param PROXYVARIABLE = 5          range=[1,5]
 252 Received score 213483652346.000000
 253 Mutating 1 settings
 254 &&&&&&&&Mutating&&&&&&&
 255 Param ELEMENTOPTSETS = 1         range=[0,1]
 256 &&&&&&&&&&&&&&&&&&&&&&&
 257 **********************
 258 Polarity time: 0.003956
 259 Preprocess time: 0.012794
 260 Decompose Order: 0.000007
 261 Encoding Graph Time: 0.005206
 262 Elapse Encode time: 3.699788
 263 Is problem UNSAT after encoding: 0
 264 CNF Encode time: 0.000000
 265 SAT Solving time: 212.723803
 266 Result Computed in SAT solver:  SAT
 267 CSOLVER solve time: 216.423604
 268 Param PREPROCESS = 1     range=[0,1]
 269 Param ELEMENTOPTSETS = 1         range=[0,1]
 270 Param ELEMENTOPT = 0     range=[0,1]
 271 Param PROXYVARIABLE = 5          range=[1,5]
 272 Received score 216423604309.000000
 273 Mutating 1 settings
 274 &&&&&&&&Mutating&&&&&&&
 275 Param PROXYVARIABLE = 1          range=[1,5]
 276 &&&&&&&&&&&&&&&&&&&&&&&
 277 **********************
 278 Polarity time: 0.003936
 279 Preprocess time: 0.012737
 280 Decompose Order: 0.000007
 281 Encoding Graph Time: 0.005156
 282 Elapse Encode time: 3.788655
 283 Is problem UNSAT after encoding: 0
 284 CNF Encode time: 0.000000
 285 SAT Solving time: 193.596544
 286 Result Computed in SAT solver:  SAT
 287 CSOLVER solve time: 197.385211
 288 Param PREPROCESS = 1     range=[0,1]
 289 Param ELEMENTOPTSETS = 1         range=[0,1]
 290 Param ELEMENTOPT = 0     range=[0,1]
 291 Param PROXYVARIABLE = 1          range=[1,5]
 292 Received score 197385211257.000000
 293 Mutating 1 settings
 294 &&&&&&&&Mutating&&&&&&&
 295 Param ELEMENTOPT = 1     range=[0,1]
 296 &&&&&&&&&&&&&&&&&&&&&&&
 297 **********************
 298 Polarity time: 0.003742
 299 Preprocess time: 0.012359
 300 Decompose Order: 0.000007
 301 Encoding Graph Time: 0.076438
 302 Elapse Encode time: 0.173937
 303 Is problem UNSAT after encoding: 0
 304 CNF Encode time: 0.000000
 305 SAT Solving time: 160.742431
 306 Result Computed in SAT solver:  SAT
 307 CSOLVER solve time: 160.916381
 308 Param PREPROCESS = 1     range=[0,1]
 309 Param ELEMENTOPTSETS = 1         range=[0,1]
 310 Param ELEMENTOPT = 1     range=[0,1]
 311 Param PROXYVARIABLE = 1          range=[1,5]
 312 Received score 160916380571.000000
 313 Mutating 1 settings
 314 &&&&&&&&Mutating&&&&&&&
 315 Param ELEMENTOPT = 0     range=[0,1]
 316 &&&&&&&&&&&&&&&&&&&&&&&
 317 **********************
 318 Polarity time: 0.003737
 319 Preprocess time: 0.012349
 320 Decompose Order: 0.000006
 321 Encoding Graph Time: 0.005086
 322 Elapse Encode time: 3.669822
 323 Is problem UNSAT after encoding: 0
 324 CNF Encode time: 0.000000
 325 SAT Solving time: 188.818087
 326 Result Computed in SAT solver:  SAT
 327 CSOLVER solve time: 192.487921
 328 Param PREPROCESS = 1     range=[0,1]
 329 Param ELEMENTOPTSETS = 1         range=[0,1]
 330 Param ELEMENTOPT = 0     range=[0,1]
 331 Param PROXYVARIABLE = 1          range=[1,5]
 332 Received score 192487920763.000000
 333 Mutating 1 settings
 334 &&&&&&&&Mutating&&&&&&&
 335 Param PROXYVARIABLE = 2          range=[1,5]
 336 &&&&&&&&&&&&&&&&&&&&&&&
 337 **********************
 338 Polarity time: 0.003727
 339 Preprocess time: 0.012391
 340 Decompose Order: 0.000007
 341 Encoding Graph Time: 0.005276
 342 Elapse Encode time: 3.682198
 343 Is problem UNSAT after encoding: 0
 344 CNF Encode time: 0.000000
 345 SAT Solving time: 211.634056
 346 Result Computed in SAT solver:  SAT
 347 CSOLVER solve time: 215.316267
 348 Param PREPROCESS = 1     range=[0,1]
 349 Param ELEMENTOPTSETS = 1         range=[0,1]
 350 Param ELEMENTOPT = 0     range=[0,1]
 351 Param PROXYVARIABLE = 2          range=[1,5]
 352 Received score 215316267144.000000
 353 Mutating 1 settings
 354 &&&&&&&&Mutating&&&&&&&
 355 Param ELEMENTOPTSETS = 0         range=[0,1]
 356 &&&&&&&&&&&&&&&&&&&&&&&
 357 **********************
 358 Polarity time: 0.003778
 359 Preprocess time: 0.012453
 360 Decompose Order: 0.000008
 361 Encoding Graph Time: 0.005142
 362 Elapse Encode time: 3.676799
 363 Is problem UNSAT after encoding: 0
 364 CNF Encode time: 0.000000
 365 SAT Solving time: 198.427101
 366 Result Computed in SAT solver:  SAT
 367 CSOLVER solve time: 202.103912
 368 Param PREPROCESS = 1     range=[0,1]
 369 Param ELEMENTOPTSETS = 0         range=[0,1]
 370 Param ELEMENTOPT = 0     range=[0,1]
 371 Param PROXYVARIABLE = 1          range=[1,5]
 372 Received score 202103912479.000000
 373 Mutating 1 settings
 374 &&&&&&&&Mutating&&&&&&&
 375 Param PREPROCESS = 0     range=[0,1]
 376 &&&&&&&&&&&&&&&&&&&&&&&
 377 **********************
 378 Polarity time: 0.003800
 379 Preprocess time: 0.000013
 380 Decompose Order: 0.000004
 381 Encoding Graph Time: 0.005169
 382 Elapse Encode time: 3.694777
 383 Is problem UNSAT after encoding: 0
 384 CNF Encode time: 0.000000
 385 SAT Solving time: 213.284328
 386 Result Computed in SAT solver:  SAT
 387 CSOLVER solve time: 216.979118
 388 Param PREPROCESS = 0     range=[0,1]
 389 Param ELEMENTOPTSETS = 0         range=[0,1]
 390 Param ELEMENTOPT = 0     range=[0,1]
 391 Param PROXYVARIABLE = 1          range=[1,5]
 392 Received score 216979117988.000000
 393 Mutating 1 settings
 394 &&&&&&&&Mutating&&&&&&&
 395 Param ELEMENTOPTSETS = 1         range=[0,1]
 396 &&&&&&&&&&&&&&&&&&&&&&&
 397 **********************
 398 Polarity time: 0.003946
 399 Preprocess time: 0.000011
 400 Decompose Order: 0.000003
 401 Encoding Graph Time: 0.005132
 402 Elapse Encode time: 3.723860
 403 Is problem UNSAT after encoding: 0
 404 CNF Encode time: 0.000000
 405 SAT Solving time: 175.762665
 406 Result Computed in SAT solver:  SAT
 407 CSOLVER solve time: 179.486539
 408 Param PREPROCESS = 0     range=[0,1]
 409 Param ELEMENTOPTSETS = 1         range=[0,1]
 410 Param ELEMENTOPT = 0     range=[0,1]
 411 Param PROXYVARIABLE = 1          range=[1,5]
 412 Received score 179486538926.000000
 413 Mutating 1 settings
 414 &&&&&&&&Mutating&&&&&&&
 415 Param PREPROCESS = 1     range=[0,1]
 416 &&&&&&&&&&&&&&&&&&&&&&&
 417 **********************
 418 Polarity time: 0.003912
 419 Preprocess time: 0.012528
 420 Decompose Order: 0.000008
 421 Encoding Graph Time: 0.005059
 422 Elapse Encode time: 3.674142
 423 Is problem UNSAT after encoding: 0
 424 CNF Encode time: 0.000000
 425 SAT Solving time: 211.915724
 426 Result Computed in SAT solver:  SAT
 427 CSOLVER solve time: 215.589878
 428 Param PREPROCESS = 1     range=[0,1]
 429 Param ELEMENTOPTSETS = 1         range=[0,1]
 430 Param ELEMENTOPT = 0     range=[0,1]
 431 Param PROXYVARIABLE = 1          range=[1,5]
 432 Received score 215589878125.000000
 433 Mutating 1 settings
 434 &&&&&&&&Mutating&&&&&&&
 435 Param ELEMENTOPTSETS = 0         range=[0,1]
 436 &&&&&&&&&&&&&&&&&&&&&&&
 437 **********************
 438 Polarity time: 0.004946
 439 Preprocess time: 0.014076
 440 Decompose Order: 0.000007
 441 Encoding Graph Time: 0.005094
 442 Elapse Encode time: 3.698828
 443 Is problem UNSAT after encoding: 0
 444 CNF Encode time: 0.000000
 445 SAT Solving time: 211.473552
 446 Result Computed in SAT solver:  SAT
 447 CSOLVER solve time: 215.172394
 448 Param PREPROCESS = 1     range=[0,1]
 449 Param ELEMENTOPTSETS = 0         range=[0,1]
 450 Param ELEMENTOPT = 0     range=[0,1]
 451 Param PROXYVARIABLE = 1          range=[1,5]
 452 Received score 215172393540.000000
 453 Mutating 1 settings
 454 &&&&&&&&Mutating&&&&&&&
 455 Param PREPROCESS = 0     range=[0,1]
 456 &&&&&&&&&&&&&&&&&&&&&&&
 457 **********************
 458 Polarity time: 0.004016
 459 Preprocess time: 0.000011
 460 Decompose Order: 0.000003
 461 Encoding Graph Time: 0.005101
 462 Elapse Encode time: 3.708234
 463 Is problem UNSAT after encoding: 0
 464 CNF Encode time: 0.000000
 465 SAT Solving time: 175.099455
 466 Result Computed in SAT solver:  SAT
 467 CSOLVER solve time: 178.807702
 468 Param PREPROCESS = 0     range=[0,1]
 469 Param ELEMENTOPTSETS = 0         range=[0,1]
 470 Param ELEMENTOPT = 0     range=[0,1]
 471 Param PROXYVARIABLE = 1          range=[1,5]
 472 Received score 178807701670.000000
 473 Mutating 1 settings
 474 &&&&&&&&Mutating&&&&&&&
 475 Param ELEMENTOPTSETS = 1         range=[0,1]
 476 &&&&&&&&&&&&&&&&&&&&&&&
 477 **********************
 478 Polarity time: 0.003954
 479 Preprocess time: 0.000011
 480 Decompose Order: 0.000003
 481 Encoding Graph Time: 0.005191
 482 Elapse Encode time: 3.710612
 483 Is problem UNSAT after encoding: 0
 484 CNF Encode time: 0.000000
 485 SAT Solving time: 189.884156
 486 Result Computed in SAT solver:  SAT
 487 CSOLVER solve time: 193.594781
 488 Param PREPROCESS = 0     range=[0,1]
 489 Param ELEMENTOPTSETS = 1         range=[0,1]
 490 Param ELEMENTOPT = 0     range=[0,1]
 491 Param PROXYVARIABLE = 1          range=[1,5]
 492 Received score 193594780541.000000
 493 Mutating 1 settings
 494 &&&&&&&&Mutating&&&&&&&
 495 Param ELEMENTOPT = 1     range=[0,1]
 496 &&&&&&&&&&&&&&&&&&&&&&&
 497 **********************
 498 Polarity time: 0.003990
 499 Preprocess time: 0.000011
 500 Decompose Order: 0.000003
 501 Encoding Graph Time: 0.077490
 502 Elapse Encode time: 0.162925
 503 Is problem UNSAT after encoding: 0
 504 CNF Encode time: 0.000000
 505 SAT Solving time: 161.874690
 506 Result Computed in SAT solver:  SAT
 507 CSOLVER solve time: 162.037625
 508 Param PREPROCESS = 0     range=[0,1]
 509 Param ELEMENTOPTSETS = 1         range=[0,1]
 510 Param ELEMENTOPT = 1     range=[0,1]
 511 Param PROXYVARIABLE = 1          range=[1,5]
 512 Received score 162037625387.000000
 513 Mutating 1 settings
 514 &&&&&&&&Mutating&&&&&&&
 515 Param ELEMENTOPT = 0     range=[0,1]
 516 &&&&&&&&&&&&&&&&&&&&&&&
 517 **********************
 518 Polarity time: 0.004718
 519 Preprocess time: 0.000019
 520 Decompose Order: 0.000004
 521 Encoding Graph Time: 0.006761
 522 Elapse Encode time: 3.685110
 523 Is problem UNSAT after encoding: 0
 524 CNF Encode time: 0.000000
 525 SAT Solving time: 196.936218
 526 Result Computed in SAT solver:  SAT
 527 CSOLVER solve time: 200.621340
 528 Param PREPROCESS = 0     range=[0,1]
 529 Param ELEMENTOPTSETS = 1         range=[0,1]
 530 Param ELEMENTOPT = 0     range=[0,1]
 531 Param PROXYVARIABLE = 1          range=[1,5]
 532 Received score 200621339784.000000
 533 Mutating 1 settings
 534 &&&&&&&&Mutating&&&&&&&
 535 Param PREPROCESS = 1     range=[0,1]
 536 &&&&&&&&&&&&&&&&&&&&&&&
 537 **********************
 538 Polarity time: 0.004118
 539 Preprocess time: 0.013453
 540 Decompose Order: 0.000009
 541 Encoding Graph Time: 0.005998
 542 Elapse Encode time: 3.686376
 543 Is problem UNSAT after encoding: 0
 544 CNF Encode time: 0.000000
 545 SAT Solving time: 194.281813
 546 Result Computed in SAT solver:  SAT
 547 CSOLVER solve time: 197.968202
 548 Param PREPROCESS = 1     range=[0,1]
 549 Param ELEMENTOPTSETS = 1         range=[0,1]
 550 Param ELEMENTOPT = 0     range=[0,1]
 551 Param PROXYVARIABLE = 1          range=[1,5]
 552 Received score 197968202182.000000
 553 Mutating 1 settings
 554 &&&&&&&&Mutating&&&&&&&
 555 Param PREPROCESS = 0     range=[0,1]
 556 &&&&&&&&&&&&&&&&&&&&&&&
 557 **********************
 558 Polarity time: 0.003897
 559 Preprocess time: 0.000011
 560 Decompose Order: 0.000003
 561 Encoding Graph Time: 0.005008
 562 Elapse Encode time: 3.673334
 563 Is problem UNSAT after encoding: 0
 564 CNF Encode time: 0.000000
 565 SAT Solving time: 209.588656
 566 Result Computed in SAT solver:  SAT
 567 CSOLVER solve time: 213.262002
 568 Param PREPROCESS = 0     range=[0,1]
 569 Param ELEMENTOPTSETS = 1         range=[0,1]
 570 Param ELEMENTOPT = 0     range=[0,1]
 571 Param PROXYVARIABLE = 1          range=[1,5]
 572 Received score 213262001799.000000
 573 Mutating 1 settings
 574 &&&&&&&&Mutating&&&&&&&
 575 Param ELEMENTOPT = 1     range=[0,1]
 576 &&&&&&&&&&&&&&&&&&&&&&&
 577 **********************
 578 Polarity time: 0.003856
 579 Preprocess time: 0.012520
 580 Decompose Order: 0.000008
 581 Encoding Graph Time: 0.077373
 582 Elapse Encode time: 0.175199
 583 Is problem UNSAT after encoding: 0
 584 CNF Encode time: 0.000000
 585 SAT Solving time: 160.810740
 586 Result Computed in SAT solver:  SAT
 587 CSOLVER solve time: 160.985950
 588 Param PREPROCESS = 1     range=[0,1]
 589 Param ELEMENTOPTSETS = 1         range=[0,1]
 590 Param ELEMENTOPT = 1     range=[0,1]
 591 Param PROXYVARIABLE = 1          range=[1,5]
 592 Received score 160985949607.000000
 593 Mutating 1 settings
 594 &&&&&&&&Mutating&&&&&&&
 595 Param PREPROCESS = 0     range=[0,1]
 596 &&&&&&&&&&&&&&&&&&&&&&&
 597 **********************
 598 Polarity time: 0.003781
 599 Preprocess time: 0.000015
 600 Decompose Order: 0.000005
 601 Encoding Graph Time: 0.077545
 602 Elapse Encode time: 0.162992
 603 Is problem UNSAT after encoding: 0
 604 CNF Encode time: 0.000000
 605 SAT Solving time: 160.765425
 606 Result Computed in SAT solver:  SAT
 607 CSOLVER solve time: 160.928428
 608 Param PREPROCESS = 0     range=[0,1]
 609 Param ELEMENTOPTSETS = 1         range=[0,1]
 610 Param ELEMENTOPT = 1     range=[0,1]
 611 Param PROXYVARIABLE = 1          range=[1,5]
 612 Received score 160928427691.000000
 613 Mutating 1 settings
 614 &&&&&&&&Mutating&&&&&&&
 615 Param PROXYVARIABLE = 2          range=[1,5]
 616 &&&&&&&&&&&&&&&&&&&&&&&
 617 **********************
 618 Polarity time: 0.003909
 619 Preprocess time: 0.000016
 620 Decompose Order: 0.000004
 621 Encoding Graph Time: 0.078728
 622 Elapse Encode time: 0.164136
 623 Is problem UNSAT after encoding: 0
 624 CNF Encode time: 0.000000
 625 SAT Solving time: 162.124576
 626 Result Computed in SAT solver:  SAT
 627 CSOLVER solve time: 162.288723
 628 Param PREPROCESS = 0     range=[0,1]
 629 Param ELEMENTOPTSETS = 1         range=[0,1]
 630 Param ELEMENTOPT = 1     range=[0,1]
 631 Param PROXYVARIABLE = 2          range=[1,5]
 632 Received score 162288723346.000000
 633 Mutating 1 settings
 634 &&&&&&&&Mutating&&&&&&&
 635 Param ELEMENTOPT = 0     range=[0,1]
 636 &&&&&&&&&&&&&&&&&&&&&&&
 637 **********************
 638 Polarity time: 0.003781
 639 Preprocess time: 0.000012
 640 Decompose Order: 0.000005
 641 Encoding Graph Time: 0.004942
 642 Elapse Encode time: 3.680737
 643 Is problem UNSAT after encoding: 0
 644 CNF Encode time: 0.000000
 645 SAT Solving time: 209.995768
 646 Result Computed in SAT solver:  SAT
 647 CSOLVER solve time: 213.676518
 648 Param PREPROCESS = 0     range=[0,1]
 649 Param ELEMENTOPTSETS = 1         range=[0,1]
 650 Param ELEMENTOPT = 0     range=[0,1]
 651 Param PROXYVARIABLE = 2          range=[1,5]
 652 Received score 213676517632.000000
 653 Mutating 1 settings
 654 &&&&&&&&Mutating&&&&&&&
 655 Param PROXYVARIABLE = 4          range=[1,5]
 656 &&&&&&&&&&&&&&&&&&&&&&&
 657 **********************
 658 Polarity time: 0.003945
 659 Preprocess time: 0.000011
 660 Decompose Order: 0.000003
 661 Encoding Graph Time: 0.078411
 662 Elapse Encode time: 0.163838
 663 Is problem UNSAT after encoding: 0
 664 CNF Encode time: 0.000000
 665 SAT Solving time: 164.902978
 666 Result Computed in SAT solver:  SAT
 667 CSOLVER solve time: 165.066828
 668 Param PREPROCESS = 0     range=[0,1]
 669 Param ELEMENTOPTSETS = 1         range=[0,1]
 670 Param ELEMENTOPT = 1     range=[0,1]
 671 Param PROXYVARIABLE = 4          range=[1,5]
 672 Received score 165066827531.000000
 673 Mutating 1 settings
 674 &&&&&&&&Mutating&&&&&&&
 675 Param ELEMENTOPT = 0     range=[0,1]
 676 &&&&&&&&&&&&&&&&&&&&&&&
 677 **********************
 678 Polarity time: 0.003898
 679 Preprocess time: 0.000011
 680 Decompose Order: 0.000004
 681 Encoding Graph Time: 0.005102
 682 Elapse Encode time: 3.732650
 683 Is problem UNSAT after encoding: 0
 684 CNF Encode time: 0.000000
 685 SAT Solving time: 174.291819
 686 Result Computed in SAT solver:  SAT
 687 CSOLVER solve time: 178.024506
 688 Param PREPROCESS = 0     range=[0,1]
 689 Param ELEMENTOPTSETS = 1         range=[0,1]
 690 Param ELEMENTOPT = 0     range=[0,1]
 691 Param PROXYVARIABLE = 4          range=[1,5]
 692 Received score 178024506426.000000
 693 Mutating 1 settings
 694 &&&&&&&&Mutating&&&&&&&
 695 Param ELEMENTOPTSETS = 0         range=[0,1]
 696 &&&&&&&&&&&&&&&&&&&&&&&
 697 **********************
 698 Polarity time: 0.003741
 699 Preprocess time: 0.000014
 700 Decompose Order: 0.000004
 701 Encoding Graph Time: 0.005041
 702 Elapse Encode time: 3.693665
 703 Is problem UNSAT after encoding: 0
 704 CNF Encode time: 0.000000
 705 SAT Solving time: 210.357435
 706 Result Computed in SAT solver:  SAT
 707 CSOLVER solve time: 214.051112
 708 Param PREPROCESS = 0     range=[0,1]
 709 Param ELEMENTOPTSETS = 0         range=[0,1]
 710 Param ELEMENTOPT = 0     range=[0,1]
 711 Param PROXYVARIABLE = 4          range=[1,5]
 712 Received score 214051112258.000000
 713 Mutating 1 settings
 714 &&&&&&&&Mutating&&&&&&&
 715 Param PREPROCESS = 1     range=[0,1]
 716 &&&&&&&&&&&&&&&&&&&&&&&
 717 **********************
 718 Polarity time: 0.003847
 719 Preprocess time: 0.012496
 720 Decompose Order: 0.000008
 721 Encoding Graph Time: 0.005112
 722 Elapse Encode time: 3.687460
 723 Is problem UNSAT after encoding: 0
 724 CNF Encode time: 0.000000
 725 SAT Solving time: 213.431153
 726 Result Computed in SAT solver:  SAT
 727 CSOLVER solve time: 217.118625
 728 Param PREPROCESS = 1     range=[0,1]
 729 Param ELEMENTOPTSETS = 0         range=[0,1]
 730 Param ELEMENTOPT = 0     range=[0,1]
 731 Param PROXYVARIABLE = 4          range=[1,5]
 732 Received score 217118624848.000000
 733 Mutating 1 settings
 734 &&&&&&&&Mutating&&&&&&&
 735 Param ELEMENTOPTSETS = 1         range=[0,1]
 736 &&&&&&&&&&&&&&&&&&&&&&&
 737 **********************
 738 Polarity time: 0.003863
 739 Preprocess time: 0.012529
 740 Decompose Order: 0.000007
 741 Encoding Graph Time: 0.005267
 742 Elapse Encode time: 3.728645
 743 Is problem UNSAT after encoding: 0
 744 CNF Encode time: 0.000000
 745 SAT Solving time: 176.863374
 746 Result Computed in SAT solver:  SAT
 747 CSOLVER solve time: 180.592032
 748 Param PREPROCESS = 1     range=[0,1]
 749 Param ELEMENTOPTSETS = 1         range=[0,1]
 750 Param ELEMENTOPT = 0     range=[0,1]
 751 Param PROXYVARIABLE = 4          range=[1,5]
 752 Received score 180592031883.000000
 753 Mutating 1 settings
 754 &&&&&&&&Mutating&&&&&&&
 755 Param ELEMENTOPTSETS = 0         range=[0,1]
 756 &&&&&&&&&&&&&&&&&&&&&&&
 757 **********************
 758 Polarity time: 0.003859
 759 Preprocess time: 0.012417
 760 Decompose Order: 0.000007
 761 Encoding Graph Time: 0.005122
 762 Elapse Encode time: 3.670089
 763 Is problem UNSAT after encoding: 0
 764 CNF Encode time: 0.000000
 765 SAT Solving time: 192.040423
 766 Result Computed in SAT solver:  SAT
 767 CSOLVER solve time: 195.710525
 768 Param PREPROCESS = 1     range=[0,1]
 769 Param ELEMENTOPTSETS = 0         range=[0,1]
 770 Param ELEMENTOPT = 0     range=[0,1]
 771 Param PROXYVARIABLE = 4          range=[1,5]
 772 Received score 195710524957.000000
 773 Mutating 1 settings
 774 &&&&&&&&Mutating&&&&&&&
 775 Param PREPROCESS = 0     range=[0,1]
 776 &&&&&&&&&&&&&&&&&&&&&&&
 777 **********************
 778 Polarity time: 0.003848
 779 Preprocess time: 0.000014
 780 Decompose Order: 0.000004
 781 Encoding Graph Time: 0.005036
 782 Elapse Encode time: 3.685831
 783 Is problem UNSAT after encoding: 0
 784 CNF Encode time: 0.000000
 785 SAT Solving time: 197.900643
 786 Result Computed in SAT solver:  SAT
 787 CSOLVER solve time: 201.586486
 788 Param PREPROCESS = 0     range=[0,1]
 789 Param ELEMENTOPTSETS = 0         range=[0,1]
 790 Param ELEMENTOPT = 0     range=[0,1]
 791 Param PROXYVARIABLE = 4          range=[1,5]
 792 Received score 201586486320.000000
 793 Mutating 1 settings
 794 &&&&&&&&Mutating&&&&&&&
 795 Param ELEMENTOPTSETS = 1         range=[0,1]
 796 &&&&&&&&&&&&&&&&&&&&&&&
 797 **********************
 798 Polarity time: 0.003800
 799 Preprocess time: 0.000011
 800 Decompose Order: 0.000004
 801 Encoding Graph Time: 0.005104
 802 Elapse Encode time: 3.653650
 803 Is problem UNSAT after encoding: 0
 804 CNF Encode time: 0.000000
 805 SAT Solving time: 191.699499
 806 Result Computed in SAT solver:  SAT
 807 CSOLVER solve time: 195.353162
 808 Param PREPROCESS = 0     range=[0,1]
 809 Param ELEMENTOPTSETS = 1         range=[0,1]
 810 Param ELEMENTOPT = 0     range=[0,1]
 811 Param PROXYVARIABLE = 4          range=[1,5]
 812 Received score 195353162260.000000
 813 Mutating 1 settings
 814 &&&&&&&&Mutating&&&&&&&
 815 Param ELEMENTOPTSETS = 0         range=[0,1]
 816 &&&&&&&&&&&&&&&&&&&&&&&
 817 **********************
 818 Polarity time: 0.003814
 819 Preprocess time: 0.000012
 820 Decompose Order: 0.000003
 821 Encoding Graph Time: 0.005189
 822 Elapse Encode time: 3.650501
 823 Is problem UNSAT after encoding: 0
 824 CNF Encode time: 0.000000
 825 SAT Solving time: 201.154915
 826 Result Computed in SAT solver:  SAT
 827 CSOLVER solve time: 204.805428
 828 Param PREPROCESS = 0     range=[0,1]
 829 Param ELEMENTOPTSETS = 0         range=[0,1]
 830 Param ELEMENTOPT = 0     range=[0,1]
 831 Param PROXYVARIABLE = 4          range=[1,5]
 832 Received score 204805427968.000000
 833 Mutating 1 settings
 834 &&&&&&&&Mutating&&&&&&&
 835 Param PROXYVARIABLE = 2          range=[1,5]
 836 &&&&&&&&&&&&&&&&&&&&&&&
 837 **********************
 838 Polarity time: 0.003763
 839 Preprocess time: 0.000014
 840 Decompose Order: 0.000004
 841 Encoding Graph Time: 0.005082
 842 Elapse Encode time: 3.699244
 843 Is problem UNSAT after encoding: 0
 844 CNF Encode time: 0.000000
 845 SAT Solving time: 200.259792
 846 Result Computed in SAT solver:  SAT
 847 CSOLVER solve time: 203.959052
 848 Param PREPROCESS = 0     range=[0,1]
 849 Param ELEMENTOPTSETS = 0         range=[0,1]
 850 Param ELEMENTOPT = 0     range=[0,1]
 851 Param PROXYVARIABLE = 2          range=[1,5]
 852 Received score 203959052436.000000
 853 Mutating 1 settings
 854 &&&&&&&&Mutating&&&&&&&
 855 Param PROXYVARIABLE = 1          range=[1,5]
 856 &&&&&&&&&&&&&&&&&&&&&&&
 857 **********************
 858 Polarity time: 0.004775
 859 Preprocess time: 0.000015
 860 Decompose Order: 0.000006
 861 Encoding Graph Time: 0.005933
 862 Elapse Encode time: 3.663216
 863 Is problem UNSAT after encoding: 0
 864 CNF Encode time: 0.000000
 865 SAT Solving time: 191.255302
 866 Result Computed in SAT solver:  SAT
 867 CSOLVER solve time: 194.918530
 868 Param PREPROCESS = 0     range=[0,1]
 869 Param ELEMENTOPTSETS = 0         range=[0,1]
 870 Param ELEMENTOPT = 0     range=[0,1]
 871 Param PROXYVARIABLE = 1          range=[1,5]
 872 Received score 194918530006.000000
 873 Mutating 1 settings
 874 &&&&&&&&Mutating&&&&&&&
 875 Param ELEMENTOPTSETS = 1         range=[0,1]
 876 &&&&&&&&&&&&&&&&&&&&&&&
 877 **********************
 878 Polarity time: 0.003849
 879 Preprocess time: 0.000013
 880 Decompose Order: 0.000004
 881 Encoding Graph Time: 0.005054
 882 Elapse Encode time: 3.650705
 883 Is problem UNSAT after encoding: 0
 884 CNF Encode time: 0.000000
 885 SAT Solving time: 194.531983
 886 Result Computed in SAT solver:  SAT
 887 CSOLVER solve time: 198.182701
 888 Param PREPROCESS = 0     range=[0,1]
 889 Param ELEMENTOPTSETS = 1         range=[0,1]
 890 Param ELEMENTOPT = 0     range=[0,1]
 891 Param PROXYVARIABLE = 1          range=[1,5]
 892 Received score 198182700896.000000
 893 Mutating 1 settings
 894 &&&&&&&&Mutating&&&&&&&
 895 Param ELEMENTOPT = 1     range=[0,1]
 896 &&&&&&&&&&&&&&&&&&&&&&&
 897 **********************
 898 Polarity time: 0.003755
 899 Preprocess time: 0.000012
 900 Decompose Order: 0.000004
 901 Encoding Graph Time: 0.077098
 902 Elapse Encode time: 0.163305
 903 Is problem UNSAT after encoding: 0
 904 CNF Encode time: 0.000000
 905 SAT Solving time: 163.264840
 906 Result Computed in SAT solver:  SAT
 907 CSOLVER solve time: 163.428155
 908 Param PREPROCESS = 0     range=[0,1]
 909 Param ELEMENTOPTSETS = 1         range=[0,1]
 910 Param ELEMENTOPT = 1     range=[0,1]
 911 Param PROXYVARIABLE = 1          range=[1,5]
 912 Received score 163428155146.000000
 913 Mutating 1 settings
 914 &&&&&&&&Mutating&&&&&&&
 915 Param PREPROCESS = 1     range=[0,1]
 916 &&&&&&&&&&&&&&&&&&&&&&&
 917 **********************
 918 Polarity time: 0.003749
 919 Preprocess time: 0.012392
 920 Decompose Order: 0.000007
 921 Encoding Graph Time: 0.078428
 922 Elapse Encode time: 0.176425
 923 Is problem UNSAT after encoding: 0
 924 CNF Encode time: 0.000000
 925 SAT Solving time: 165.949550
 926 Result Computed in SAT solver:  SAT
 927 CSOLVER solve time: 166.125986
 928 Param PREPROCESS = 1     range=[0,1]
 929 Param ELEMENTOPTSETS = 1         range=[0,1]
 930 Param ELEMENTOPT = 1     range=[0,1]
 931 Param PROXYVARIABLE = 1          range=[1,5]
 932 Received score 166125986333.000000
 933 Mutating 1 settings
 934 &&&&&&&&Mutating&&&&&&&
 935 Param PREPROCESS = 0     range=[0,1]
 936 &&&&&&&&&&&&&&&&&&&&&&&
 937 **********************
 938 Polarity time: 0.003869
 939 Preprocess time: 0.000013
 940 Decompose Order: 0.000004
 941 Encoding Graph Time: 0.076888
 942 Elapse Encode time: 0.162166
 943 Is problem UNSAT after encoding: 0
 944 CNF Encode time: 0.000000
 945 SAT Solving time: 170.109839
 946 Result Computed in SAT solver:  SAT
 947 CSOLVER solve time: 170.272016
 948 Param PREPROCESS = 0     range=[0,1]
 949 Param ELEMENTOPTSETS = 1         range=[0,1]
 950 Param ELEMENTOPT = 1     range=[0,1]
 951 Param PROXYVARIABLE = 1          range=[1,5]
 952 Received score 170272015757.000000
 953 Mutating 1 settings
 954 &&&&&&&&Mutating&&&&&&&
 955 Param PROXYVARIABLE = 4          range=[1,5]
 956 &&&&&&&&&&&&&&&&&&&&&&&
 957 **********************
 958 Polarity time: 0.004817
 959 Preprocess time: 0.000020
 960 Decompose Order: 0.000004
 961 Encoding Graph Time: 0.078371
 962 Elapse Encode time: 0.164605
 963 Is problem UNSAT after encoding: 0
 964 CNF Encode time: 0.000000
 965 SAT Solving time: 168.438953
 966 Result Computed in SAT solver:  SAT
 967 CSOLVER solve time: 168.603570
 968 Param PREPROCESS = 0     range=[0,1]
 969 Param ELEMENTOPTSETS = 1         range=[0,1]
 970 Param ELEMENTOPT = 1     range=[0,1]
 971 Param PROXYVARIABLE = 4          range=[1,5]
 972 Received score 168603569572.000000
 973 Mutating 1 settings
 974 &&&&&&&&Mutating&&&&&&&
 975 Param PREPROCESS = 1     range=[0,1]
 976 &&&&&&&&&&&&&&&&&&&&&&&
 977 **********************
 978 Polarity time: 0.003824
 979 Preprocess time: 0.012402
 980 Decompose Order: 0.000008
 981 Encoding Graph Time: 0.076665
 982 Elapse Encode time: 0.182050
 983 Is problem UNSAT after encoding: 0
 984 CNF Encode time: 0.000000
 985 SAT Solving time: 172.658556
 986 Result Computed in SAT solver:  SAT
 987 CSOLVER solve time: 172.840620
 988 Param PREPROCESS = 1     range=[0,1]
 989 Param ELEMENTOPTSETS = 1         range=[0,1]
 990 Param ELEMENTOPT = 1     range=[0,1]
 991 Param PROXYVARIABLE = 4          range=[1,5]
 992 Received score 172840619808.000000
 993 Mutating 1 settings
 994 &&&&&&&&Mutating&&&&&&&
 995 Param ELEMENTOPTSETS = 0         range=[0,1]
 996 &&&&&&&&&&&&&&&&&&&&&&&
 997 **********************
 998 Polarity time: 0.003732
 999 Preprocess time: 0.012341
1000 Decompose Order: 0.000007
1001 Encoding Graph Time: 0.038782
1002 Elapse Encode time: 1.084408
1003 Is problem UNSAT after encoding: 0
1004 CNF Encode time: 0.000000
1005 SAT Solving time: 196.086515
1006 Result Computed in SAT solver:  SAT
1007 CSOLVER solve time: 197.170934
1008 Param PREPROCESS = 1     range=[0,1]
1009 Param ELEMENTOPTSETS = 0         range=[0,1]
1010 Param ELEMENTOPT = 1     range=[0,1]
1011 Param PROXYVARIABLE = 4          range=[1,5]
1012 Received score 197170934389.000000
1013 Mutating 1 settings
1014 &&&&&&&&Mutating&&&&&&&
1015 Param ELEMENTOPT = 0     range=[0,1]
1016 &&&&&&&&&&&&&&&&&&&&&&&
1017 **********************
1018 Polarity time: 0.003798
1019 Preprocess time: 0.012459
1020 Decompose Order: 0.000007
1021 Encoding Graph Time: 0.005163
1022 Elapse Encode time: 3.646471
1023 Is problem UNSAT after encoding: 0
1024 CNF Encode time: 0.000000
1025 SAT Solving time: 196.787236
1026 Result Computed in SAT solver:  SAT
1027 CSOLVER solve time: 200.433720
1028 Param PREPROCESS = 1     range=[0,1]
1029 Param ELEMENTOPTSETS = 0         range=[0,1]
1030 Param ELEMENTOPT = 0     range=[0,1]
1031 Param PROXYVARIABLE = 4          range=[1,5]
1032 Received score 200433720214.000000
1033 Mutating 1 settings
1034 &&&&&&&&Mutating&&&&&&&
1035 Param PROXYVARIABLE = 2          range=[1,5]
1036 &&&&&&&&&&&&&&&&&&&&&&&
1037 **********************
1038 Polarity time: 0.003800
1039 Preprocess time: 0.012387
1040 Decompose Order: 0.000007
1041 Encoding Graph Time: 0.005125
1042 Elapse Encode time: 3.736603
1043 Is problem UNSAT after encoding: 0
1044 CNF Encode time: 0.000000
1045 SAT Solving time: 199.242297
1046 Result Computed in SAT solver:  SAT
1047 CSOLVER solve time: 202.978913
1048 Param PREPROCESS = 1     range=[0,1]
1049 Param ELEMENTOPTSETS = 0         range=[0,1]
1050 Param ELEMENTOPT = 0     range=[0,1]
1051 Param PROXYVARIABLE = 2          range=[1,5]
1052 Received score 202978913249.000000
1053 Mutating 1 settings
1054 &&&&&&&&Mutating&&&&&&&
1055 Param PROXYVARIABLE = 1          range=[1,5]
1056 &&&&&&&&&&&&&&&&&&&&&&&
1057 **********************
1058 Polarity time: 0.003796
1059 Preprocess time: 0.012289
1060 Decompose Order: 0.000008
1061 Encoding Graph Time: 0.005060
1062 Elapse Encode time: 3.702186
1063 Is problem UNSAT after encoding: 0
1064 CNF Encode time: 0.000000
1065 SAT Solving time: 230.594846
1066 Result Computed in SAT solver:  SAT
1067 CSOLVER solve time: 234.297043
1068 Param PREPROCESS = 1     range=[0,1]
1069 Param ELEMENTOPTSETS = 0         range=[0,1]
1070 Param ELEMENTOPT = 0     range=[0,1]
1071 Param PROXYVARIABLE = 1          range=[1,5]
1072 Received score 234297042838.000000
1073 Mutating 1 settings
1074 &&&&&&&&Mutating&&&&&&&
1075 Param PREPROCESS = 0     range=[0,1]
1076 &&&&&&&&&&&&&&&&&&&&&&&
1077 **********************
1078 Polarity time: 0.003742
1079 Preprocess time: 0.000014
1080 Decompose Order: 0.000004
1081 Encoding Graph Time: 0.005005
1082 Elapse Encode time: 3.657660
1083 Is problem UNSAT after encoding: 0
1084 CNF Encode time: 0.000000
1085 SAT Solving time: 213.216063
1086 Result Computed in SAT solver:  SAT
1087 CSOLVER solve time: 216.873736
1088 Param PREPROCESS = 0     range=[0,1]
1089 Param ELEMENTOPTSETS = 0         range=[0,1]
1090 Param ELEMENTOPT = 0     range=[0,1]
1091 Param PROXYVARIABLE = 1          range=[1,5]
1092 Received score 216873735962.000000
1093 Mutating 1 settings
1094 &&&&&&&&Mutating&&&&&&&
1095 Param ELEMENTOPTSETS = 1         range=[0,1]
1096 &&&&&&&&&&&&&&&&&&&&&&&
1097 **********************
1098 Polarity time: 0.003802
1099 Preprocess time: 0.000014
1100 Decompose Order: 0.000004
1101 Encoding Graph Time: 0.005021
1102 Elapse Encode time: 3.666980
1103 Is problem UNSAT after encoding: 0
1104 CNF Encode time: 0.000000
1105 SAT Solving time: 190.150496
1106 Result Computed in SAT solver:  SAT
1107 CSOLVER solve time: 193.817488
1108 Param PREPROCESS = 0     range=[0,1]
1109 Param ELEMENTOPTSETS = 1         range=[0,1]
1110 Param ELEMENTOPT = 0     range=[0,1]
1111 Param PROXYVARIABLE = 1          range=[1,5]
1112 Received score 193817487748.000000
1113 Mutating 1 settings
1114 &&&&&&&&Mutating&&&&&&&
1115 Param PREPROCESS = 1     range=[0,1]
1116 &&&&&&&&&&&&&&&&&&&&&&&
1117 **********************
1118 Polarity time: 0.003708
1119 Preprocess time: 0.012303
1120 Decompose Order: 0.000007
1121 Encoding Graph Time: 0.005073
1122 Elapse Encode time: 3.691539
1123 Is problem UNSAT after encoding: 0
1124 CNF Encode time: 0.000000
1125 SAT Solving time: 190.448437
1126 Result Computed in SAT solver:  SAT
1127 CSOLVER solve time: 194.139991
1128 Param PREPROCESS = 1     range=[0,1]
1129 Param ELEMENTOPTSETS = 1         range=[0,1]
1130 Param ELEMENTOPT = 0     range=[0,1]
1131 Param PROXYVARIABLE = 1          range=[1,5]
1132 Received score 194139990727.000000
1133 Mutating 1 settings
1134 &&&&&&&&Mutating&&&&&&&
1135 Param PROXYVARIABLE = 2          range=[1,5]
1136 &&&&&&&&&&&&&&&&&&&&&&&
1137 **********************
1138 Polarity time: 0.003739
1139 Preprocess time: 0.012630
1140 Decompose Order: 0.000007
1141 Encoding Graph Time: 0.005020
1142 Elapse Encode time: 3.672934
1143 Is problem UNSAT after encoding: 0
1144 CNF Encode time: 0.000000
1145 SAT Solving time: 209.209322
1146 Result Computed in SAT solver:  SAT
1147 CSOLVER solve time: 212.882268
1148 Param PREPROCESS = 1     range=[0,1]
1149 Param ELEMENTOPTSETS = 1         range=[0,1]
1150 Param ELEMENTOPT = 0     range=[0,1]
1151 Param PROXYVARIABLE = 2          range=[1,5]
1152 Received score 212882267611.000000
1153 Mutating 1 settings
1154 &&&&&&&&Mutating&&&&&&&
1155 Param PROXYVARIABLE = 5          range=[1,5]
1156 &&&&&&&&&&&&&&&&&&&&&&&
1157 **********************
1158 Polarity time: 0.003949
1159 Preprocess time: 0.012802
1160 Decompose Order: 0.000008
1161 Encoding Graph Time: 0.005295
1162 Elapse Encode time: 3.687023
1163 Is problem UNSAT after encoding: 0
1164 CNF Encode time: 0.000000
1165 SAT Solving time: 213.265444
1166 Result Computed in SAT solver:  SAT
1167 CSOLVER solve time: 216.952480
1168 Param PREPROCESS = 1     range=[0,1]
1169 Param ELEMENTOPTSETS = 1         range=[0,1]
1170 Param ELEMENTOPT = 0     range=[0,1]
1171 Param PROXYVARIABLE = 5          range=[1,5]
1172 Received score 216952479581.000000
1173 Mutating 1 settings
1174 &&&&&&&&Mutating&&&&&&&
1175 Param PROXYVARIABLE = 1          range=[1,5]
1176 &&&&&&&&&&&&&&&&&&&&&&&
1177 **********************
1178 Polarity time: 0.003912
1179 Preprocess time: 0.012691
1180 Decompose Order: 0.000007
1181 Encoding Graph Time: 0.005183
1182 Elapse Encode time: 3.664000
1183 Is problem UNSAT after encoding: 0
1184 CNF Encode time: 0.000000
1185 SAT Solving time: 232.840413
1186 Result Computed in SAT solver:  SAT
1187 CSOLVER solve time: 236.504427
1188 Param PREPROCESS = 1     range=[0,1]
1189 Param ELEMENTOPTSETS = 1         range=[0,1]
1190 Param ELEMENTOPT = 0     range=[0,1]
1191 Param PROXYVARIABLE = 1          range=[1,5]
1192 Received score 236504426550.000000
1193 Mutating 1 settings
1194 &&&&&&&&Mutating&&&&&&&
1195 Param PROXYVARIABLE = 3          range=[1,5]
1196 &&&&&&&&&&&&&&&&&&&&&&&
1197 **********************
1198 Polarity time: 0.003916
1199 Preprocess time: 0.012733
1200 Decompose Order: 0.000007
1201 Encoding Graph Time: 0.005209
1202 Elapse Encode time: 3.735942
1203 Is problem UNSAT after encoding: 0
1204 CNF Encode time: 0.000000
1205 SAT Solving time: 197.100228
1206 Result Computed in SAT solver:  SAT
1207 CSOLVER solve time: 200.836183
1208 Param PREPROCESS = 1     range=[0,1]
1209 Param ELEMENTOPTSETS = 1         range=[0,1]
1210 Param ELEMENTOPT = 0     range=[0,1]
1211 Param PROXYVARIABLE = 3          range=[1,5]
1212 Received score 200836183201.000000
1213 Mutating 1 settings
1214 &&&&&&&&Mutating&&&&&&&
1215 Param PROXYVARIABLE = 5          range=[1,5]
1216 &&&&&&&&&&&&&&&&&&&&&&&
1217 **********************
1218 Polarity time: 0.003979
1219 Preprocess time: 0.012754
1220 Decompose Order: 0.000008
1221 Encoding Graph Time: 0.005272
1222 Elapse Encode time: 3.688929
1223 Is problem UNSAT after encoding: 0
1224 CNF Encode time: 0.000000
1225 SAT Solving time: 194.572067
1226 Result Computed in SAT solver:  SAT
1227 CSOLVER solve time: 198.261009
1228 Param PREPROCESS = 1     range=[0,1]
1229 Param ELEMENTOPTSETS = 1         range=[0,1]
1230 Param ELEMENTOPT = 0     range=[0,1]
1231 Param PROXYVARIABLE = 5          range=[1,5]
1232 Received score 198261009074.000000
1233 Mutating 1 settings
1234 &&&&&&&&Mutating&&&&&&&
1235 Param ELEMENTOPTSETS = 0         range=[0,1]
1236 &&&&&&&&&&&&&&&&&&&&&&&
1237 **********************
1238 Polarity time: 0.003906
1239 Preprocess time: 0.012603
1240 Decompose Order: 0.000007
1241 Encoding Graph Time: 0.005185
1242 Elapse Encode time: 3.679947
1243 Is problem UNSAT after encoding: 0
1244 CNF Encode time: 0.000000
1245 SAT Solving time: 195.583452
1246 Result Computed in SAT solver:  SAT
1247 CSOLVER solve time: 199.263412
1248 Param PREPROCESS = 1     range=[0,1]
1249 Param ELEMENTOPTSETS = 0         range=[0,1]
1250 Param ELEMENTOPT = 0     range=[0,1]
1251 Param PROXYVARIABLE = 5          range=[1,5]
1252 Received score 199263412053.000000
1253 Mutating 1 settings
1254 &&&&&&&&Mutating&&&&&&&
1255 Param ELEMENTOPTSETS = 0         range=[0,1]
1256 &&&&&&&&&&&&&&&&&&&&&&&
1257 **********************
1258 Polarity time: 0.003884
1259 Preprocess time: 0.012608
1260 Decompose Order: 0.000007
1261 Encoding Graph Time: 0.005214
1262 Elapse Encode time: 3.673056
1263 Is problem UNSAT after encoding: 0
1264 CNF Encode time: 0.000000
1265 SAT Solving time: 196.515939
1266 Result Computed in SAT solver:  SAT
1267 CSOLVER solve time: 200.189008
1268 Param PREPROCESS = 1     range=[0,1]
1269 Param ELEMENTOPTSETS = 0         range=[0,1]
1270 Param ELEMENTOPT = 0     range=[0,1]
1271 Param PROXYVARIABLE = 5          range=[1,5]
1272 Received score 200189008299.000000
1273 Mutating 1 settings
1274 &&&&&&&&Mutating&&&&&&&
1275 Param ELEMENTOPTSETS = 1         range=[0,1]
1276 &&&&&&&&&&&&&&&&&&&&&&&
1277 **********************
1278 Polarity time: 0.004310
1279 Preprocess time: 0.013806
1280 Decompose Order: 0.000008
1281 Encoding Graph Time: 0.005863
1282 Elapse Encode time: 3.672479
1283 Is problem UNSAT after encoding: 0
1284 CNF Encode time: 0.000000
1285 SAT Solving time: 218.462610
1286 Result Computed in SAT solver:  SAT
1287 CSOLVER solve time: 222.135100
1288 Param PREPROCESS = 1     range=[0,1]
1289 Param ELEMENTOPTSETS = 1         range=[0,1]
1290 Param ELEMENTOPT = 0     range=[0,1]
1291 Param PROXYVARIABLE = 5          range=[1,5]
1292 Received score 222135099600.000000
1293 Mutating 1 settings
1294 &&&&&&&&Mutating&&&&&&&
1295 Param PROXYVARIABLE = 4          range=[1,5]
1296 &&&&&&&&&&&&&&&&&&&&&&&
1297 **********************
1298 Polarity time: 0.003947
1299 Preprocess time: 0.012763
1300 Decompose Order: 0.000007
1301 Encoding Graph Time: 0.005078
1302 Elapse Encode time: 3.672946
1303 Is problem UNSAT after encoding: 0
1304 CNF Encode time: 0.000000
1305 SAT Solving time: 216.175640
1306 Result Computed in SAT solver:  SAT
1307 CSOLVER solve time: 219.848599
1308 Param PREPROCESS = 1     range=[0,1]
1309 Param ELEMENTOPTSETS = 0         range=[0,1]
1310 Param ELEMENTOPT = 0     range=[0,1]
1311 Param PROXYVARIABLE = 4          range=[1,5]
1312 Received score 219848599063.000000
1313 Mutating 1 settings
1314 &&&&&&&&Mutating&&&&&&&
1315 Param ELEMENTOPTSETS = 1         range=[0,1]
1316 &&&&&&&&&&&&&&&&&&&&&&&
1317 **********************
1318 Polarity time: 0.003876
1319 Preprocess time: 0.012703
1320 Decompose Order: 0.000007
1321 Encoding Graph Time: 0.005016
1322 Elapse Encode time: 3.681634
1323 Is problem UNSAT after encoding: 0
1324 CNF Encode time: 0.000000
1325 SAT Solving time: 189.323384
1326 Result Computed in SAT solver:  SAT
1327 CSOLVER solve time: 193.005032
1328 Param PREPROCESS = 1     range=[0,1]
1329 Param ELEMENTOPTSETS = 1         range=[0,1]
1330 Param ELEMENTOPT = 0     range=[0,1]
1331 Param PROXYVARIABLE = 5          range=[1,5]
1332 Received score 193005031629.000000
1333 Mutating 1 settings
1334 &&&&&&&&Mutating&&&&&&&
1335 Param PROXYVARIABLE = 4          range=[1,5]
1336 &&&&&&&&&&&&&&&&&&&&&&&
1337 **********************
1338 Polarity time: 0.003947
1339 Preprocess time: 0.012753
1340 Decompose Order: 0.000007
1341 Encoding Graph Time: 0.005069
1342 Elapse Encode time: 3.690430
1343 Is problem UNSAT after encoding: 0
1344 CNF Encode time: 0.000000
1345 SAT Solving time: 213.451942
1346 Result Computed in SAT solver:  SAT
1347 CSOLVER solve time: 217.142385
1348 Param PREPROCESS = 1     range=[0,1]
1349 Param ELEMENTOPTSETS = 1         range=[0,1]
1350 Param ELEMENTOPT = 0     range=[0,1]
1351 Param PROXYVARIABLE = 4          range=[1,5]
1352 Received score 217142384630.000000
1353 Mutating 1 settings
1354 &&&&&&&&Mutating&&&&&&&
1355 Param ELEMENTOPT = 1     range=[0,1]
1356 &&&&&&&&&&&&&&&&&&&&&&&
1357 **********************
1358 Polarity time: 0.003889
1359 Preprocess time: 0.012737
1360 Decompose Order: 0.000006
1361 Encoding Graph Time: 0.077964
1362 Elapse Encode time: 0.175904
1363 Is problem UNSAT after encoding: 0
1364 CNF Encode time: 0.000000
1365 SAT Solving time: 168.975013
1366 Result Computed in SAT solver:  SAT
1367 CSOLVER solve time: 169.150954
1368 Param PREPROCESS = 1     range=[0,1]
1369 Param ELEMENTOPTSETS = 1         range=[0,1]
1370 Param ELEMENTOPT = 1     range=[0,1]
1371 Param PROXYVARIABLE = 5          range=[1,5]
1372 Received score 169150954004.000000
1373 Mutating 1 settings
1374 &&&&&&&&Mutating&&&&&&&
1375 Param PREPROCESS = 0     range=[0,1]
1376 &&&&&&&&&&&&&&&&&&&&&&&
1377 **********************
1378 Polarity time: 0.003954
1379 Preprocess time: 0.000011
1380 Decompose Order: 0.000003
1381 Encoding Graph Time: 0.078389
1382 Elapse Encode time: 0.163362
1383 Is problem UNSAT after encoding: 0
1384 CNF Encode time: 0.000000
1385 SAT Solving time: 162.638351
1386 Result Computed in SAT solver:  SAT
1387 CSOLVER solve time: 162.801724
1388 Param PREPROCESS = 0     range=[0,1]
1389 Param ELEMENTOPTSETS = 1         range=[0,1]
1390 Param ELEMENTOPT = 1     range=[0,1]
1391 Param PROXYVARIABLE = 5          range=[1,5]
1392 Received score 162801723981.000000
1393 Mutating 1 settings
1394 &&&&&&&&Mutating&&&&&&&
1395 Param PREPROCESS = 1     range=[0,1]
1396 &&&&&&&&&&&&&&&&&&&&&&&
1397 **********************
1398 Polarity time: 0.003933
1399 Preprocess time: 0.012814
1400 Decompose Order: 0.000007
1401 Encoding Graph Time: 0.077829
1402 Elapse Encode time: 0.175715
1403 Is problem UNSAT after encoding: 0
1404 CNF Encode time: 0.000000
1405 SAT Solving time: 167.368509
1406 Result Computed in SAT solver:  SAT
1407 CSOLVER solve time: 167.544236
1408 Param PREPROCESS = 1     range=[0,1]
1409 Param ELEMENTOPTSETS = 1         range=[0,1]
1410 Param ELEMENTOPT = 1     range=[0,1]
1411 Param PROXYVARIABLE = 5          range=[1,5]
1412 Received score 167544235684.000000
1413 Mutating 1 settings
1414 &&&&&&&&Mutating&&&&&&&
1415 Param ELEMENTOPTSETS = 0         range=[0,1]
1416 &&&&&&&&&&&&&&&&&&&&&&&
1417 **********************
1418 Polarity time: 0.003915
1419 Preprocess time: 0.012472
1420 Decompose Order: 0.000008
1421 Encoding Graph Time: 0.038816
1422 Elapse Encode time: 1.084491
1423 Is problem UNSAT after encoding: 0
1424 CNF Encode time: 0.000000
1425 SAT Solving time: 157.594607
1426 Result Computed in SAT solver:  SAT
1427 CSOLVER solve time: 158.679111
1428 Param PREPROCESS = 1     range=[0,1]
1429 Param ELEMENTOPTSETS = 0         range=[0,1]
1430 Param ELEMENTOPT = 1     range=[0,1]
1431 Param PROXYVARIABLE = 5          range=[1,5]
1432 Received score 158679110536.000000
1433 Mutating 1 settings
1434 &&&&&&&&Mutating&&&&&&&
1435 Param PROXYVARIABLE = 3          range=[1,5]
1436 &&&&&&&&&&&&&&&&&&&&&&&
1437 **********************
1438 Polarity time: 0.003909
1439 Preprocess time: 0.012711
1440 Decompose Order: 0.000007
1441 Encoding Graph Time: 0.039867
1442 Elapse Encode time: 1.087709
1443 Is problem UNSAT after encoding: 0
1444 CNF Encode time: 0.000000
1445 SAT Solving time: 196.644086
1446 Result Computed in SAT solver:  SAT
1447 CSOLVER solve time: 197.731808
1448 Param PREPROCESS = 1     range=[0,1]
1449 Param ELEMENTOPTSETS = 0         range=[0,1]
1450 Param ELEMENTOPT = 1     range=[0,1]
1451 Param PROXYVARIABLE = 3          range=[1,5]
1452 Received score 197731807552.000000
1453 Mutating 1 settings
1454 &&&&&&&&Mutating&&&&&&&
1455 Param ELEMENTOPT = 0     range=[0,1]
1456 &&&&&&&&&&&&&&&&&&&&&&&
1457 **********************
1458 Polarity time: 0.003935
1459 Preprocess time: 0.012286
1460 Decompose Order: 0.000008
1461 Encoding Graph Time: 0.005066
1462 Elapse Encode time: 3.692239
1463 Is problem UNSAT after encoding: 0
1464 CNF Encode time: 0.000000
1465 SAT Solving time: 212.237224
1466 Result Computed in SAT solver:  SAT
1467 CSOLVER solve time: 215.929477
1468 Param PREPROCESS = 1     range=[0,1]
1469 Param ELEMENTOPTSETS = 0         range=[0,1]
1470 Param ELEMENTOPT = 0     range=[0,1]
1471 Param PROXYVARIABLE = 5          range=[1,5]
1472 Received score 215929476801.000000
1473 Mutating 1 settings
1474 &&&&&&&&Mutating&&&&&&&
1475 Param ELEMENTOPTSETS = 1         range=[0,1]
1476 &&&&&&&&&&&&&&&&&&&&&&&
1477 **********************
1478 Polarity time: 0.003914
1479 Preprocess time: 0.012774
1480 Decompose Order: 0.000007
1481 Encoding Graph Time: 0.077064
1482 Elapse Encode time: 0.175014
1483 Is problem UNSAT after encoding: 0
1484 CNF Encode time: 0.000000
1485 SAT Solving time: 163.079861
1486 Result Computed in SAT solver:  SAT
1487 CSOLVER solve time: 163.254888
1488 Param PREPROCESS = 1     range=[0,1]
1489 Param ELEMENTOPTSETS = 1         range=[0,1]
1490 Param ELEMENTOPT = 1     range=[0,1]
1491 Param PROXYVARIABLE = 5          range=[1,5]
1492 Received score 163254887957.000000
1493 Mutating 1 settings
1494 &&&&&&&&Mutating&&&&&&&
1495 Param ELEMENTOPTSETS = 0         range=[0,1]
1496 &&&&&&&&&&&&&&&&&&&&&&&
1497 **********************
1498 Polarity time: 0.003723
1499 Preprocess time: 0.012345
1500 Decompose Order: 0.000007
1501 Encoding Graph Time: 0.038708
1502 Elapse Encode time: 1.086417
1503 Is problem UNSAT after encoding: 0
1504 CNF Encode time: 0.000000
1505 SAT Solving time: 173.854583
1506 Result Computed in SAT solver:  SAT
1507 CSOLVER solve time: 174.941041
1508 Param PREPROCESS = 1     range=[0,1]
1509 Param ELEMENTOPTSETS = 0         range=[0,1]
1510 Param ELEMENTOPT = 1     range=[0,1]
1511 Param PROXYVARIABLE = 5          range=[1,5]
1512 Received score 174941041047.000000
1513 Mutating 1 settings
1514 &&&&&&&&Mutating&&&&&&&
1515 Param ELEMENTOPT = 0     range=[0,1]
1516 &&&&&&&&&&&&&&&&&&&&&&&
1517 **********************
1518 Polarity time: 0.003894
1519 Preprocess time: 0.012772
1520 Decompose Order: 0.000007
1521 Encoding Graph Time: 0.005053
1522 Elapse Encode time: 3.645309
1523 Is problem UNSAT after encoding: 0
1524 CNF Encode time: 0.000000
1525 SAT Solving time: 193.549004
1526 Result Computed in SAT solver:  SAT
1527 CSOLVER solve time: 197.194326
1528 Param PREPROCESS = 1     range=[0,1]
1529 Param ELEMENTOPTSETS = 0         range=[0,1]
1530 Param ELEMENTOPT = 0     range=[0,1]
1531 Param PROXYVARIABLE = 5          range=[1,5]
1532 Received score 197194326176.000000
1533 Mutating 1 settings
1534 &&&&&&&&Mutating&&&&&&&
1535 Param ELEMENTOPT = 1     range=[0,1]
1536 &&&&&&&&&&&&&&&&&&&&&&&
1537 **********************
1538 Polarity time: 0.003943
1539 Preprocess time: 0.012657
1540 Decompose Order: 0.000008
1541 Encoding Graph Time: 0.039015
1542 Elapse Encode time: 1.086697
1543 Is problem UNSAT after encoding: 0
1544 CNF Encode time: 0.000000
1545 SAT Solving time: 170.687788
1546 Result Computed in SAT solver:  SAT
1547 CSOLVER solve time: 171.774497
1548 Param PREPROCESS = 1     range=[0,1]
1549 Param ELEMENTOPTSETS = 0         range=[0,1]
1550 Param ELEMENTOPT = 1     range=[0,1]
1551 Param PROXYVARIABLE = 5          range=[1,5]
1552 Received score 171774497026.000000
1553 Mutating 1 settings
1554 &&&&&&&&Mutating&&&&&&&
1555 Param PROXYVARIABLE = 4          range=[1,5]
1556 &&&&&&&&&&&&&&&&&&&&&&&
1557 **********************
1558 Polarity time: 0.003915
1559 Preprocess time: 0.012660
1560 Decompose Order: 0.000006
1561 Encoding Graph Time: 0.038827
1562 Elapse Encode time: 1.091702
1563 Is problem UNSAT after encoding: 0
1564 CNF Encode time: 0.000000
1565 SAT Solving time: 211.483507
1566 Result Computed in SAT solver:  SAT
1567 CSOLVER solve time: 212.575221
1568 Param PREPROCESS = 1     range=[0,1]
1569 Param ELEMENTOPTSETS = 0         range=[0,1]
1570 Param ELEMENTOPT = 1     range=[0,1]
1571 Param PROXYVARIABLE = 4          range=[1,5]
1572 Received score 212575220713.000000
1573 Mutating 1 settings
1574 &&&&&&&&Mutating&&&&&&&
1575 Param PREPROCESS = 0     range=[0,1]
1576 &&&&&&&&&&&&&&&&&&&&&&&
1577 **********************
1578 Polarity time: 0.003908
1579 Preprocess time: 0.000011
1580 Decompose Order: 0.000003
1581 Encoding Graph Time: 0.040577
1582 Elapse Encode time: 1.075268
1583 Is problem UNSAT after encoding: 0
1584 CNF Encode time: 0.000000
1585 SAT Solving time: 175.800611
1586 Result Computed in SAT solver:  SAT
1587 CSOLVER solve time: 176.875891
1588 Param PREPROCESS = 0     range=[0,1]
1589 Param ELEMENTOPTSETS = 0         range=[0,1]
1590 Param ELEMENTOPT = 1     range=[0,1]
1591 Param PROXYVARIABLE = 5          range=[1,5]
1592 Received score 176875890670.000000
1593 Mutating 1 settings
1594 &&&&&&&&Mutating&&&&&&&
1595 Param PREPROCESS = 1     range=[0,1]
1596 &&&&&&&&&&&&&&&&&&&&&&&
1597 **********************
1598 Polarity time: 0.003938
1599 Preprocess time: 0.012794
1600 Decompose Order: 0.000008
1601 Encoding Graph Time: 0.038757
1602 Elapse Encode time: 1.091536
1603 Is problem UNSAT after encoding: 0
1604 CNF Encode time: 0.000000
1605 SAT Solving time: 186.924864
1606 Result Computed in SAT solver:  SAT
1607 CSOLVER solve time: 188.016412
1608 Param PREPROCESS = 1     range=[0,1]
1609 Param ELEMENTOPTSETS = 0         range=[0,1]
1610 Param ELEMENTOPT = 1     range=[0,1]
1611 Param PROXYVARIABLE = 5          range=[1,5]
1612 Received score 188016412411.000000
1613 Mutating 1 settings
1614 &&&&&&&&Mutating&&&&&&&
1615 Param ELEMENTOPT = 0     range=[0,1]
1616 &&&&&&&&&&&&&&&&&&&&&&&
1617 **********************
1618 Polarity time: 0.003900
1619 Preprocess time: 0.012565
1620 Decompose Order: 0.000007
1621 Encoding Graph Time: 0.005207
1622 Elapse Encode time: 3.682209
1623 Is problem UNSAT after encoding: 0
1624 CNF Encode time: 0.000000
1625 SAT Solving time: 192.647723
1626 Result Computed in SAT solver:  SAT
1627 CSOLVER solve time: 196.329945
1628 Param PREPROCESS = 1     range=[0,1]
1629 Param ELEMENTOPTSETS = 0         range=[0,1]
1630 Param ELEMENTOPT = 0     range=[0,1]
1631 Param PROXYVARIABLE = 5          range=[1,5]
1632 Received score 196329945231.000000
1633 Mutating 1 settings
1634 &&&&&&&&Mutating&&&&&&&
1635 Param ELEMENTOPT = 1     range=[0,1]
1636 &&&&&&&&&&&&&&&&&&&&&&&
1637 **********************
1638 Polarity time: 0.003941
1639 Preprocess time: 0.012756
1640 Decompose Order: 0.000037
1641 Encoding Graph Time: 0.038824
1642 Elapse Encode time: 1.083426
1643 Is problem UNSAT after encoding: 0
1644 CNF Encode time: 0.000000
1645 SAT Solving time: 179.833990
1646 Result Computed in SAT solver:  SAT
1647 CSOLVER solve time: 180.917429
1648 Param PREPROCESS = 1     range=[0,1]
1649 Param ELEMENTOPTSETS = 0         range=[0,1]
1650 Param ELEMENTOPT = 1     range=[0,1]
1651 Param PROXYVARIABLE = 5          range=[1,5]
1652 Received score 180917428919.000000
1653 Mutating 1 settings
1654 &&&&&&&&Mutating&&&&&&&
1655 Param ELEMENTOPTSETS = 1         range=[0,1]
1656 &&&&&&&&&&&&&&&&&&&&&&&
1657 **********************
1658 Polarity time: 0.003811
1659 Preprocess time: 0.012519
1660 Decompose Order: 0.000007
1661 Encoding Graph Time: 0.079074
1662 Elapse Encode time: 0.176448
1663 Is problem UNSAT after encoding: 0
1664 CNF Encode time: 0.000000
1665 SAT Solving time: 170.526937
1666 Result Computed in SAT solver:  SAT
1667 CSOLVER solve time: 170.703396
1668 Param PREPROCESS = 1     range=[0,1]
1669 Param ELEMENTOPTSETS = 1         range=[0,1]
1670 Param ELEMENTOPT = 1     range=[0,1]
1671 Param PROXYVARIABLE = 5          range=[1,5]
1672 Received score 170703395848.000000
1673 Mutating 1 settings
1674 &&&&&&&&Mutating&&&&&&&
1675 Param ELEMENTOPT = 0     range=[0,1]
1676 &&&&&&&&&&&&&&&&&&&&&&&
1677 **********************
1678 Polarity time: 0.003958
1679 Preprocess time: 0.012776
1680 Decompose Order: 0.000007
1681 Encoding Graph Time: 0.005126
1682 Elapse Encode time: 3.666501
1683 Is problem UNSAT after encoding: 0
1684 CNF Encode time: 0.000000
1685 SAT Solving time: 199.348463
1686 Result Computed in SAT solver:  SAT
1687 CSOLVER solve time: 203.014978
1688 Param PREPROCESS = 1     range=[0,1]
1689 Param ELEMENTOPTSETS = 1         range=[0,1]
1690 Param ELEMENTOPT = 0     range=[0,1]
1691 Param PROXYVARIABLE = 5          range=[1,5]
1692 Received score 203014977559.000000
1693 Mutating 1 settings
1694 &&&&&&&&Mutating&&&&&&&
1695 Param PREPROCESS = 0     range=[0,1]
1696 &&&&&&&&&&&&&&&&&&&&&&&
1697 **********************
1698 Polarity time: 0.003882
1699 Preprocess time: 0.000010
1700 Decompose Order: 0.000003
1701 Encoding Graph Time: 0.077627
1702 Elapse Encode time: 0.162374
1703 Is problem UNSAT after encoding: 0
1704 CNF Encode time: 0.000001
1705 SAT Solving time: 167.578118
1706 Result Computed in SAT solver:  SAT
1707 CSOLVER solve time: 167.740504
1708 Param PREPROCESS = 0     range=[0,1]
1709 Param ELEMENTOPTSETS = 1         range=[0,1]
1710 Param ELEMENTOPT = 1     range=[0,1]
1711 Param PROXYVARIABLE = 5          range=[1,5]
1712 Received score 167740503520.000000
1713 Mutating 1 settings
1714 &&&&&&&&Mutating&&&&&&&
1715 Param ELEMENTOPT = 0     range=[0,1]
1716 &&&&&&&&&&&&&&&&&&&&&&&
1717 **********************
1718 Polarity time: 0.003840
1719 Preprocess time: 0.000011
1720 Decompose Order: 0.000004
1721 Encoding Graph Time: 0.004883
1722 Elapse Encode time: 3.645558
1723 Is problem UNSAT after encoding: 0
1724 CNF Encode time: 0.000000
1725 SAT Solving time: 202.727908
1726 Result Computed in SAT solver:  SAT
1727 CSOLVER solve time: 206.373478
1728 Param PREPROCESS = 0     range=[0,1]
1729 Param ELEMENTOPTSETS = 1         range=[0,1]
1730 Param ELEMENTOPT = 0     range=[0,1]
1731 Param PROXYVARIABLE = 5          range=[1,5]
1732 Received score 206373478044.000000
1733 Mutating 1 settings
1734 &&&&&&&&Mutating&&&&&&&
1735 Param PREPROCESS = 1     range=[0,1]
1736 &&&&&&&&&&&&&&&&&&&&&&&
1737 **********************
1738 Polarity time: 0.003943
1739 Preprocess time: 0.012472
1740 Decompose Order: 0.000007
1741 Encoding Graph Time: 0.076030
1742 Elapse Encode time: 0.173739
1743 Is problem UNSAT after encoding: 0
1744 CNF Encode time: 0.000000
1745 SAT Solving time: 164.271451
1746 Result Computed in SAT solver:  SAT
1747 CSOLVER solve time: 164.445200
1748 Param PREPROCESS = 1     range=[0,1]
1749 Param ELEMENTOPTSETS = 1         range=[0,1]
1750 Param ELEMENTOPT = 1     range=[0,1]
1751 Param PROXYVARIABLE = 5          range=[1,5]
1752 Received score 164445200208.000000
1753 Mutating 1 settings
1754 &&&&&&&&Mutating&&&&&&&
1755 Param ELEMENTOPT = 0     range=[0,1]
1756 &&&&&&&&&&&&&&&&&&&&&&&
1757 **********************
1758 Polarity time: 0.003937
1759 Preprocess time: 0.012865
1760 Decompose Order: 0.000009
1761 Encoding Graph Time: 0.005197
1762 Elapse Encode time: 3.736503
1763 Is problem UNSAT after encoding: 0
1764 CNF Encode time: 0.000000
1765 SAT Solving time: 194.532342
1766 Result Computed in SAT solver:  SAT
1767 CSOLVER solve time: 198.268858
1768 Param PREPROCESS = 1     range=[0,1]
1769 Param ELEMENTOPTSETS = 1         range=[0,1]
1770 Param ELEMENTOPT = 0     range=[0,1]
1771 Param PROXYVARIABLE = 5          range=[1,5]
1772 Received score 198268858437.000000
1773 Mutating 1 settings
1774 &&&&&&&&Mutating&&&&&&&
1775 Param ELEMENTOPT = 0     range=[0,1]
1776 &&&&&&&&&&&&&&&&&&&&&&&
1777 **********************
1778 Polarity time: 0.003731
1779 Preprocess time: 0.012372
1780 Decompose Order: 0.000007
1781 Encoding Graph Time: 0.005044
1782 Elapse Encode time: 3.673733
1783 Is problem UNSAT after encoding: 0
1784 CNF Encode time: 0.000000
1785 SAT Solving time: 195.935119
1786 Result Computed in SAT solver:  SAT
1787 CSOLVER solve time: 199.608864
1788 Param PREPROCESS = 1     range=[0,1]
1789 Param ELEMENTOPTSETS = 1         range=[0,1]
1790 Param ELEMENTOPT = 0     range=[0,1]
1791 Param PROXYVARIABLE = 5          range=[1,5]
1792 Received score 199608864374.000000
1793 Mutating 1 settings
1794 &&&&&&&&Mutating&&&&&&&
1795 Param PREPROCESS = 0     range=[0,1]
1796 &&&&&&&&&&&&&&&&&&&&&&&
1797 **********************
1798 Polarity time: 0.003797
1799 Preprocess time: 0.000014
1800 Decompose Order: 0.000005
1801 Encoding Graph Time: 0.005054
1802 Elapse Encode time: 3.657081
1803 Is problem UNSAT after encoding: 0
1804 CNF Encode time: 0.000000
1805 SAT Solving time: 187.706833
1806 Result Computed in SAT solver:  SAT
1807 CSOLVER solve time: 191.363926
1808 Param PREPROCESS = 0     range=[0,1]
1809 Param ELEMENTOPTSETS = 1         range=[0,1]
1810 Param ELEMENTOPT = 0     range=[0,1]
1811 Param PROXYVARIABLE = 5          range=[1,5]
1812 Received score 191363925511.000000
1813 Mutating 1 settings
1814 &&&&&&&&Mutating&&&&&&&
1815 Param PROXYVARIABLE = 3          range=[1,5]
1816 &&&&&&&&&&&&&&&&&&&&&&&
1817 **********************
1818 Polarity time: 0.003741
1819 Preprocess time: 0.000013
1820 Decompose Order: 0.000004
1821 Encoding Graph Time: 0.005019
1822 Elapse Encode time: 3.656541
1823 Is problem UNSAT after encoding: 0
1824 CNF Encode time: 0.000000
1825 SAT Solving time: 188.132679
1826 Result Computed in SAT solver:  SAT
1827 CSOLVER solve time: 191.789232
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 191789231675.000000
1833 Mutating 1 settings
1834 &&&&&&&&Mutating&&&&&&&
1835 Param PROXYVARIABLE = 2          range=[1,5]
1836 &&&&&&&&&&&&&&&&&&&&&&&
1837 **********************
1838 Polarity time: 0.003762
1839 Preprocess time: 0.000014
1840 Decompose Order: 0.000004
1841 Encoding Graph Time: 0.005036
1842 Elapse Encode time: 3.622179
1843 Is problem UNSAT after encoding: 0
1844 CNF Encode time: 0.000000
1845 SAT Solving time: 200.267486
1846 Result Computed in SAT solver:  SAT
1847 CSOLVER solve time: 203.889678
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 203889677771.000000
1853 Mutating 1 settings
1854 &&&&&&&&Mutating&&&&&&&
1855 Param ELEMENTOPTSETS = 0         range=[0,1]
1856 &&&&&&&&&&&&&&&&&&&&&&&
1857 **********************
1858 Polarity time: 0.003778
1859 Preprocess time: 0.000014
1860 Decompose Order: 0.000004
1861 Encoding Graph Time: 0.005054
1862 Elapse Encode time: 3.682708
1863 Is problem UNSAT after encoding: 0
1864 CNF Encode time: 0.000000
1865 SAT Solving time: 176.876994
1866 Result Computed in SAT solver:  SAT
1867 CSOLVER solve time: 180.559715
1868 Param PREPROCESS = 0     range=[0,1]
1869 Param ELEMENTOPTSETS = 0         range=[0,1]
1870 Param ELEMENTOPT = 0     range=[0,1]
1871 Param PROXYVARIABLE = 2          range=[1,5]
1872 Received score 180559715113.000000
1873 Mutating 1 settings
1874 &&&&&&&&Mutating&&&&&&&
1875 Param ELEMENTOPT = 1     range=[0,1]
1876 &&&&&&&&&&&&&&&&&&&&&&&
1877 **********************
1878 Polarity time: 0.003776
1879 Preprocess time: 0.000014
1880 Decompose Order: 0.000004
1881 Encoding Graph Time: 0.039241
1882 Elapse Encode time: 1.071814
1883 Is problem UNSAT after encoding: 0
1884 CNF Encode time: 0.000000
1885 SAT Solving time: 179.120002
1886 Result Computed in SAT solver:  SAT
1887 CSOLVER solve time: 180.191829
1888 Param PREPROCESS = 0     range=[0,1]
1889 Param ELEMENTOPTSETS = 0         range=[0,1]
1890 Param ELEMENTOPT = 1     range=[0,1]
1891 Param PROXYVARIABLE = 2          range=[1,5]
1892 Received score 180191828542.000000
1893 Mutating 1 settings
1894 &&&&&&&&Mutating&&&&&&&
1895 Param PROXYVARIABLE = 3          range=[1,5]
1896 &&&&&&&&&&&&&&&&&&&&&&&
1897 **********************
1898 Polarity time: 0.003753
1899 Preprocess time: 0.000014
1900 Decompose Order: 0.000005
1901 Encoding Graph Time: 0.038972
1902 Elapse Encode time: 1.077591
1903 Is problem UNSAT after encoding: 0
1904 CNF Encode time: 0.000000
1905 SAT Solving time: 173.747742
1906 Result Computed in SAT solver:  SAT
1907 CSOLVER solve time: 174.825345
1908 Param PREPROCESS = 0     range=[0,1]
1909 Param ELEMENTOPTSETS = 0         range=[0,1]
1910 Param ELEMENTOPT = 1     range=[0,1]
1911 Param PROXYVARIABLE = 3          range=[1,5]
1912 Received score 174825345064.000000
1913 Mutating 1 settings
1914 &&&&&&&&Mutating&&&&&&&
1915 Param PREPROCESS = 1     range=[0,1]
1916 &&&&&&&&&&&&&&&&&&&&&&&
1917 **********************
1918 Polarity time: 0.003741
1919 Preprocess time: 0.012412
1920 Decompose Order: 0.000007
1921 Encoding Graph Time: 0.038641
1922 Elapse Encode time: 1.083641
1923 Is problem UNSAT after encoding: 0
1924 CNF Encode time: 0.000000
1925 SAT Solving time: 197.424468
1926 Result Computed in SAT solver:  SAT
1927 CSOLVER solve time: 198.508122
1928 Param PREPROCESS = 1     range=[0,1]
1929 Param ELEMENTOPTSETS = 0         range=[0,1]
1930 Param ELEMENTOPT = 1     range=[0,1]
1931 Param PROXYVARIABLE = 3          range=[1,5]
1932 Received score 198508121760.000000
1933 Mutating 1 settings
1934 &&&&&&&&Mutating&&&&&&&
1935 Param ELEMENTOPTSETS = 1         range=[0,1]
1936 &&&&&&&&&&&&&&&&&&&&&&&
1937 **********************
1938 Polarity time: 0.003766
1939 Preprocess time: 0.000014
1940 Decompose Order: 0.000004
1941 Encoding Graph Time: 0.077172
1942 Elapse Encode time: 0.162511
1943 Is problem UNSAT after encoding: 0
1944 CNF Encode time: 0.000000
1945 SAT Solving time: 165.982214
1946 Result Computed in SAT solver:  SAT
1947 CSOLVER solve time: 166.144737
1948 Param PREPROCESS = 0     range=[0,1]
1949 Param ELEMENTOPTSETS = 1         range=[0,1]
1950 Param ELEMENTOPT = 1     range=[0,1]
1951 Param PROXYVARIABLE = 3          range=[1,5]
1952 Received score 166144736612.000000
1953 Mutating 1 settings
1954 &&&&&&&&Mutating&&&&&&&
1955 Param PROXYVARIABLE = 4          range=[1,5]
1956 &&&&&&&&&&&&&&&&&&&&&&&
1957 **********************
1958 Polarity time: 0.003798
1959 Preprocess time: 0.000012
1960 Decompose Order: 0.000004
1961 Encoding Graph Time: 0.078314
1962 Elapse Encode time: 0.163238
1963 Is problem UNSAT after encoding: 0
1964 CNF Encode time: 0.000000
1965 SAT Solving time: 167.105501
1966 Result Computed in SAT solver:  SAT
1967 CSOLVER solve time: 167.268750
1968 Param PREPROCESS = 0     range=[0,1]
1969 Param ELEMENTOPTSETS = 1         range=[0,1]
1970 Param ELEMENTOPT = 1     range=[0,1]
1971 Param PROXYVARIABLE = 4          range=[1,5]
1972 Received score 167268749810.000000
1973 Mutating 1 settings
1974 &&&&&&&&Mutating&&&&&&&
1975 Param PREPROCESS = 1     range=[0,1]
1976 &&&&&&&&&&&&&&&&&&&&&&&
1977 **********************
1978 Polarity time: 0.003741
1979 Preprocess time: 0.012401
1980 Decompose Order: 0.000006
1981 Encoding Graph Time: 0.076291
1982 Elapse Encode time: 0.178145
1983 Is problem UNSAT after encoding: 0
1984 CNF Encode time: 0.000000
1985 SAT Solving time: 168.574659
1986 Result Computed in SAT solver:  SAT
1987 CSOLVER solve time: 168.752816
1988 Param PREPROCESS = 1     range=[0,1]
1989 Param ELEMENTOPTSETS = 1         range=[0,1]
1990 Param ELEMENTOPT = 1     range=[0,1]
1991 Param PROXYVARIABLE = 4          range=[1,5]
1992 Received score 168752815677.000000
1993 Mutating 1 settings
1994 &&&&&&&&Mutating&&&&&&&
1995 Param PREPROCESS = 0     range=[0,1]
1996 &&&&&&&&&&&&&&&&&&&&&&&
1997 **********************
1998 Polarity time: 0.003763
1999 Preprocess time: 0.000012
2000 Decompose Order: 0.000005
2001 Encoding Graph Time: 0.076082
2002 Elapse Encode time: 0.160938
2003 Is problem UNSAT after encoding: 0
2004 CNF Encode time: 0.000000
2005 SAT Solving time: 165.394703
2006 Result Computed in SAT solver:  SAT
2007 CSOLVER solve time: 165.555651
2008 Param PREPROCESS = 0     range=[0,1]
2009 Param ELEMENTOPTSETS = 1         range=[0,1]
2010 Param ELEMENTOPT = 1     range=[0,1]
2011 Param PROXYVARIABLE = 4          range=[1,5]
2012 Received score 165555651137.000000
2013 Best tuner:
2014 Param PREPROCESS = 0     range=[0,1]
2015 Param ELEMENTOPTSETS = 1         range=[0,1]
2016 Param ELEMENTOPT = 1     range=[0,1]
2017 Param PROXYVARIABLE = 5          range=[1,5]
2018 Received score 156357122315.000000