Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-vpm2.opb |
MD5SUM | 8c44064d4224b1d41c28f152218dd39f |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 98 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 168 |
Biggest coefficient in the objective function | 5 |
Number of bits for the biggest coefficient in the objective function | 3 |
Sum of the numbers in the objective function | 504 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 102400 |
Number of bits of the biggest number in a constraint | 17 |
Biggest sum of numbers in a constraint | 615983 |
Number of bits of the biggest sum of numbers | 20 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.05084 |
Number of variables | 2124 |
Total number of constraints | 612 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 168 |
Number of constraints which are nor clauses,nor cardinality constraints | 444 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 64 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc28 THE 2005-05-27 09:28:33 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23751 boxname=wulflinc28 idbench=1395 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 8c44064d4224b1d41c28f152218dd39f /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-vpm2.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-vpm2.opb IDLAUNCH: 23751 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 881636 kB Buffers: 14832 kB Cached: 117592 kB SwapCached: 788 kB Active: 17812 kB Inactive: 116876 kB HighTotal: 131008 kB HighFree: 10584 kB LowTotal: 903652 kB LowFree: 871052 kB SwapTotal: 2097640 kB SwapFree: 2096168 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5448 kB Slab: 12740 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 09:49:03 (client local time) WITH STATUS 152 IN 1229.88 SECONDS stats: 23751 7 1229.88 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 486 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################## c -- Clauses(.)/Splits(s): (none) c ---[ 485]---> BDD-cost: 7 c ---[ 484]---> BDD-cost: 7 c ---[ 483]---> BDD-cost: 7 c ---[ 482]---> BDD-cost: 7 c ---[ 481]---> BDD-cost: 7 c ---[ 480]---> BDD-cost: 7 c ---[ 479]---> BDD-cost: 7 c ---[ 478]---> BDD-cost: 7 c ---[ 477]---> BDD-cost: 7 c ---[ 474]---> BDD-cost: 7 c ---[ 473]---> BDD-cost: 7 c ---[ 472]---> BDD-cost: 7 c ---[ 471]---> BDD-cost: 7 c ---[ 468]---> BDD-cost: 7 c ---[ 467]---> BDD-cost: 7 c ---[ 466]---> BDD-cost: 7 c ---[ 465]---> BDD-cost: 7 c ---[ 462]---> BDD-cost: 7 c ---[ 459]---> BDD-cost: 7 c ---[ 458]---> BDD-cost: 7 c ---[ 457]---> BDD-cost: 7 c ---[ 454]---> BDD-cost: 7 c ---[ 453]---> BDD-cost: 7 c ---[ 452]---> BDD-cost: 7 c ---[ 451]---> BDD-cost: 7 c ---[ 450]---> BDD-cost: 7 c ---[ 448]---> BDD-cost: 7 c ---[ 447]---> BDD-cost: 7 c ---[ 446]---> BDD-cost: 7 c ---[ 445]---> BDD-cost: 7 c ---[ 444]---> BDD-cost: 7 c ---[ 441]---> BDD-cost: 7 c ---[ 440]---> BDD-cost: 7 c ---[ 439]---> BDD-cost: 7 c ---[ 433]---> BDD-cost: 7 c ---[ 427]---> BDD-cost: 7 c ---[ 422]---> BDD-cost: 7 c ---[ 421]---> BDD-cost: 7 c ---[ 415]---> BDD-cost: 7 c ---[ 409]---> BDD-cost: 7 c ---[ 408]---> BDD-cost: 7 c ---[ 402]---> BDD-cost: 7 c ---[ 397]---> BDD-cost: 7 c ---[ 396]---> BDD-cost: 7 c ---[ 391]---> BDD-cost: 7 c ---[ 390]---> BDD-cost: 7 c ---[ 386]---> BDD-cost: 7 c ---[ 385]---> BDD-cost: 7 c ---[ 384]---> BDD-cost: 7 c ---[ 380]---> BDD-cost: 7 c ---[ 379]---> BDD-cost: 7 c ---[ 378]---> BDD-cost: 7 c ---[ 374]---> BDD-cost: 7 c ---[ 373]---> BDD-cost: 7 c ---[ 372]---> BDD-cost: 7 c ---[ 368]---> BDD-cost: 7 c ---[ 367]---> BDD-cost: 7 c ---[ 366]---> BDD-cost: 7 c ---[ 365]---> BDD-cost: 7 c ---[ 364]---> BDD-cost: 7 c ---[ 359]---> BDD-cost: 7 c ---[ 353]---> BDD-cost: 7 c ---[ 347]---> BDD-cost: 7 c ---[ 339]---> BDD-cost: 7 c ---[ 333]---> BDD-cost: 7 c ---[ 327]---> BDD-cost: 7 c ---[ 321]---> BDD-cost: 7 c ---[ 317]---> BDD-cost: 14 c ---[ 316]---> BDD-cost: 14 c ---[ 315]---> BDD-cost: 14 c ---[ 314]---> BDD-cost: 14 c ---[ 313]---> BDD-cost: 14 c ---[ 312]---> BDD-cost: 14 c ---[ 310]---> BDD-cost: 14 c ---[ 309]---> BDD-cost: 14 c ---[ 308]---> BDD-cost: 14 c ---[ 307]---> BDD-cost: 14 c ---[ 306]---> BDD-cost: 14 c ---[ 302]---> BDD-cost: 13 c ---[ 301]---> BDD-cost: 13 c ---[ 300]---> BDD-cost: 13 c ---[ 295]---> BDD-cost: 13 c ---[ 294]---> BDD-cost: 13 c ---[ 290]---> BDD-cost: 15 c ---[ 289]---> BDD-cost: 15 c ---[ 288]---> BDD-cost: 15 c ---[ 287]---> BDD-cost: 13 c ---[ 286]---> BDD-cost: 13 c ---[ 285]---> BDD-cost: 13 c ---[ 284]---> BDD-cost: 13 c ---[ 283]---> BDD-cost: 13 c ---[ 282]---> BDD-cost: 13 c ---[ 280]---> BDD-cost: 13 c ---[ 279]---> BDD-cost: 13 c ---[ 278]---> BDD-cost: 13 c ---[ 277]---> BDD-cost: 13 c ---[ 276]---> BDD-cost: 13 c ---[ 274]---> BDD-cost:10530 c ---[ 272]---> BDD-cost: 3166 c ---[ 271]---> BDD-cost: 3 c ---[ 270]---> BDD-cost: 3 c ---[ 269]---> BDD-cost: 3 c ---[ 267]---> BDD-cost: 3 c ---[ 266]---> BDD-cost: 3 c ---[ 265]---> BDD-cost: 3 c ---[ 264]---> BDD-cost: 3 c ---[ 263]---> BDD-cost: 3 c ---[ 259]---> BDD-cost: 7 c ---[ 258]---> BDD-cost: 3 c ---[ 257]---> BDD-cost: 3 c ---[ 256]---> BDD-cost: 3 c ---[ 255]---> BDD-cost: 7 c ---[ 251]---> BDD-cost: 7 c ---[ 250]---> BDD-cost: 3 c ---[ 247]---> BDD-cost: 6 c ---[ 243]---> BDD-cost: 7 c ---[ 242]---> BDD-cost: 3 c ---[ 241]---> BDD-cost: 6 c ---[ 236]---> BDD-cost: 2842 c ---[ 235]---> BDD-cost: 3 c ---[ 234]---> BDD-cost: 3 c ---[ 233]---> BDD-cost: 6 c ---[ 229]---> BDD-cost: 7 c ---[ 228]---> BDD-cost: 3 c ---[ 227]---> BDD-cost: 6 c ---[ 224]---> BDD-cost: 7167 c ---[ 220]---> BDD-cost: 3 c ---[ 219]---> BDD-cost: 3 c ---[ 214]---> BDD-cost: 7 c ---[ 212]---> BDD-cost: 4105 c ---[ 211]---> BDD-cost: 3 c ---[ 206]---> BDD-cost: 3 c ---[ 205]---> BDD-cost: 3 c ---[ 198]---> BDD-cost: 3 c ---[ 197]---> BDD-cost: 3 c ---[ 193]---> BDD-cost: 3 c ---[ 192]---> BDD-cost: 3 c ---[ 191]---> BDD-cost: 3 c ---[ 185]---> BDD-cost: 3 c ---[ 184]---> BDD-cost: 3 c ---[ 183]---> BDD-cost: 3 c ---[ 179]---> BDD-cost: 3 c ---[ 178]---> BDD-cost: 3 c ---[ 175]---> BDD-cost: 3 c ---[ 171]---> BDD-cost: 3 c ---[ 170]---> BDD-cost: 3 c ---[ 169]---> BDD-cost: 3 c ---[ 168]---> BDD-cost: 3 c ---[ 167]---> BDD-cost: 3 c ---[ 166]---> BDD-cost: 6 c ---[ 164]---> BDD-cost: 3441 c ---[ 163]---> BDD-cost: 6 c ---[ 162]---> BDD-cost: 6 c ---[ 161]---> BDD-cost: 6 c ---[ 160]---> BDD-cost: 3 c ---[ 159]---> BDD-cost: 7 c ---[ 158]---> BDD-cost: 6 c ---[ 157]---> BDD-cost: 6 c ---[ 156]---> BDD-cost: 6 c ---[ 155]---> BDD-cost: 6 c ---[ 154]---> BDD-cost: 3 c ---[ 152]---> BDD-cost:10530 c ---[ 150]---> BDD-cost: 8215 c ---[ 149]---> BDD-cost: 7 c ---[ 148]---> BDD-cost: 5 c ---[ 147]---> BDD-cost: 5 c ---[ 146]---> BDD-cost: 5 c ---[ 145]---> BDD-cost: 5 c ---[ 144]---> BDD-cost: 3 c ---[ 143]---> BDD-cost: 7 c ---[ 142]---> BDD-cost: 5 c ---[ 141]---> BDD-cost: 5 c ---[ 140]---> BDD-cost: 5 c ---[ 137]---> BDD-cost: 5 c ---[ 135]---> BDD-cost: 7 c ---[ 134]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 6 c ---[ 132]---> BDD-cost: 6 c ---[ 131]---> BDD-cost: 6 c ---[ 129]---> BDD-cost: 7 c ---[ 128]---> BDD-cost: 3 c ---[ 125]---> BDD-cost: 6 c ---[ 124]---> BDD-cost: 6 c ---[ 123]---> BDD-cost: 6 c ---[ 121]---> BDD-cost: 7 c ---[ 120]---> BDD-cost: 3 c ---[ 119]---> BDD-cost: 6 c ---[ 118]---> BDD-cost: 6 c ---[ 117]---> BDD-cost: 6 c ---[ 114]---> BDD-cost: 3369 c ---[ 113]---> BDD-cost: 7 c ---[ 112]---> BDD-cost: 3 c ---[ 111]---> BDD-cost: 5 c ---[ 110]---> BDD-cost: 5 c ---[ 109]---> BDD-cost: 5 c ---[ 107]---> BDD-cost: 4733 c ---[ 105]---> BDD-cost: 4964 c ---[ 103]---> BDD-cost: 7397 c ---[ 101]---> BDD-cost: 3944 c ---[ 99]---> BDD-cost: 3944 c ---[ 97]---> BDD-cost: 3944 c ---[ 95]---> BDD-cost: 7522 c ---[ 93]---> BDD-cost: 3944 c ---[ 91]---> BDD-cost: 3997 c ---[ 89]---> BDD-cost: 9563 c ---[ 87]---> BDD-cost: 4987 c ---[ 85]---> BDD-cost: 4987 c ---[ 83]---> BDD-cost: 4987 c ---[ 81]---> BDD-cost: 5216 c ---[ 73]---> BDD-cost: 7522 c ---[ 69]---> BDD-cost: 3154 c ---[ 66]---> BDD-cost: 136 c ---[ 65]---> BDD-cost: 283 c ---[ 64]---> BDD-cost: 282 c ---[ 63]---> BDD-cost: 470 c ---[ 62]---> BDD-cost: 579 c ---[ 61]---> BDD-cost: 572 c ---[ 60]---> BDD-cost: 182 c ---[ 58]---> BDD-cost:10993 c ---[ 57]---> BDD-cost: 387 c ---[ 56]---> BDD-cost: 386 c ---[ 55]---> BDD-cost: 647 c ---[ 54]---> BDD-cost: 805 c ---[ 53]---> BDD-cost: 804 c ---[ 52]---> BDD-cost: 200 c ---[ 51]---> BDD-cost: 446 c ---[ 50]---> BDD-cost: 440 c ---[ 49]---> BDD-cost: 784 c ---[ 48]---> BDD-cost: 985 c ---[ 46]---> BDD-cost: 2194 c ---[ 45]---> BDD-cost: 982 c ---[ 44]---> BDD-cost: 87 c ---[ 43]---> BDD-cost: 178 c ---[ 42]---> BDD-cost: 174 c ---[ 41]---> BDD-cost: 291 c ---[ 40]---> BDD-cost: 374 c ---[ 39]---> BDD-cost: 369 c ---[ 38]---> BDD-cost: 3 c ---[ 37]---> BDD-cost: 3 c ---[ 36]---> BDD-cost: 3 c ---[ 34]---> BDD-cost: 4013 c ---[ 33]---> BDD-cost: 3 c ---[ 32]---> BDD-cost: 3 c ---[ 31]---> BDD-cost: 3 c ---[ 30]---> BDD-cost: 3 c ---[ 29]---> BDD-cost: 3 c ---[ 28]---> BDD-cost: 3 c ---[ 27]---> BDD-cost: 7 c ---[ 26]---> BDD-cost: 7 c ---[ 25]---> BDD-cost: 3 c ---[ 24]---> BDD-cost: 3 c ---[ 22]---> BDD-cost: 4263 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 3 c ---[ 19]---> BDD-cost: 7 c ---[ 18]---> BDD-cost: 7 c ---[ 17]---> BDD-cost: 3 c ---[ 16]---> BDD-cost: 3 c ---[ 15]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 3 c ---[ 13]---> BDD-cost: 7 c ---[ 12]---> BDD-cost: 7 c ---[ 10]---> BDD-cost: 4263 c ---[ 9]---> BDD-cost: 3 c ---[ 7]---> BDD-cost: 7 c ---[ 6]---> BDD-cost: 3 c ---[ 5]---> BDD-cost: 3 c ---[ 4]---> BDD-cost: 3 c ---[ 3]---> BDD-cost: 7 c ---[ 1]---> BDD-cost: 3 c ---[ 0]---> BDD-cost: 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 457558 1265621 | 152519 0 0 nan | 0.000 % | c | 101 | 457558 1265621 | 167770 101 1035 10.2 | 0.549 % | c | 251 | 457452 1265319 | 184547 235 4169 17.7 | 0.565 % | c | 478 | 457376 1265101 | 203002 455 9845 21.6 | 0.575 % | c | 816 | 457350 1265024 | 223303 791 16444 20.8 | 0.579 % | c | 1322 | 457266 1264793 | 245633 1291 30889 23.9 | 0.590 % | c | 2081 | 457266 1264793 | 270196 2050 58303 28.4 | 0.590 % | c | 3220 | 457199 1264612 | 297216 3182 98499 31.0 | 0.601 % | c | 4928 | 457156 1264487 | 326938 4881 149564 30.6 | 0.610 % | c | 7491 | 457124 1264394 | 359631 7439 229291 30.8 | 0.616 % | c | 11335 | 457018 1264094 | 395595 11270 418115 37.1 | 0.637 % | c | 17101 | 457018 1264094 | 435154 17036 647974 38.0 | 0.637 % | c | 25750 | 456973 1263964 | 478669 25680 908094 35.4 | 0.647 % | c | 38724 | 456889 1263725 | 526536 38645 1637252 42.4 | 0.660 % | c ============================================================================== c [1mFound solution: 143[0m c ---[ 0]---> Sorter-cost: 6414 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39880 | 470257 1294935 | 156752 39800 1680425 42.2 | 0.660 % | c | 39980 | 470215 1294814 | 172427 39895 1684276 42.2 | 0.650 % | c | 40130 | 470161 1294686 | 189669 40041 1687653 42.1 | 0.655 % | c | 40356 | 470161 1294686 | 208636 40267 1697260 42.2 | 0.655 % | c | 40693 | 470151 1294658 | 229500 40603 1709934 42.1 | 0.656 % | c | 41199 | 470105 1294549 | 252450 41107 1727320 42.0 | 0.661 % | c | 41958 | 470105 1294549 | 277695 41866 1752549 41.9 | 0.661 % | c | 43099 | 470089 1294503 | 305465 43003 1785863 41.5 | 0.665 % | c | 44809 | 470089 1294503 | 336011 44713 1826588 40.9 | 0.665 % | c | 47371 | 470077 1294469 | 369613 47274 1913086 40.5 | 0.667 % | c | 51215 | 470054 1294416 | 406574 51117 2018145 39.5 | 0.669 % | c | 56981 | 470054 1294416 | 447231 56883 2185308 38.4 | 0.669 % | c | 65630 | 470054 1294416 | 491954 65532 2525905 38.5 | 0.669 % | c ============================================================================== c [1mFound solution: 115[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 75481 | 470093 1294505 | 156697 75381 3328804 44.2 | 0.669 % | c | 75582 | 470082 1294473 | 172366 75481 3337237 44.2 | 0.674 % | c | 75733 | 470082 1294473 | 189603 75632 3339021 44.1 | 0.674 % | c | 75959 | 470082 1294473 | 208563 75858 3340765 44.0 | 0.674 % | c | 76297 | 470082 1294473 | 229420 76196 3351703 44.0 | 0.674 % | c | 76803 | 470082 1294473 | 252362 76702 3369335 43.9 | 0.674 % | c | 77563 | 470082 1294473 | 277598 77462 3460024 44.7 | 0.674 % | c | 78703 | 469990 1294272 | 305358 78598 3477722 44.2 | 0.691 % | c | 80411 | 469793 1293808 | 335893 80221 3539878 44.1 | 0.722 % | c | 82975 | 469793 1293808 | 369483 82785 3683832 44.5 | 0.722 % | c | 86819 | 469793 1293808 | 406431 86629 3884323 44.8 | 0.722 % | c | 92586 | 469654 1293495 | 447074 91727 4139810 45.1 | 0.748 % | c | 101236 | 469647 1293475 | 491782 100376 4505463 44.9 | 0.749 % | c ============================================================================== c [1mFound solution: 113[0m c ---[ 0]---> Sorter-cost: 4837 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 103199 | 475285 1306698 | 158428 102339 4608803 45.0 | 0.749 % | c | 103299 | 475285 1306698 | 174270 102439 4611411 45.0 | 0.735 % | c | 103452 | 475285 1306698 | 191697 102592 4615017 45.0 | 0.735 % | c | 103677 | 475285 1306698 | 210867 102817 4623894 45.0 | 0.735 % | c | 104014 | 475285 1306698 | 231954 103154 4637200 45.0 | 0.735 % | c | 104522 | 475285 1306698 | 255149 103662 4660564 45.0 | 0.735 % | c | 105281 | 475285 1306698 | 280664 104421 4691283 44.9 | 0.735 % | c | 106420 | 475285 1306698 | 308731 105560 4725387 44.8 | 0.735 % | c | 108130 | 475285 1306698 | 339604 107270 4777409 44.5 | 0.735 % | c | 110698 | 475285 1306698 | 373564 109838 4908084 44.7 | 0.735 % | c ============================================================================== c [1mFound solution: 108[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 110998 | 480058 1317841 | 160019 110138 4919258 44.7 | 0.735 % | c | 111098 | 480058 1317841 | 176020 110238 4926262 44.7 | 0.736 % | c | 111249 | 480058 1317841 | 193622 110389 4929850 44.7 | 0.736 % | c | 111478 | 480058 1317841 | 212985 110618 4936111 44.6 | 0.736 % | c | 111815 | 480058 1317841 | 234283 110955 4949127 44.6 | 0.736 % | c | 112322 | 480058 1317841 | 257712 111462 4973648 44.6 | 0.736 % | c | 113081 | 480058 1317841 | 283483 112221 5002783 44.6 | 0.736 % | c | 114222 | 480058 1317841 | 311831 113362 5067501 44.7 | 0.736 % | c ============================================================================== c [1mFound solution: 106[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 114844 | 480065 1317941 | 160021 113984 5099651 44.7 | 0.736 % | c | 114946 | 480065 1317941 | 176023 114086 5101268 44.7 | 0.736 % | c | 115096 | 480065 1317941 | 193625 114236 5102171 44.7 | 0.736 % | c | 115321 | 480065 1317941 | 212987 114461 5106340 44.6 | 0.736 % | c | 115659 | 480065 1317941 | 234286 114799 5113368 44.5 | 0.736 % | c | 116165 | 480052 1317913 | 257715 115301 5118882 44.4 | 0.739 % | c | 116926 | 480052 1317913 | 283486 116062 5143563 44.3 | 0.739 % | c | 118065 | 480052 1317913 | 311835 117201 5181715 44.2 | 0.739 % | c | 119774 | 480052 1317913 | 343019 118910 5243306 44.1 | 0.739 % | c | 122336 | 480052 1317913 | 377321 121472 5356913 44.1 | 0.739 % | c | 126181 | 480023 1317831 | 415053 125316 5489286 43.8 | 0.741 % | c | 131948 | 480023 1317831 | 456558 131083 5739671 43.8 | 0.741 % | c ============================================================================== c [1mFound solution: 105[0m c ---[ 0]---> Sorter-cost: 1 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 133769 | 480027 1317843 | 160009 132904 5920861 44.5 | 0.741 % | c | 133870 | 480027 1317843 | 176009 133005 5921948 44.5 | 0.741 % | c | 134020 | 480027 1317843 | 193610 133155 5923660 44.5 | 0.741 % | c | 134246 | 480027 1317843 | 212971 133381 5925334 44.4 | 0.741 % | c | 134584 | 479959 1317701 | 234269 133696 5933761 44.4 | 0.758 % | c | 135091 | 479959 1317701 | 257696 134203 5951920 44.4 | 0.758 % | c | 135854 | 479959 1317701 | 283465 134966 5986093 44.4 | 0.758 % | c | 136996 | 479959 1317701 | 311812 136108 6040429 44.4 | 0.758 % | c | 138704 | 479950 1317683 | 342993 137815 6122223 44.4 | 0.760 % | c | 141267 | 479950 1317683 | 377292 140378 6261082 44.6 | 0.760 % | c ============================================================================== c [1mFound solution: 104[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 142561 | 479914 1317612 | 159971 141660 6351995 44.8 | 0.760 % | c | 142662 | 479914 1317612 | 175968 141761 6353303 44.8 | 0.771 % | c | 142812 | 479914 1317612 | 193564 141911 6357679 44.8 | 0.771 % | c | 143037 | 479914 1317612 | 212921 142136 6363544 44.8 | 0.771 % | c | 143374 | 479914 1317612 | 234213 142473 6375783 44.8 | 0.771 % | c | 143882 | 479914 1317612 | 257634 142981 6399199 44.8 | 0.771 % | c | 144644 | 479914 1317612 | 283398 143743 6434810 44.8 | 0.771 % | c ============================================================================== c [1mFound solution: 92[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 145331 | 479945 1317687 | 159981 144430 6464774 44.8 | 0.771 % | c | 145431 | 479945 1317687 | 175979 144530 6467264 44.7 | 0.772 % | c | 145581 | 479945 1317687 | 193577 144680 6469971 44.7 | 0.772 % | c | 145806 | 479945 1317687 | 212934 144905 6482685 44.7 | 0.772 % | c | 146143 | 479945 1317687 | 234228 145242 6498336 44.7 | 0.772 % | c | 146649 | 479945 1317687 | 257651 145748 6522811 44.8 | 0.772 % | c | 147408 | 479945 1317687 | 283416 146507 6559756 44.8 | 0.772 % | c | 148549 | 479945 1317687 | 311757 147648 6640764 45.0 | 0.772 % | c | 150258 | 479945 1317687 | 342933 149357 6777073 45.4 | 0.772 % | c | 152820 | 479945 1317687 | 377226 151919 6886476 45.3 | 0.772 % | c | 156666 | 479945 1317687 | 414949 155765 7355928 47.2 | 0.772 % | c ============================================================================== c [1mFound solution: 91[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 158382 | 479952 1317706 | 159984 157481 7422946 47.1 | 0.772 % | c | 158484 | 479952 1317706 | 175982 157583 7425964 47.1 | 0.772 % | c | 158635 | 479952 1317706 | 193580 157734 7430276 47.1 | 0.772 % | c | 158860 | 479952 1317706 | 212938 157959 7441004 47.1 | 0.772 % | c | 159198 | 479952 1317706 | 234232 158297 7452593 47.1 | 0.772 % | c | 159705 | 479952 1317706 | 257655 158804 7465972 47.0 | 0.772 % | c | 160465 | 479952 1317706 | 283421 159564 7506171 47.0 | 0.772 % | c | 161612 | 479944 1317684 | 311763 160710 7608850 47.3 | 0.773 % | c | 163320 | 479944 1317684 | 342939 162418 7652982 47.1 | 0.773 % | c | 165882 | 479944 1317684 | 377233 164980 7770131 47.1 | 0.773 % | c ============================================================================== c [1mFound solution: 90[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 168881 | 479949 1317695 | 159983 167979 8004153 47.6 | 0.773 % | c | 168981 | 479949 1317695 | 175981 21530 828029 38.5 | 0.774 % | c | 169131 | 479949 1317695 | 193579 21680 829301 38.3 | 0.774 % | c | 169356 | 479949 1317695 | 212937 21905 831721 38.0 | 0.774 % | c | 169695 | 479949 1317695 | 234231 22244 837360 37.6 | 0.774 % | c | 170201 | 479849 1317477 | 257654 22746 861336 37.9 | 0.792 % | c | 170960 | 479849 1317477 | 283419 23505 909830 38.7 | 0.792 % | c | 172099 | 479849 1317477 | 311761 24644 983990 39.9 | 0.792 % | c | 173808 | 479849 1317477 | 342937 26353 1075388 40.8 | 0.792 % | c | 176372 | 479849 1317477 | 377231 28917 1158372 40.1 | 0.792 % | c | 180216 | 479849 1317477 | 414954 32761 1550642 47.3 | 0.792 % | c | 185983 | 479839 1317457 | 456450 38527 1919264 49.8 | 0.794 % | c ============================================================================== c [1mFound solution: 88[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 189621 | 479845 1317473 | 159948 42165 2160633 51.2 | 0.794 % | c | 189723 | 479845 1317473 | 175942 42267 2161896 51.1 | 0.794 % | c | 189874 | 479845 1317473 | 193537 42418 2164254 51.0 | 0.794 % | c | 190100 | 479845 1317473 | 212890 42644 2168463 50.9 | 0.794 % | c | 190437 | 479845 1317473 | 234179 42981 2182103 50.8 | 0.794 % | c | 190944 | 479845 1317473 | 257597 43488 2196148 50.5 | 0.794 % | c | 191703 | 479845 1317473 | 283357 44247 2210889 50.0 | 0.794 % | c | 192843 | 479845 1317473 | 311693 45387 2283583 50.3 | 0.794 % | c | 194551 | 479845 1317473 | 342862 47095 2351141 49.9 | 0.794 % | c | 197113 | 479845 1317473 | 377149 49657 2541259 51.2 | 0.794 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 19110 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.93 0.98 0.91 2/54 19106 Raw data (stat): 19106 (runsolver) R 19105 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855089805 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.94 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0007 s] Raw data (loadavg): 0.95 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0013 s] Raw data (loadavg): 0.95 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.002 s] Raw data (loadavg): 0.96 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0027 s] Raw data (loadavg): 0.97 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0023 s] Raw data (loadavg): 0.97 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.002 s] Raw data (loadavg): 0.97 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0027 s] Raw data (loadavg): 0.98 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0023 s] Raw data (loadavg): 0.98 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.98 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.11 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.111 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.111 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.11 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.111 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.111 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.111 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.112 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.112 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.112 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.113 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.114 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.114 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.114 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.115 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.114 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.115 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.116 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.115 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.116 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.116 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.116 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.116 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.116 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.117 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.116 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.117 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.117 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.116 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.117 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.117 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.117 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.118 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.118 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.118 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.119 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.12 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.119 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.119 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.12 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.119 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.12 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.121 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.12 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.121 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.122 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.123 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.123 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.123 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.124 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.123 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.124 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.125 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.125 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.125 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.126 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.126 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.126 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.126 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.127 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.127 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.128 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.129 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.128 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.129 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.13 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.13 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.13 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.13 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.13 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.13 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.139 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.139 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.139 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.139 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.139 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.14 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.15 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.15 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.15 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.15 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.71 s] Raw data (loadavg): 0.99 0.98 0.91 1/53 19110 Raw data (stat): 19106 (minisat+_script) S 19105 24821 24820 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855089805 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.71 CPU time (s): 1229.88 CPU user time (s): 1229.1 CPU system time (s): 0.777881 CPU usage (%): 100.014 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####