Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm2.opb |
MD5SUM | fae1fae180d772ad3ee6c1acfa1c8b4f |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 122 |
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 | 2000000 |
Number of bits of the biggest number in a constraint | 21 |
Biggest sum of numbers in a constraint | 30041153 |
Number of bits of the biggest sum of numbers | 25 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.01 |
Number of variables | 2124 |
Total number of constraints | 444 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 444 |
Minimum length of a constraint | 8 |
Maximum length of a constraint | 64 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc11 THE 2005-04-21 02:12:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18953 boxname=wulflinc11 idbench=1458 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fae1fae180d772ad3ee6c1acfa1c8b4f /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-vpm2.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-vpm2.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-vpm2.opb IDLAUNCH: 18953 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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 : 2 cpu MHz : 451.028 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: 881184 kB Buffers: 19464 kB Cached: 113340 kB SwapCached: 0 kB Active: 63968 kB Inactive: 71668 kB HighTotal: 131008 kB HighFree: 17108 kB LowTotal: 903652 kB LowFree: 864076 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6816 kB Slab: 12308 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 02:32:06 (client local time) WITH STATUS 0 IN 1200.25 SECONDS stats: 18953 7 1200.25 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 486 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp 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: 5216 c ---[ 264]---> BDD-cost: 3154 c ---[ 260]---> BDD-cost:10530 c ---[ 258]---> BDD-cost:10530 c ---[ 256]---> BDD-cost: 7522 c ---[ 254]---> BDD-cost: 7522 c ---[ 252]---> BDD-cost:10993 c ---[ 250]---> BDD-cost: 2194 c ---[ 248]---> BDD-cost: 4013 c ---[ 246]---> BDD-cost: 4263 c ---[ 244]---> BDD-cost: 4263 c ---[ 242]---> BDD-cost: 3166 c ---[ 236]---> BDD-cost: 2842 c ---[ 234]---> BDD-cost: 7167 c ---[ 232]---> BDD-cost: 4105 c ---[ 224]---> BDD-cost: 3441 c ---[ 222]---> BDD-cost: 8215 c ---[ 216]---> BDD-cost: 3369 c ---[ 214]---> BDD-cost: 4733 c ---[ 212]---> BDD-cost: 4964 c ---[ 210]---> BDD-cost: 7397 c ---[ 208]---> BDD-cost: 3944 c ---[ 206]---> BDD-cost: 3944 c ---[ 204]---> BDD-cost: 3944 c ---[ 202]---> BDD-cost: 3944 c ---[ 200]---> BDD-cost: 3997 c ---[ 198]---> BDD-cost: 9563 c ---[ 196]---> BDD-cost: 4987 c ---[ 194]---> BDD-cost: 4987 c ---[ 192]---> BDD-cost: 4987 c ---[ 191]---> BDD-cost: 110 c ---[ 190]---> BDD-cost: 237 c ---[ 189]---> BDD-cost: 236 c ---[ 188]---> BDD-cost: 393 c ---[ 187]---> BDD-cost: 495 c ---[ 186]---> BDD-cost: 488 c ---[ 185]---> BDD-cost: 131 c ---[ 184]---> BDD-cost: 262 c ---[ 183]---> BDD-cost: 261 c ---[ 182]---> BDD-cost: 448 c ---[ 181]---> BDD-cost: 550 c ---[ 180]---> BDD-cost: 549 c ---[ 179]---> BDD-cost: 200 c ---[ 178]---> BDD-cost: 446 c ---[ 177]---> BDD-cost: 440 c ---[ 176]---> BDD-cost: 784 c ---[ 175]---> BDD-cost: 985 c ---[ 174]---> BDD-cost: 982 c ---[ 173]---> BDD-cost: 87 c ---[ 172]---> BDD-cost: 178 c ---[ 171]---> BDD-cost: 174 c ---[ 170]---> BDD-cost: 291 c ---[ 169]---> BDD-cost: 374 c ---[ 168]---> BDD-cost: 369 c ---[ 167]---> BDD-cost: 3 c ---[ 166]---> BDD-cost: 3 c ---[ 165]---> BDD-cost: 3 c ---[ 164]---> BDD-cost: 3 c ---[ 163]---> BDD-cost: 3 c ---[ 162]---> BDD-cost: 3 c ---[ 161]---> BDD-cost: 3 c ---[ 160]---> BDD-cost: 3 c ---[ 159]---> BDD-cost: 3 c ---[ 158]---> BDD-cost: 7 c ---[ 157]---> BDD-cost: 7 c ---[ 156]---> BDD-cost: 3 c ---[ 155]---> BDD-cost: 3 c ---[ 154]---> BDD-cost: 3 c ---[ 153]---> BDD-cost: 3 c ---[ 152]---> BDD-cost: 7 c ---[ 151]---> BDD-cost: 7 c ---[ 150]---> BDD-cost: 3 c ---[ 149]---> BDD-cost: 3 c ---[ 148]---> BDD-cost: 3 c ---[ 147]---> BDD-cost: 3 c ---[ 146]---> BDD-cost: 7 c ---[ 145]---> BDD-cost: 7 c ---[ 144]---> BDD-cost: 3 c ---[ 142]---> BDD-cost: 7 c ---[ 141]---> BDD-cost: 3 c ---[ 140]---> BDD-cost: 3 c ---[ 139]---> BDD-cost: 3 c ---[ 138]---> BDD-cost: 7 c ---[ 136]---> BDD-cost: 3 c ---[ 135]---> BDD-cost: 3 c ---[ 134]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 3 c ---[ 132]---> BDD-cost: 3 c ---[ 130]---> BDD-cost: 3 c ---[ 129]---> BDD-cost: 3 c ---[ 128]---> BDD-cost: 3 c ---[ 127]---> BDD-cost: 3 c ---[ 126]---> BDD-cost: 3 c ---[ 124]---> BDD-cost: 7 c ---[ 123]---> BDD-cost: 3 c ---[ 122]---> BDD-cost: 3 c ---[ 121]---> BDD-cost: 3 c ---[ 120]---> BDD-cost: 7 c ---[ 116]---> BDD-cost: 7 c ---[ 115]---> BDD-cost: 3 c ---[ 114]---> BDD-cost: 6 c ---[ 110]---> BDD-cost: 7 c ---[ 109]---> BDD-cost: 3 c ---[ 108]---> BDD-cost: 6 c ---[ 104]---> BDD-cost: 3 c ---[ 103]---> BDD-cost: 3 c ---[ 102]---> BDD-cost: 6 c ---[ 98]---> BDD-cost: 7 c ---[ 97]---> BDD-cost: 3 c ---[ 96]---> BDD-cost: 6 c ---[ 91]---> BDD-cost: 3 c ---[ 90]---> BDD-cost: 3 c ---[ 85]---> BDD-cost: 7 c ---[ 84]---> BDD-cost: 3 c ---[ 79]---> BDD-cost: 3 c ---[ 78]---> BDD-cost: 3 c ---[ 73]---> BDD-cost: 3 c ---[ 72]---> BDD-cost: 3 c ---[ 68]---> BDD-cost: 3 c ---[ 67]---> BDD-cost: 3 c ---[ 66]---> BDD-cost: 3 c ---[ 62]---> BDD-cost: 3 c ---[ 61]---> BDD-cost: 3 c ---[ 60]---> BDD-cost: 3 c ---[ 56]---> BDD-cost: 3 c ---[ 55]---> BDD-cost: 3 c ---[ 54]---> BDD-cost: 3 c ---[ 50]---> BDD-cost: 3 c ---[ 49]---> BDD-cost: 3 c ---[ 48]---> BDD-cost: 3 c ---[ 47]---> BDD-cost: 3 c ---[ 46]---> BDD-cost: 3 c ---[ 45]---> BDD-cost: 6 c ---[ 44]---> BDD-cost: 6 c ---[ 43]---> BDD-cost: 6 c ---[ 42]---> BDD-cost: 6 c ---[ 41]---> BDD-cost: 3 c ---[ 40]---> BDD-cost: 7 c ---[ 39]---> BDD-cost: 6 c ---[ 38]---> BDD-cost: 6 c ---[ 37]---> BDD-cost: 6 c ---[ 36]---> BDD-cost: 6 c ---[ 35]---> BDD-cost: 3 c ---[ 34]---> BDD-cost: 7 c ---[ 33]---> BDD-cost: 5 c ---[ 32]---> BDD-cost: 5 c ---[ 31]---> BDD-cost: 5 c ---[ 30]---> BDD-cost: 5 c ---[ 29]---> BDD-cost: 3 c ---[ 28]---> BDD-cost: 7 c ---[ 27]---> BDD-cost: 5 c ---[ 26]---> BDD-cost: 5 c ---[ 25]---> BDD-cost: 5 c ---[ 24]---> BDD-cost: 5 c ---[ 22]---> BDD-cost: 7 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 6 c ---[ 19]---> BDD-cost: 6 c ---[ 18]---> BDD-cost: 6 c ---[ 16]---> BDD-cost: 7 c ---[ 15]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 6 c ---[ 13]---> BDD-cost: 6 c ---[ 12]---> BDD-cost: 6 c ---[ 10]---> BDD-cost: 7 c ---[ 9]---> BDD-cost: 3 c ---[ 8]---> BDD-cost: 6 c ---[ 7]---> BDD-cost: 6 c ---[ 6]---> BDD-cost: 6 c ---[ 4]---> BDD-cost: 7 c ---[ 3]---> BDD-cost: 3 c ---[ 2]---> BDD-cost: 5 c ---[ 1]---> BDD-cost: 5 c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 454043 1255430 | 151347 0 0 nan | 0.000 % | c | 100 | 453973 1255238 | 166481 93 1660 17.8 | 0.565 % | c | 250 | 453950 1255172 | 183129 241 4695 19.5 | 0.569 % | c | 475 | 453902 1255034 | 201442 461 8683 18.8 | 0.578 % | c | 812 | 453747 1254604 | 221587 784 14296 18.2 | 0.600 % | c | 1320 | 453734 1254566 | 243745 1290 40773 31.6 | 0.603 % | c | 2079 | 453659 1254362 | 268120 2042 72297 35.4 | 0.612 % | c | 3219 | 453617 1254241 | 294932 3179 110292 34.7 | 0.617 % | c | 4927 | 453566 1254108 | 324425 4884 158566 32.5 | 0.623 % | c | 7491 | 453409 1253709 | 356868 7433 225238 30.3 | 0.655 % | c | 11338 | 453377 1253617 | 392555 11275 450448 40.0 | 0.662 % | c | 17105 | 453353 1253549 | 431810 17039 767695 45.1 | 0.666 % | c | 25754 | 453306 1253428 | 474991 25686 1096740 42.7 | 0.669 % | c | 38728 | 453295 1253396 | 522490 38659 1522744 39.4 | 0.671 % | c | 58189 | 453255 1253283 | 574739 58114 2334938 40.2 | 0.679 % | c | 87381 | 453249 1253265 | 632213 87304 3998074 45.8 | 0.681 % | c | 131170 | 453236 1253227 | 695435 131092 5961914 45.5 | 0.684 % | c | 196855 | 453186 1253082 | 764978 196772 10804657 54.9 | 0.694 % | #### 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.77 0.92 0.97 2/54 26218 Raw data (stat): 26218 (runsolver) R 26217 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483158402 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99976 s] Raw data (loadavg): 0.81 0.92 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 14997 0 0 0 963 35 0 0 25 0 1 0 483158402 67891200 14195 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16575 14195 603 41 0 16534 0 vsize: 66300 [startup+19.9996 s] Raw data (loadavg): 0.84 0.93 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15185 0 0 0 1963 36 0 0 25 0 1 0 483158402 68718592 14383 4294967295 134512640 134672761 3221224544 3221223616 1074719016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16777 14383 603 41 0 16736 0 vsize: 67108 [startup+30.0009 s] Raw data (loadavg): 0.86 0.93 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15315 0 0 0 2962 37 0 0 25 0 1 0 483158402 69246976 14513 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16906 14513 603 41 0 16865 0 vsize: 67624 [startup+40.0012 s] Raw data (loadavg): 0.88 0.93 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15428 0 0 0 3961 38 0 0 25 0 1 0 483158402 69672960 14626 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17010 14626 603 41 0 16969 0 vsize: 68040 [startup+50.0019 s] Raw data (loadavg): 0.90 0.93 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15592 0 0 0 4960 39 0 0 25 0 1 0 483158402 70459392 14790 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17202 14790 603 41 0 17161 0 vsize: 68808 [startup+60.0022 s] Raw data (loadavg): 0.91 0.93 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15765 0 0 0 5959 40 0 0 25 0 1 0 483158402 71131136 14963 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17366 14963 603 41 0 17325 0 vsize: 69464 [startup+70.0026 s] Raw data (loadavg): 0.93 0.94 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 15914 0 0 0 6958 41 0 0 25 0 1 0 483158402 71667712 15112 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17497 15112 603 41 0 17456 0 vsize: 69988 [startup+80.0038 s] Raw data (loadavg): 0.94 0.94 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16097 0 0 0 7957 42 0 0 25 0 1 0 483158402 72511488 15295 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17703 15295 603 41 0 17662 0 vsize: 70812 [startup+90.0046 s] Raw data (loadavg): 0.95 0.94 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16341 0 0 0 8957 42 0 0 25 0 1 0 483158402 73445376 15539 4294967295 134512640 134672761 3221224544 3221223712 134560811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17931 15539 603 41 0 17890 0 vsize: 71724 [startup+100.005 s] Raw data (loadavg): 0.95 0.94 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16513 0 0 0 9956 43 0 0 25 0 1 0 483158402 74113024 15711 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18094 15711 603 41 0 18053 0 vsize: 72376 [startup+110.006 s] Raw data (loadavg): 0.96 0.94 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16657 0 0 0 10956 44 0 0 25 0 1 0 483158402 74772480 15855 4294967295 134512640 134672761 3221224544 3221223728 134558918 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18255 15855 603 41 0 18214 0 vsize: 73020 [startup+120.006 s] Raw data (loadavg): 0.97 0.94 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16768 0 0 0 11956 44 0 0 25 0 1 0 483158402 75300864 15966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18384 15966 603 41 0 18343 0 vsize: 73536 [startup+130.006 s] Raw data (loadavg): 0.97 0.94 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16854 0 0 0 12955 45 0 0 25 0 1 0 483158402 75694080 16052 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18480 16052 603 41 0 18439 0 vsize: 73920 [startup+140.007 s] Raw data (loadavg): 0.98 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 16930 0 0 0 13955 45 0 0 25 0 1 0 483158402 75964416 16128 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18546 16128 603 41 0 18505 0 vsize: 74184 [startup+150.008 s] Raw data (loadavg): 0.98 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 17079 0 0 0 14955 46 0 0 25 0 1 0 483158402 76640256 16277 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18711 16277 603 41 0 18670 0 vsize: 74844 [startup+160.009 s] Raw data (loadavg): 0.98 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 17359 0 0 0 15954 46 0 0 25 0 1 0 483158402 77737984 16557 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18979 16557 603 41 0 18938 0 vsize: 75916 [startup+170.008 s] Raw data (loadavg): 0.98 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 17643 0 0 0 16953 48 0 0 25 0 1 0 483158402 78823424 16841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19244 16841 603 41 0 19203 0 vsize: 76976 [startup+180.009 s] Raw data (loadavg): 0.99 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 17800 0 0 0 17952 49 0 0 25 0 1 0 483158402 79503360 16998 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19410 16998 603 41 0 19369 0 vsize: 77640 [startup+190.009 s] Raw data (loadavg): 0.99 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18019 0 0 0 18952 49 0 0 25 0 1 0 483158402 80437248 17217 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19638 17217 603 41 0 19597 0 vsize: 78552 [startup+200.01 s] Raw data (loadavg): 0.99 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18143 0 0 0 19951 50 0 0 25 0 1 0 483158402 80969728 17341 4294967295 134512640 134672761 3221224544 3221223728 134558360 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19768 17341 603 41 0 19727 0 vsize: 79072 [startup+210.011 s] Raw data (loadavg): 0.99 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18321 0 0 0 20951 51 0 0 25 0 1 0 483158402 81633280 17519 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19930 17519 603 41 0 19889 0 vsize: 79720 [startup+220.011 s] Raw data (loadavg): 0.99 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18547 0 0 0 21949 53 0 0 25 0 1 0 483158402 82833408 17745 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20223 17745 603 41 0 20182 0 vsize: 80892 [startup+230.011 s] Raw data (loadavg): 0.99 0.95 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 18785 0 0 0 22948 54 0 0 25 0 1 0 483158402 83763200 17983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20450 17983 603 41 0 20409 0 vsize: 81800 [startup+240.011 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19015 0 0 0 23946 56 0 0 25 0 1 0 483158402 84701184 18213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20679 18213 603 41 0 20638 0 vsize: 82716 [startup+250.012 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19246 0 0 0 24946 57 0 0 25 0 1 0 483158402 85659648 18444 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20913 18444 603 41 0 20872 0 vsize: 83652 [startup+260.013 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19468 0 0 0 25944 58 0 0 25 0 1 0 483158402 86556672 18666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21132 18666 603 41 0 21091 0 vsize: 84528 [startup+270.012 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19687 0 0 0 26944 59 0 0 25 0 1 0 483158402 87482368 18885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21358 18885 603 41 0 21317 0 vsize: 85432 [startup+280.012 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 19880 0 0 0 27943 59 0 0 25 0 1 0 483158402 88281088 19078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21553 19078 603 41 0 21512 0 vsize: 86212 [startup+290.012 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20049 0 0 0 28943 60 0 0 25 0 1 0 483158402 88969216 19247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21721 19247 603 41 0 21680 0 vsize: 86884 [startup+300.013 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20232 0 0 0 29942 61 0 0 25 0 1 0 483158402 89702400 19430 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21900 19430 603 41 0 21859 0 vsize: 87600 [startup+310.013 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20401 0 0 0 30942 61 0 0 25 0 1 0 483158402 90361856 19599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22061 19599 603 41 0 22020 0 vsize: 88244 [startup+320.014 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20588 0 0 0 31941 62 0 0 25 0 1 0 483158402 91160576 19786 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22256 19786 603 41 0 22215 0 vsize: 89024 [startup+330.014 s] Raw data (loadavg): 0.99 0.96 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20757 0 0 0 32940 64 0 0 25 0 1 0 483158402 91840512 19955 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22422 19955 603 41 0 22381 0 vsize: 89688 [startup+340.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 20922 0 0 0 33939 64 0 0 25 0 1 0 483158402 92549120 20120 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22595 20120 603 41 0 22554 0 vsize: 90380 [startup+350.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21086 0 0 0 34938 65 0 0 25 0 1 0 483158402 93310976 20284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22781 20284 603 41 0 22740 0 vsize: 91124 [startup+360.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21251 0 0 0 35938 66 0 0 25 0 1 0 483158402 93995008 20449 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22948 20449 603 41 0 22907 0 vsize: 91792 [startup+370.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21401 0 0 0 36938 66 0 0 25 0 1 0 483158402 94519296 20599 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23076 20599 603 41 0 23035 0 vsize: 92304 [startup+380.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21563 0 0 0 37938 67 0 0 25 0 1 0 483158402 95186944 20761 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23239 20761 603 41 0 23198 0 vsize: 92956 [startup+390.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21688 0 0 0 38937 68 0 0 25 0 1 0 483158402 95727616 20886 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23371 20886 603 41 0 23330 0 vsize: 93484 [startup+400.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21774 0 0 0 39937 68 0 0 25 0 1 0 483158402 96124928 20972 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23468 20972 603 41 0 23427 0 vsize: 93872 [startup+410.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 21905 0 0 0 40936 69 0 0 25 0 1 0 483158402 96657408 21103 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23598 21103 603 41 0 23557 0 vsize: 94392 [startup+420.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22003 0 0 0 41935 70 0 0 25 0 1 0 483158402 97083392 21201 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23702 21201 603 41 0 23661 0 vsize: 94808 [startup+430.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22116 0 0 0 42935 70 0 0 25 0 1 0 483158402 97513472 21314 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23807 21314 603 41 0 23766 0 vsize: 95228 [startup+440.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22222 0 0 0 43935 70 0 0 25 0 1 0 483158402 97927168 21420 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23908 21420 603 41 0 23867 0 vsize: 95632 [startup+450.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22339 0 0 0 44934 71 0 0 25 0 1 0 483158402 98455552 21537 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24037 21537 603 41 0 23996 0 vsize: 96148 [startup+460.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22424 0 0 0 45934 71 0 0 25 0 1 0 483158402 99241984 21622 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24229 21622 603 41 0 24188 0 vsize: 96916 [startup+470.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22506 0 0 0 46933 72 0 0 25 0 1 0 483158402 99639296 21704 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24326 21704 603 41 0 24285 0 vsize: 97304 [startup+480.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22642 0 0 0 47933 73 0 0 25 0 1 0 483158402 100184064 21840 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24459 21840 603 41 0 24418 0 vsize: 97836 [startup+490.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22753 0 0 0 48932 73 0 0 25 0 1 0 483158402 100601856 21951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24561 21951 603 41 0 24520 0 vsize: 98244 [startup+500.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22871 0 0 0 49932 74 0 0 25 0 1 0 483158402 101130240 22069 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24690 22069 603 41 0 24649 0 vsize: 98760 [startup+510.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 22996 0 0 0 50931 75 0 0 25 0 1 0 483158402 101658624 22194 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24819 22194 603 41 0 24778 0 vsize: 99276 [startup+520.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23111 0 0 0 51931 75 0 0 25 0 1 0 483158402 102060032 22309 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24917 22309 603 41 0 24876 0 vsize: 99668 [startup+530.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23235 0 0 0 52930 76 0 0 25 0 1 0 483158402 102604800 22433 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25050 22433 603 41 0 25009 0 vsize: 100200 [startup+540.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23371 0 0 0 53930 76 0 0 25 0 1 0 483158402 103157760 22569 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25185 22569 603 41 0 25144 0 vsize: 100740 [startup+550.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23480 0 0 0 54930 77 0 0 25 0 1 0 483158402 103555072 22678 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25282 22678 603 41 0 25241 0 vsize: 101128 [startup+560.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23570 0 0 0 55929 77 0 0 25 0 1 0 483158402 103956480 22768 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25380 22768 603 41 0 25339 0 vsize: 101520 [startup+570.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23696 0 0 0 56929 78 0 0 25 0 1 0 483158402 104493056 22894 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25511 22894 603 41 0 25470 0 vsize: 102044 [startup+580.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 23836 0 0 0 57929 78 0 0 25 0 1 0 483158402 105025536 23034 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25641 23034 603 41 0 25600 0 vsize: 102564 [startup+590.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24126 0 0 0 58927 80 0 0 25 0 1 0 483158402 106237952 23324 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25937 23324 603 41 0 25896 0 vsize: 103748 [startup+600.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24315 0 0 0 59927 80 0 0 25 0 1 0 483158402 106921984 23513 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26104 23513 603 41 0 26063 0 vsize: 104416 [startup+610.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24477 0 0 0 60927 81 0 0 25 0 1 0 483158402 107458560 23675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26235 23675 603 41 0 26194 0 vsize: 104940 [startup+620.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24639 0 0 0 61926 81 0 0 25 0 1 0 483158402 108052480 23837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26380 23837 603 41 0 26339 0 vsize: 105520 [startup+630.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24794 0 0 0 62926 82 0 0 25 0 1 0 483158402 108720128 23992 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26543 23992 603 41 0 26502 0 vsize: 106172 [startup+640.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 24954 0 0 0 63926 82 0 0 25 0 1 0 483158402 109387776 24152 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26706 24152 603 41 0 26665 0 vsize: 106824 [startup+650.029 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25140 0 0 0 64925 83 0 0 25 0 1 0 483158402 110194688 24338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26903 24338 603 41 0 26862 0 vsize: 107612 [startup+660.029 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25325 0 0 0 65925 84 0 0 25 0 1 0 483158402 110862336 24523 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27066 24523 603 41 0 27025 0 vsize: 108264 [startup+670.029 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25516 0 0 0 66924 85 0 0 25 0 1 0 483158402 111665152 24714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27262 24714 603 41 0 27221 0 vsize: 109048 [startup+680.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25692 0 0 0 67924 85 0 0 25 0 1 0 483158402 112476160 24890 4294967295 134512640 134672761 3221224544 3221223500 1075350469 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27460 24890 603 41 0 27419 0 vsize: 109840 [startup+690.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 25882 0 0 0 68922 87 0 0 25 0 1 0 483158402 113303552 25080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27662 25080 603 41 0 27621 0 vsize: 110648 [startup+700.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26088 0 0 0 69922 87 0 0 25 0 1 0 483158402 114122752 25286 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27862 25286 603 41 0 27821 0 vsize: 111448 [startup+710.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26282 0 0 0 70922 88 0 0 25 0 1 0 483158402 114925568 25480 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28058 25480 603 41 0 28017 0 vsize: 112232 [startup+720.032 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26467 0 0 0 71921 88 0 0 25 0 1 0 483158402 115597312 25665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28222 25665 603 41 0 28181 0 vsize: 112888 [startup+730.032 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26654 0 0 0 72921 89 0 0 25 0 1 0 483158402 116404224 25852 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28419 25852 603 41 0 28378 0 vsize: 113676 [startup+740.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 26839 0 0 0 73920 90 0 0 25 0 1 0 483158402 117231616 26037 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28621 26037 603 41 0 28580 0 vsize: 114484 [startup+750.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27002 0 0 0 74919 91 0 0 25 0 1 0 483158402 117903360 26200 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28785 26200 603 41 0 28744 0 vsize: 115140 [startup+760.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27169 0 0 0 75919 91 0 0 25 0 1 0 483158402 118579200 26367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28950 26367 603 41 0 28909 0 vsize: 115800 [startup+770.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27332 0 0 0 76918 92 0 0 25 0 1 0 483158402 119115776 26530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29081 26530 603 41 0 29040 0 vsize: 116324 [startup+780.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27470 0 0 0 77918 93 0 0 25 0 1 0 483158402 119701504 26668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29224 26668 603 41 0 29183 0 vsize: 116896 [startup+790.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27615 0 0 0 78917 93 0 0 25 0 1 0 483158402 120393728 26813 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29393 26813 603 41 0 29352 0 vsize: 117572 [startup+800.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27776 0 0 0 79917 94 0 0 25 0 1 0 483158402 121131008 26974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29573 26974 603 41 0 29532 0 vsize: 118292 [startup+810.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 27929 0 0 0 80916 95 0 0 25 0 1 0 483158402 121667584 27127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29704 27127 603 41 0 29663 0 vsize: 118816 [startup+820.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28055 0 0 0 81916 95 0 0 25 0 1 0 483158402 122204160 27253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29835 27253 603 41 0 29794 0 vsize: 119340 [startup+830.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28130 0 0 0 82915 95 0 0 25 0 1 0 483158402 122474496 27328 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29901 27328 603 41 0 29860 0 vsize: 119604 [startup+840.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28240 0 0 0 83915 96 0 0 25 0 1 0 483158402 122875904 27438 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29999 27438 603 41 0 29958 0 vsize: 119996 [startup+850.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28299 0 0 0 84915 96 0 0 25 0 1 0 483158402 123133952 27497 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30062 27497 603 41 0 30021 0 vsize: 120248 [startup+860.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28420 0 0 0 85915 96 0 0 25 0 1 0 483158402 123666432 27618 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30192 27618 603 41 0 30151 0 vsize: 120768 [startup+870.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28591 0 0 0 86914 97 0 0 25 0 1 0 483158402 124334080 27789 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30355 27789 603 41 0 30314 0 vsize: 121420 [startup+880.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28762 0 0 0 87914 97 0 0 25 0 1 0 483158402 125169664 27960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30559 27960 603 41 0 30518 0 vsize: 122236 [startup+890.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 28938 0 0 0 88914 98 0 0 25 0 1 0 483158402 125845504 28136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30724 28136 603 41 0 30683 0 vsize: 122896 [startup+900.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29096 0 0 0 89913 98 0 0 25 0 1 0 483158402 126382080 28294 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30855 28294 603 41 0 30814 0 vsize: 123420 [startup+910.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29240 0 0 0 90913 99 0 0 25 0 1 0 483158402 127053824 28438 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31019 28438 603 41 0 30978 0 vsize: 124076 [startup+920.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29400 0 0 0 91913 100 0 0 25 0 1 0 483158402 127717376 28598 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31181 28598 603 41 0 31140 0 vsize: 124724 [startup+930.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29562 0 0 0 92912 100 0 0 25 0 1 0 483158402 128393216 28760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31346 28760 603 41 0 31305 0 vsize: 125384 [startup+940.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29731 0 0 0 93912 100 0 0 25 0 1 0 483158402 129056768 28929 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31508 28929 603 41 0 31467 0 vsize: 126032 [startup+950.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 29894 0 0 0 94912 101 0 0 25 0 1 0 483158402 129724416 29092 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31671 29092 603 41 0 31630 0 vsize: 126684 [startup+960.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30055 0 0 0 95911 102 0 0 25 0 1 0 483158402 130392064 29253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31834 29253 603 41 0 31793 0 vsize: 127336 [startup+970.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30207 0 0 0 96911 102 0 0 25 0 1 0 483158402 130924544 29405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31964 29405 603 41 0 31923 0 vsize: 127856 [startup+980.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30340 0 0 0 97911 102 0 0 25 0 1 0 483158402 131469312 29538 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32097 29538 603 41 0 32056 0 vsize: 128388 [startup+990.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30437 0 0 0 98911 102 0 0 25 0 1 0 483158402 131870720 29635 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32195 29635 603 41 0 32154 0 vsize: 128780 [startup+1000.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30586 0 0 0 99911 103 0 0 25 0 1 0 483158402 132689920 29784 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32395 29784 603 41 0 32354 0 vsize: 129580 [startup+1010.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30720 0 0 0 100911 103 0 0 25 0 1 0 483158402 133230592 29918 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32527 29918 603 41 0 32486 0 vsize: 130108 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30847 0 0 0 101911 103 0 0 25 0 1 0 483158402 133632000 30045 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32625 30045 603 41 0 32584 0 vsize: 130500 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 30965 0 0 0 102911 103 0 0 25 0 1 0 483158402 134168576 30163 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32756 30163 603 41 0 32715 0 vsize: 131024 [startup+1040.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31092 0 0 0 103911 104 0 0 25 0 1 0 483158402 134705152 30290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32887 30290 603 41 0 32846 0 vsize: 131548 [startup+1050.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31209 0 0 0 104911 104 0 0 25 0 1 0 483158402 135102464 30407 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32984 30407 603 41 0 32943 0 vsize: 131936 [startup+1060.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31324 0 0 0 105911 104 0 0 25 0 1 0 483158402 135634944 30522 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33114 30522 603 41 0 33073 0 vsize: 132456 [startup+1070.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31438 0 0 0 106911 105 0 0 25 0 1 0 483158402 136036352 30636 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33212 30636 603 41 0 33171 0 vsize: 132848 [startup+1080.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31547 0 0 0 107910 105 0 0 25 0 1 0 483158402 136433664 30745 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33309 30745 603 41 0 33268 0 vsize: 133236 [startup+1090.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31665 0 0 0 108910 106 0 0 25 0 1 0 483158402 137019392 30863 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33452 30863 603 41 0 33411 0 vsize: 133808 [startup+1100.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31778 0 0 0 109910 106 0 0 25 0 1 0 483158402 137416704 30976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33549 30976 603 41 0 33508 0 vsize: 134196 [startup+1110.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 31893 0 0 0 110909 107 0 0 25 0 1 0 483158402 137953280 31091 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33680 31091 603 41 0 33639 0 vsize: 134720 [startup+1120.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32003 0 0 0 111909 107 0 0 25 0 1 0 483158402 138420224 31201 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33794 31201 603 41 0 33753 0 vsize: 135176 [startup+1130.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32106 0 0 0 112909 108 0 0 25 0 1 0 483158402 138821632 31304 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33892 31304 603 41 0 33851 0 vsize: 135568 [startup+1140.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32217 0 0 0 113909 108 0 0 25 0 1 0 483158402 139223040 31415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33990 31415 603 41 0 33949 0 vsize: 135960 [startup+1150.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32336 0 0 0 114908 108 0 0 25 0 1 0 483158402 139759616 31534 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34121 31534 603 41 0 34080 0 vsize: 136484 [startup+1160.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32458 0 0 0 115908 109 0 0 25 0 1 0 483158402 140279808 31656 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34248 31656 603 41 0 34207 0 vsize: 136992 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32580 0 0 0 116908 109 0 0 25 0 1 0 483158402 140812288 31778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34378 31778 603 41 0 34337 0 vsize: 137512 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32691 0 0 0 117908 110 0 0 25 0 1 0 483158402 141213696 31889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34476 31889 603 41 0 34435 0 vsize: 137904 [startup+1190.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32823 0 0 0 118907 110 0 0 25 0 1 0 483158402 141889536 32021 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34641 32021 603 41 0 34600 0 vsize: 138564 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 26218 Raw data (stat): 26218 (minisat+) R 26217 32461 32460 0 -1 0 32929 0 0 0 119907 110 0 0 25 0 1 0 483158402 142290944 32127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34739 32127 603 41 0 34698 0 vsize: 138956 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.97 1/54 26218 Raw data (stat): 26218 (minisat+) Z 26217 32461 32460 0 -1 12 32931 0 0 0 119907 117 0 0 25 0 1 0 483158402 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.11 CPU time (s): 1200.25 CPU user time (s): 1199.08 CPU system time (s): 1.17182 CPU usage (%): 100.012 Max. virtual memory (Kb): 138956 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####