Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-pp08aCUTS.opb |
MD5SUM | fa6454a9831f2da4180d8bfab7c0a21b |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 2304 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 178464600 |
Number of bits of the sum of numbers in the objective function | 28 |
Biggest number in a constraint | 1048576 |
Number of bits of the biggest number in a constraint | 21 |
Biggest sum of numbers in a constraint | 178464600 |
Number of bits of the biggest sum of numbers | 28 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.037993 |
Number of variables | 3288 |
Total number of constraints | 310 |
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 | 310 |
Minimum length of a constraint | 14 |
Maximum length of a constraint | 123 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc19 THE 2005-04-21 12:53:59 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18764 boxname=wulflinc19 idbench=1444 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: fa6454a9831f2da4180d8bfab7c0a21b /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-pp08aCUTS.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-pp08aCUTS.opb IDLAUNCH: 18764 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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: 787440 kB Buffers: 16604 kB Cached: 206152 kB SwapCached: 556 kB Active: 35076 kB Inactive: 189728 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 787188 kB SwapTotal: 2097892 kB SwapFree: 2096388 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5164 kB Slab: 16568 kB Committed_AS: 63848 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 13:14:01 (client local time) WITH STATUS 0 IN 1200.22 SECONDS stats: 18764 7 1200.22 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 374 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################ c -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss c ---[ 501]---> BDD-cost: 15 c ---[ 500]---> BDD-cost: 15 c ---[ 499]---> BDD-cost: 15 c ---[ 498]---> BDD-cost: 15 c ---[ 497]---> BDD-cost: 15 c ---[ 496]---> BDD-cost: 15 c ---[ 495]---> BDD-cost: 15 c ---[ 494]---> BDD-cost: 15 c ---[ 485]---> BDD-cost: 15 c ---[ 484]---> BDD-cost: 15 c ---[ 483]---> BDD-cost: 15 c ---[ 482]---> BDD-cost: 15 c ---[ 481]---> BDD-cost: 15 c ---[ 480]---> BDD-cost: 15 c ---[ 479]---> BDD-cost: 15 c ---[ 477]---> BDD-cost: 15 c ---[ 476]---> BDD-cost: 15 c ---[ 475]---> BDD-cost: 15 c ---[ 474]---> BDD-cost: 15 c ---[ 473]---> BDD-cost: 15 c ---[ 472]---> BDD-cost: 15 c ---[ 471]---> BDD-cost: 15 c ---[ 469]---> BDD-cost: 14 c ---[ 468]---> BDD-cost: 14 c ---[ 467]---> BDD-cost: 14 c ---[ 466]---> BDD-cost: 14 c ---[ 465]---> BDD-cost: 14 c ---[ 464]---> BDD-cost: 14 c ---[ 463]---> BDD-cost: 14 c ---[ 462]---> BDD-cost: 14 c ---[ 461]---> BDD-cost: 15 c ---[ 460]---> BDD-cost: 15 c ---[ 459]---> BDD-cost: 15 c ---[ 458]---> BDD-cost: 15 c ---[ 457]---> BDD-cost: 15 c ---[ 456]---> BDD-cost: 15 c ---[ 455]---> BDD-cost: 15 c ---[ 454]---> BDD-cost: 15 c ---[ 445]---> BDD-cost: 13 c ---[ 444]---> BDD-cost: 13 c ---[ 443]---> BDD-cost: 13 c ---[ 442]---> BDD-cost: 13 c ---[ 441]---> BDD-cost: 13 c ---[ 440]---> BDD-cost: 13 c ---[ 439]---> BDD-cost: 13 c ---[ 438]---> BDD-cost: 13 c ---[ 437]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 436]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 435]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 434]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 433]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 432]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 431]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 430]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 428]---> BDD-cost: 158 c ---[ 426]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 424]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 422]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 420]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 418]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 416]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 414]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 412]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 410]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 408]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 406]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 404]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 402]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 400]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 398]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 396]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 394]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 392]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 390]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 388]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 386]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 384]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 382]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 380]---> BDD-cost: 158 c ---[ 378]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 376]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 374]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 372]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 370]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 368]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 366]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 364]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 362]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 360]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 358]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 356]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 354]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 352]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 350]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 348]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 346]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 344]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 342]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 340]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 338]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 336]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 334]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 332]---> BDD-cost: 154 c ---[ 330]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 328]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 326]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 324]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 322]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 320]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 318]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 316]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 314]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 312]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 310]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 308]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 306]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 304]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 302]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 301]---> BDD-cost: 9 c ---[ 300]---> BDD-cost: 9 c ---[ 299]---> BDD-cost: 9 c ---[ 298]---> BDD-cost: 6 c ---[ 297]---> BDD-cost: 6 c ---[ 296]---> BDD-cost: 6 c ---[ 295]---> BDD-cost: 6 c ---[ 294]---> BDD-cost: 8 c ---[ 293]---> BDD-cost: 19 c ---[ 292]---> BDD-cost: 19 c ---[ 291]---> BDD-cost: 19 c ---[ 290]---> BDD-cost: 19 c ---[ 289]---> BDD-cost: 19 c ---[ 288]---> BDD-cost: 19 c ---[ 287]---> BDD-cost: 19 c ---[ 286]---> BDD-cost: 19 c ---[ 285]---> BDD-cost: 9 c ---[ 284]---> BDD-cost: 9 c ---[ 283]---> BDD-cost: 9 c ---[ 282]---> BDD-cost: 6 c ---[ 281]---> BDD-cost: 6 c ---[ 280]---> BDD-cost: 6 c ---[ 279]---> BDD-cost: 6 c ---[ 278]---> BDD-cost: 23 c ---[ 277]---> BDD-cost: 9 c ---[ 276]---> BDD-cost: 9 c ---[ 275]---> BDD-cost: 9 c ---[ 274]---> BDD-cost: 6 c ---[ 273]---> BDD-cost: 6 c ---[ 272]---> BDD-cost: 6 c ---[ 271]---> BDD-cost: 6 c ---[ 270]---> BDD-cost: 23 c ---[ 269]---> BDD-cost: 4 c ---[ 268]---> BDD-cost: 4 c ---[ 267]---> BDD-cost: 4 c ---[ 266]---> BDD-cost: 4 c ---[ 265]---> BDD-cost: 4 c ---[ 264]---> BDD-cost: 4 c ---[ 263]---> BDD-cost: 4 c ---[ 262]---> BDD-cost: 4 c ---[ 261]---> BDD-cost: 9 c ---[ 260]---> BDD-cost: 9 c ---[ 259]---> BDD-cost: 9 c ---[ 258]---> BDD-cost: 6 c ---[ 257]---> BDD-cost: 6 c ---[ 256]---> BDD-cost: 6 c ---[ 255]---> BDD-cost: 6 c ---[ 254]---> BDD-cost: 6 c ---[ 253]---> BDD-cost: 19 c ---[ 252]---> BDD-cost: 19 c ---[ 251]---> BDD-cost: 19 c ---[ 250]---> BDD-cost: 19 c ---[ 249]---> BDD-cost: 19 c ---[ 248]---> BDD-cost: 19 c ---[ 247]---> BDD-cost: 19 c ---[ 246]---> BDD-cost: 19 c ---[ 245]---> BDD-cost: 6 c ---[ 244]---> BDD-cost: 6 c ---[ 243]---> BDD-cost: 6 c ---[ 242]---> BDD-cost: 6 c ---[ 241]---> BDD-cost: 6 c ---[ 240]---> BDD-cost: 6 c ---[ 239]---> BDD-cost: 6 c ---[ 238]---> BDD-cost: 6 c ---[ 127]---> BDD-cost: 1 c ---[ 126]---> BDD-cost: 1 c ---[ 125]---> BDD-cost: 1 c ---[ 124]---> BDD-cost: 1 c ---[ 123]---> BDD-cost: 1 c ---[ 122]---> BDD-cost: 1 c ---[ 121]---> BDD-cost: 1 c ---[ 120]---> BDD-cost: 1 c ---[ 119]---> BDD-cost: 1 c ---[ 118]---> BDD-cost: 1 c ---[ 117]---> BDD-cost: 1 c ---[ 116]---> BDD-cost: 1 c ---[ 115]---> BDD-cost: 1 c ---[ 114]---> BDD-cost: 1 c ---[ 113]---> BDD-cost: 1 c ---[ 112]---> BDD-cost: 1 c ---[ 111]---> BDD-cost: 1 c ---[ 110]---> BDD-cost: 1 c ---[ 109]---> BDD-cost: 50 c ---[ 108]---> BDD-cost: 167 c ---[ 107]---> BDD-cost: 59 c ---[ 106]---> BDD-cost: 38 c ---[ 105]---> BDD-cost: 149 c ---[ 104]---> BDD-cost: 35 c ---[ 103]---> BDD-cost: 152 c ---[ 102]---> BDD-cost: 35 c ---[ 101]---> BDD-cost: 152 c ---[ 100]---> BDD-cost: 38 c ---[ 99]---> BDD-cost: 149 c ---[ 98]---> BDD-cost: 4 c ---[ 97]---> BDD-cost: 5 c ---[ 96]---> BDD-cost: 62 c ---[ 95]---> BDD-cost: 73 c ---[ 94]---> BDD-cost: 3 c ---[ 93]---> BDD-cost: 62 c ---[ 92]---> BDD-cost: 41 c ---[ 91]---> BDD-cost: 158 c ---[ 90]---> BDD-cost: 45 c ---[ 89]---> BDD-cost: 182 c ---[ 88]---> BDD-cost: 40 c ---[ 87]---> BDD-cost: 203 c ---[ 86]---> BDD-cost: 173 c ---[ 85]---> BDD-cost: 35 c ---[ 84]---> BDD-cost: 164 c ---[ 83]---> BDD-cost: 41 c ---[ 82]---> BDD-cost: 158 c ---[ 81]---> BDD-cost: 5 c ---[ 80]---> BDD-cost: 70 c ---[ 79]---> BDD-cost: 3 c ---[ 78]---> BDD-cost: 65 c ---[ 77]---> BDD-cost: 45 c ---[ 76]---> BDD-cost: 45 c ---[ 75]---> BDD-cost: 194 c ---[ 74]---> BDD-cost: 48 c ---[ 73]---> BDD-cost: 191 c ---[ 72]---> BDD-cost: 41 c ---[ 71]---> BDD-cost: 170 c ---[ 70]---> BDD-cost: 44 c ---[ 69]---> BDD-cost: 167 c ---[ 68]---> BDD-cost: 50 c ---[ 67]---> BDD-cost: 203 c ---[ 66]---> BDD-cost: 3 c ---[ 65]---> BDD-cost: 194 c ---[ 64]---> BDD-cost: 61 c ---[ 63]---> BDD-cost: 48 c ---[ 62]---> BDD-cost: 191 c ---[ 61]---> BDD-cost: 48 c ---[ 60]---> BDD-cost: 191 c ---[ 59]---> BDD-cost: 55 c ---[ 58]---> Sorter-cost: 751 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> BDD-cost: 47 c ---[ 56]---> BDD-cost: 161 c ---[ 55]---> BDD-cost: 50 c ---[ 54]---> BDD-cost: 48 c ---[ 53]---> BDD-cost: 203 c ---[ 52]---> BDD-cost: 48 c ---[ 51]---> BDD-cost: 191 c ---[ 50]---> BDD-cost: 5 c ---[ 49]---> BDD-cost: 73 c ---[ 48]---> BDD-cost: 5 c ---[ 47]---> BDD-cost: 70 c ---[ 46]---> BDD-cost: 38 c ---[ 45]---> BDD-cost: 161 c ---[ 44]---> BDD-cost: 41 c ---[ 43]---> BDD-cost: 191 c ---[ 42]---> BDD-cost: 158 c ---[ 41]---> BDD-cost: 35 c ---[ 40]---> BDD-cost: 164 c ---[ 39]---> BDD-cost: 35 c ---[ 38]---> BDD-cost: 164 c ---[ 37]---> BDD-cost: 38 c ---[ 36]---> BDD-cost: 161 c ---[ 35]---> BDD-cost: 3 c ---[ 34]---> BDD-cost: 64 c ---[ 33]---> BDD-cost: 6 c ---[ 32]---> BDD-cost: 38 c ---[ 31]---> BDD-cost: 78 c ---[ 30]---> BDD-cost: 41 c ---[ 29]---> BDD-cost: 170 c ---[ 28]---> BDD-cost: 41 c ---[ 27]---> BDD-cost: 170 c ---[ 26]---> BDD-cost: 41 c ---[ 25]---> BDD-cost: 170 c ---[ 24]---> BDD-cost: 48 c ---[ 23]---> BDD-cost: 191 c ---[ 22]---> BDD-cost: 38 c ---[ 21]---> BDD-cost: 173 c ---[ 20]---> BDD-cost: 173 c ---[ 19]---> BDD-cost: 41 c ---[ 18]---> BDD-cost: 170 c ---[ 17]---> BDD-cost: 5 c ---[ 16]---> BDD-cost: 75 c ---[ 15]---> BDD-cost: 38 c ---[ 14]---> BDD-cost: 161 c ---[ 13]---> BDD-cost: 45 c ---[ 12]---> BDD-cost: 182 c ---[ 11]---> BDD-cost: 35 c ---[ 10]---> BDD-cost: 44 c ---[ 9]---> BDD-cost: 164 c ---[ 8]---> BDD-cost: 38 c ---[ 7]---> BDD-cost: 161 c ---[ 6]---> BDD-cost: 43 c ---[ 5]---> BDD-cost: 170 c ---[ 4]---> BDD-cost: 41 c ---[ 3]---> BDD-cost: 158 c ---[ 2]---> BDD-cost: 3 c ---[ 1]---> BDD-cost: 60 c ---[ 0]---> BDD-cost: 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 215438 519594 | 71812 0 0 nan | 0.000 % | c | 100 | 215317 519326 | 78993 85 297 3.5 | 4.798 % | c | 252 | 215250 519177 | 86892 230 1279 5.6 | 4.822 % | c | 477 | 215017 518658 | 95581 419 1998 4.8 | 4.904 % | c | 814 | 214690 517929 | 105139 706 3191 4.5 | 5.022 % | c | 1320 | 214206 516851 | 115653 1147 4686 4.1 | 5.197 % | c | 2081 | 213777 515892 | 127219 1851 7475 4.0 | 5.346 % | c | 3220 | 213265 514751 | 139941 2913 13437 4.6 | 5.528 % | c | 4928 | 212597 513260 | 153935 4530 19792 4.4 | 5.766 % | c | 7491 | 211927 511762 | 169328 7017 31746 4.5 | 6.002 % | c | 11335 | 210797 509228 | 186261 10729 52175 4.9 | 6.392 % | c | 17102 | 209752 506890 | 204888 16365 92151 5.6 | 6.757 % | c | 25751 | 208643 504413 | 225376 24862 148831 6.0 | 7.149 % | c | 38725 | 208052 503090 | 247914 37757 317212 8.4 | 7.355 % | c | 58188 | 207566 501999 | 272705 57154 747689 13.1 | 7.526 % | c | 87380 | 206308 499177 | 299976 86159 1393567 16.2 | 7.970 % | c | 131171 | 206005 498499 | 329974 129904 2588408 19.9 | 8.077 % | c | 196857 | 205794 498026 | 362971 195554 4238870 21.7 | 8.152 % | c | 295383 | 205426 497203 | 399268 294027 7129688 24.2 | 8.284 % | #### 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.92 0.95 0.90 2/55 799 Raw data (stat): 799 (runsolver) R 798 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545229249 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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+10.0012 s] Raw data (loadavg): 0.93 0.96 0.91 2/55 799 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7180 0 0 0 983 15 0 0 25 0 1 0 545229249 33681408 6847 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8223 6847 603 41 0 8182 0 vsize: 32892 [startup+20.0022 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 799 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7222 0 0 0 1983 15 0 0 25 0 1 0 545229249 33816576 6889 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8256 6889 603 41 0 8215 0 vsize: 33024 [startup+30.0016 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 799 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7268 0 0 0 2982 16 0 0 25 0 1 0 545229249 33951744 6935 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8289 6935 603 41 0 8248 0 vsize: 33156 [startup+40.0019 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 799 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7315 0 0 0 3981 17 0 0 25 0 1 0 545229249 34111488 6982 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8328 6982 603 41 0 8287 0 vsize: 33312 [startup+50.0024 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 799 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7357 0 0 0 4980 17 0 0 25 0 1 0 545229249 34246656 7024 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8361 7024 603 41 0 8320 0 vsize: 33444 [startup+60.0029 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7414 0 0 0 5980 17 0 0 25 0 1 0 545229249 34603008 7081 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8448 7081 603 41 0 8407 0 vsize: 33792 [startup+70.003 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7460 0 0 0 6979 18 0 0 25 0 1 0 545229249 34734080 7127 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8480 7127 603 41 0 8439 0 vsize: 33920 [startup+80.0028 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7490 0 0 0 7979 18 0 0 25 0 1 0 545229249 34869248 7157 4294967295 134512640 134672761 3221224624 3221223792 134564738 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8513 7157 603 41 0 8472 0 vsize: 34052 [startup+90.0033 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7566 0 0 0 8979 18 0 0 25 0 1 0 545229249 35135488 7233 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8578 7233 603 41 0 8537 0 vsize: 34312 [startup+100.004 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7622 0 0 0 9979 18 0 0 25 0 1 0 545229249 35401728 7289 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8643 7289 603 41 0 8602 0 vsize: 34572 [startup+110.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7777 0 0 0 10979 19 0 0 25 0 1 0 545229249 36061184 7444 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8804 7444 603 41 0 8763 0 vsize: 35216 [startup+120.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 7911 0 0 0 11979 19 0 0 25 0 1 0 545229249 36597760 7578 4294967295 134512640 134672761 3221224624 3221223808 134559542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8935 7578 603 41 0 8894 0 vsize: 35740 [startup+130.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 8250 0 0 0 12978 20 0 0 25 0 1 0 545229249 37933056 7917 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9261 7917 603 41 0 9220 0 vsize: 37044 [startup+140.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 8420 0 0 0 13977 21 0 0 25 0 1 0 545229249 38596608 8087 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9423 8087 603 41 0 9382 0 vsize: 37692 [startup+150.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 8705 0 0 0 14976 22 0 0 25 0 1 0 545229249 40058880 8372 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9780 8372 603 41 0 9739 0 vsize: 39120 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 8815 0 0 0 15976 23 0 0 25 0 1 0 545229249 40460288 8482 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9878 8482 603 41 0 9837 0 vsize: 39512 [startup+170.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 8879 0 0 0 16976 23 0 0 25 0 1 0 545229249 40726528 8546 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9943 8546 603 41 0 9902 0 vsize: 39772 [startup+180.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 9029 0 0 0 17976 23 0 0 25 0 1 0 545229249 41263104 8696 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10074 8696 603 41 0 10033 0 vsize: 40296 [startup+190.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 9165 0 0 0 18976 23 0 0 25 0 1 0 545229249 41803776 8832 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10206 8832 603 41 0 10165 0 vsize: 40824 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 9314 0 0 0 19975 24 0 0 25 0 1 0 545229249 42475520 8981 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10370 8981 603 41 0 10329 0 vsize: 41480 [startup+210.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 9506 0 0 0 20975 24 0 0 25 0 1 0 545229249 43270144 9173 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10564 9173 603 41 0 10523 0 vsize: 42256 [startup+220.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 9618 0 0 0 21975 25 0 0 25 0 1 0 545229249 43675648 9285 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10663 9285 603 41 0 10622 0 vsize: 42652 [startup+230.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 9804 0 0 0 22974 26 0 0 25 0 1 0 545229249 44474368 9471 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10858 9471 603 41 0 10817 0 vsize: 43432 [startup+240.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 9997 0 0 0 23974 26 0 0 25 0 1 0 545229249 45142016 9664 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11021 9664 603 41 0 10980 0 vsize: 44084 [startup+250.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 10144 0 0 0 24974 27 0 0 25 0 1 0 545229249 45821952 9811 4294967295 134512640 134672761 3221224624 3221223840 134557543 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11187 9811 603 41 0 11146 0 vsize: 44748 [startup+260.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 10209 0 0 0 25974 27 0 0 25 0 1 0 545229249 45957120 9876 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11220 9876 603 41 0 11179 0 vsize: 44880 [startup+270.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 10518 0 0 0 26973 28 0 0 25 0 1 0 545229249 47271936 10185 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11541 10185 603 41 0 11500 0 vsize: 46164 [startup+280.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 10685 0 0 0 27972 28 0 0 25 0 1 0 545229249 47939584 10352 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11704 10352 603 41 0 11663 0 vsize: 46816 [startup+290.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 10860 0 0 0 28972 29 0 0 25 0 1 0 545229249 48611328 10527 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11868 10527 603 41 0 11827 0 vsize: 47472 [startup+300.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 10985 0 0 0 29972 30 0 0 25 0 1 0 545229249 49668096 10652 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12126 10652 603 41 0 12085 0 vsize: 48504 [startup+310.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 11059 0 0 0 30972 30 0 0 25 0 1 0 545229249 49938432 10726 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12192 10726 603 41 0 12151 0 vsize: 48768 [startup+320.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 11189 0 0 0 31971 30 0 0 25 0 1 0 545229249 50479104 10856 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12324 10856 603 41 0 12283 0 vsize: 49296 [startup+330.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 11295 0 0 0 32970 31 0 0 25 0 1 0 545229249 50876416 10962 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12421 10962 603 41 0 12380 0 vsize: 49684 [startup+340.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 11428 0 0 0 33970 31 0 0 25 0 1 0 545229249 51429376 11095 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12556 11095 603 41 0 12515 0 vsize: 50224 [startup+350.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 801 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 11593 0 0 0 34970 32 0 0 25 0 1 0 545229249 52125696 11260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12726 11260 603 41 0 12685 0 vsize: 50904 [startup+360.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 803 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 11733 0 0 0 35969 32 0 0 25 0 1 0 545229249 52686848 11400 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12863 11400 603 41 0 12822 0 vsize: 51452 [startup+370.01 s] Raw data (loadavg): 1.07 0.99 0.91 2/55 858 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 11817 0 0 0 36964 36 0 0 25 0 1 0 545229249 53096448 11484 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12963 11484 603 41 0 12922 0 vsize: 51852 [startup+380.01 s] Raw data (loadavg): 1.06 0.99 0.91 2/55 858 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 11918 0 0 0 37964 36 0 0 25 0 1 0 545229249 53362688 11585 4294967295 134512640 134672761 3221224624 3221223888 134562262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13028 11585 603 41 0 12987 0 vsize: 52112 [startup+390.011 s] Raw data (loadavg): 1.05 0.99 0.91 2/55 858 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 12057 0 0 0 38963 38 0 0 25 0 1 0 545229249 54026240 11724 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13190 11724 603 41 0 13149 0 vsize: 52760 [startup+400.011 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 858 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 12150 0 0 0 39962 38 0 0 25 0 1 0 545229249 54296576 11817 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13256 11817 603 41 0 13215 0 vsize: 53024 [startup+410.011 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 858 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 12225 0 0 0 40962 39 0 0 25 0 1 0 545229249 54697984 11892 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13354 11892 603 41 0 13313 0 vsize: 53416 [startup+420.011 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 858 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 12303 0 0 0 41961 40 0 0 25 0 1 0 545229249 54968320 11970 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13420 11970 603 41 0 13379 0 vsize: 53680 [startup+430.011 s] Raw data (loadavg): 1.03 0.99 0.91 2/55 858 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 12368 0 0 0 42960 41 0 0 25 0 1 0 545229249 55238656 12035 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13486 12035 603 41 0 13445 0 vsize: 53944 [startup+440.011 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 858 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 12479 0 0 0 43959 42 0 0 25 0 1 0 545229249 55635968 12146 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13583 12146 603 41 0 13542 0 vsize: 54332 [startup+450.011 s] Raw data (loadavg): 1.02 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 12648 0 0 0 44958 44 0 0 25 0 1 0 545229249 56311808 12315 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13748 12315 603 41 0 13707 0 vsize: 54992 [startup+460.012 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 12748 0 0 0 45957 45 0 0 25 0 1 0 545229249 56733696 12415 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13851 12415 603 41 0 13810 0 vsize: 55404 [startup+470.012 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 12940 0 0 0 46956 46 0 0 25 0 1 0 545229249 57528320 12607 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14045 12607 603 41 0 14004 0 vsize: 56180 [startup+480.012 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 13190 0 0 0 47955 47 0 0 25 0 1 0 545229249 58601472 12857 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14307 12857 603 41 0 14266 0 vsize: 57228 [startup+490.013 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 13277 0 0 0 48954 48 0 0 25 0 1 0 545229249 58871808 12944 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14373 12944 603 41 0 14332 0 vsize: 57492 [startup+500.013 s] Raw data (loadavg): 1.01 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 13337 0 0 0 49954 49 0 0 25 0 1 0 545229249 59142144 13004 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14439 13004 603 41 0 14398 0 vsize: 57756 [startup+510.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 13487 0 0 0 50953 50 0 0 25 0 1 0 545229249 59670528 13154 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14568 13154 603 41 0 14527 0 vsize: 58272 [startup+520.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 13567 0 0 0 51952 50 0 0 25 0 1 0 545229249 60076032 13234 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14667 13234 603 41 0 14626 0 vsize: 58668 [startup+530.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 13647 0 0 0 52952 51 0 0 25 0 1 0 545229249 60346368 13314 4294967295 134512640 134672761 3221224624 3221223760 134565096 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14733 13314 603 41 0 14692 0 vsize: 58932 [startup+540.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 13798 0 0 0 53951 52 0 0 25 0 1 0 545229249 60964864 13465 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14884 13465 603 41 0 14843 0 vsize: 59536 [startup+550.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 13874 0 0 0 54950 53 0 0 25 0 1 0 545229249 61362176 13541 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14981 13541 603 41 0 14940 0 vsize: 59924 [startup+560.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 13950 0 0 0 55950 54 0 0 25 0 1 0 545229249 61628416 13617 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15046 13617 603 41 0 15005 0 vsize: 60184 [startup+570.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 14083 0 0 0 56949 55 0 0 25 0 1 0 545229249 62160896 13750 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15176 13750 603 41 0 15135 0 vsize: 60704 [startup+580.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 14243 0 0 0 57949 55 0 0 25 0 1 0 545229249 62832640 13910 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15340 13910 603 41 0 15299 0 vsize: 61360 [startup+590.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 14392 0 0 0 58948 57 0 0 25 0 1 0 545229249 63500288 14059 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15503 14059 603 41 0 15462 0 vsize: 62012 [startup+600.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 14480 0 0 0 59947 58 0 0 25 0 1 0 545229249 63770624 14147 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15569 14147 603 41 0 15528 0 vsize: 62276 [startup+610.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 14548 0 0 0 60946 59 0 0 25 0 1 0 545229249 64036864 14215 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15634 14215 603 41 0 15593 0 vsize: 62536 [startup+620.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 14655 0 0 0 61944 60 0 0 25 0 1 0 545229249 64573440 14322 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15765 14322 603 41 0 15724 0 vsize: 63060 [startup+630.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 14854 0 0 0 62943 62 0 0 25 0 1 0 545229249 65368064 14521 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15959 14521 603 41 0 15918 0 vsize: 63836 [startup+640.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 15071 0 0 0 63942 63 0 0 25 0 1 0 545229249 66174976 14738 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16156 14738 603 41 0 16115 0 vsize: 64624 [startup+650.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 860 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 15304 0 0 0 64941 64 0 0 25 0 1 0 545229249 67117056 14971 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16386 14971 603 41 0 16345 0 vsize: 65544 [startup+660.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 862 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 15433 0 0 0 65940 65 0 0 25 0 1 0 545229249 67653632 15100 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16517 15100 603 41 0 16476 0 vsize: 66068 [startup+670.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 862 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 15544 0 0 0 66940 66 0 0 25 0 1 0 545229249 68050944 15211 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16614 15211 603 41 0 16573 0 vsize: 66456 [startup+680.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 862 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 15648 0 0 0 67939 67 0 0 25 0 1 0 545229249 69517312 15315 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16972 15315 603 41 0 16931 0 vsize: 67888 [startup+690.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 862 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 15757 0 0 0 68938 68 0 0 25 0 1 0 545229249 69922816 15424 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17071 15424 603 41 0 17030 0 vsize: 68284 [startup+700.018 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 862 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 15881 0 0 0 69938 68 0 0 25 0 1 0 545229249 70459392 15548 4294967295 134512640 134672761 3221224624 3221223792 134561275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17202 15548 603 41 0 17161 0 vsize: 68808 [startup+710.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 862 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 15954 0 0 0 70938 69 0 0 25 0 1 0 545229249 70737920 15621 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17270 15621 603 41 0 17229 0 vsize: 69080 [startup+720.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 862 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 16109 0 0 0 71936 70 0 0 25 0 1 0 545229249 71401472 15776 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17432 15776 603 41 0 17391 0 vsize: 69728 [startup+730.019 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 862 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 16280 0 0 0 72935 72 0 0 25 0 1 0 545229249 72069120 15947 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17595 15947 603 41 0 17554 0 vsize: 70380 [startup+740.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 862 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 16445 0 0 0 73935 72 0 0 25 0 1 0 545229249 72732672 16112 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17757 16112 603 41 0 17716 0 vsize: 71028 [startup+750.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 16610 0 0 0 74934 73 0 0 25 0 1 0 545229249 73400320 16277 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17920 16277 603 41 0 17879 0 vsize: 71680 [startup+760.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 16790 0 0 0 75933 74 0 0 25 0 1 0 545229249 74256384 16457 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18129 16457 603 41 0 18088 0 vsize: 72516 [startup+770.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 16937 0 0 0 76933 75 0 0 25 0 1 0 545229249 74805248 16604 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18263 16604 603 41 0 18222 0 vsize: 73052 [startup+780.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 17056 0 0 0 77932 76 0 0 25 0 1 0 545229249 75350016 16723 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18396 16723 603 41 0 18355 0 vsize: 73584 [startup+790.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 17144 0 0 0 78932 76 0 0 25 0 1 0 545229249 75776000 16811 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18500 16811 603 41 0 18459 0 vsize: 74000 [startup+800.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 17306 0 0 0 79931 77 0 0 25 0 1 0 545229249 76451840 16973 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18665 16973 603 41 0 18624 0 vsize: 74660 [startup+810.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 17490 0 0 0 80930 78 0 0 25 0 1 0 545229249 77123584 17157 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18829 17157 603 41 0 18788 0 vsize: 75316 [startup+820.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 17569 0 0 0 81930 79 0 0 25 0 1 0 545229249 77393920 17236 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18895 17236 603 41 0 18854 0 vsize: 75580 [startup+830.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 17663 0 0 0 82929 80 0 0 25 0 1 0 545229249 77795328 17330 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18993 17330 603 41 0 18952 0 vsize: 75972 [startup+840.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 17749 0 0 0 83929 80 0 0 25 0 1 0 545229249 78196736 17416 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19091 17416 603 41 0 19050 0 vsize: 76364 [startup+850.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 17860 0 0 0 84928 81 0 0 25 0 1 0 545229249 78594048 17527 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19188 17527 603 41 0 19147 0 vsize: 76752 [startup+860.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 17967 0 0 0 85927 83 0 0 25 0 1 0 545229249 78995456 17634 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19286 17634 603 41 0 19245 0 vsize: 77144 [startup+870.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 18116 0 0 0 86926 84 0 0 25 0 1 0 545229249 79556608 17783 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19423 17783 603 41 0 19382 0 vsize: 77692 [startup+880.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 18258 0 0 0 87925 85 0 0 25 0 1 0 545229249 80220160 17925 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19585 17925 603 41 0 19544 0 vsize: 78340 [startup+890.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 18373 0 0 0 88925 85 0 0 25 0 1 0 545229249 80617472 18040 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19682 18040 603 41 0 19641 0 vsize: 78728 [startup+900.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 18485 0 0 0 89925 86 0 0 25 0 1 0 545229249 81018880 18152 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19780 18152 603 41 0 19739 0 vsize: 79120 [startup+910.026 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 18610 0 0 0 90924 86 0 0 25 0 1 0 545229249 81555456 18277 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19911 18277 603 41 0 19870 0 vsize: 79644 [startup+920.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 18807 0 0 0 91923 87 0 0 25 0 1 0 545229249 82354176 18474 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20106 18474 603 41 0 20065 0 vsize: 80424 [startup+930.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 18987 0 0 0 92922 88 0 0 25 0 1 0 545229249 83021824 18654 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20269 18654 603 41 0 20228 0 vsize: 81076 [startup+940.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 19146 0 0 0 93921 90 0 0 25 0 1 0 545229249 83681280 18813 4294967295 134512640 134672761 3221224624 3221223816 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20430 18813 603 41 0 20389 0 vsize: 81720 [startup+950.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 864 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 19576 0 0 0 94919 92 0 0 25 0 1 0 545229249 85409792 19243 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20852 19243 603 41 0 20811 0 vsize: 83408 [startup+960.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 20055 0 0 0 95918 94 0 0 25 0 1 0 545229249 87429120 19722 4294967295 134512640 134672761 3221224624 3221223808 134559376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21345 19722 603 41 0 21304 0 vsize: 85380 [startup+970.028 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 20215 0 0 0 96918 94 0 0 25 0 1 0 545229249 87973888 19882 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21478 19882 603 41 0 21437 0 vsize: 85912 [startup+980.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 20306 0 0 0 97918 94 0 0 25 0 1 0 545229249 88379392 19973 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21577 19973 603 41 0 21536 0 vsize: 86308 [startup+990.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 20427 0 0 0 98917 94 0 0 25 0 1 0 545229249 88838144 20094 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21689 20094 603 41 0 21648 0 vsize: 86756 [startup+1000.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 20543 0 0 0 99917 95 0 0 25 0 1 0 545229249 89427968 20210 4294967295 134512640 134672761 3221224624 3221223776 134565137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21833 20210 603 41 0 21792 0 vsize: 87332 [startup+1010.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 20653 0 0 0 100917 95 0 0 25 0 1 0 545229249 89829376 20320 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21931 20320 603 41 0 21890 0 vsize: 87724 [startup+1020.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 20711 0 0 0 101917 95 0 0 25 0 1 0 545229249 90095616 20378 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21996 20378 603 41 0 21955 0 vsize: 87984 [startup+1030.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 20816 0 0 0 102917 95 0 0 25 0 1 0 545229249 90501120 20483 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22095 20483 603 41 0 22054 0 vsize: 88380 [startup+1040.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 20917 0 0 0 103917 96 0 0 25 0 1 0 545229249 90906624 20584 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22194 20584 603 41 0 22153 0 vsize: 88776 [startup+1050.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 21149 0 0 0 104916 97 0 0 25 0 1 0 545229249 91848704 20816 4294967295 134512640 134672761 3221224624 3221223792 134564689 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22424 20816 603 41 0 22383 0 vsize: 89696 [startup+1060.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 21377 0 0 0 105915 98 0 0 25 0 1 0 545229249 92651520 21044 4294967295 134512640 134672761 3221224624 3221223716 1075351233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22620 21044 603 41 0 22579 0 vsize: 90480 [startup+1070.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 21514 0 0 0 106915 98 0 0 25 0 1 0 545229249 93188096 21181 4294967295 134512640 134672761 3221224624 3221223808 134559609 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22751 21181 603 41 0 22710 0 vsize: 91004 [startup+1080.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 21589 0 0 0 107915 98 0 0 25 0 1 0 545229249 93593600 21256 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22850 21256 603 41 0 22809 0 vsize: 91400 [startup+1090.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 22011 0 0 0 108915 99 0 0 25 0 1 0 545229249 95207424 21678 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23244 21678 603 41 0 23203 0 vsize: 92976 [startup+1100.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 22493 0 0 0 109914 101 0 0 25 0 1 0 545229249 97230848 22160 4294967295 134512640 134672761 3221224624 3221223760 134542710 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23738 22160 603 41 0 23697 0 vsize: 94952 [startup+1110.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 22948 0 0 0 110913 102 0 0 25 0 1 0 545229249 99119104 22615 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24199 22615 603 41 0 24158 0 vsize: 96796 [startup+1120.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 23370 0 0 0 111912 103 0 0 25 0 1 0 545229249 100732928 23037 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24593 23037 603 41 0 24552 0 vsize: 98372 [startup+1130.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 23796 0 0 0 112911 104 0 0 25 0 1 0 545229249 102486016 23463 4294967295 134512640 134672761 3221224624 3221222400 134565885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25021 23463 603 41 0 24980 0 vsize: 100084 [startup+1140.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 23796 0 0 0 113911 104 0 0 25 0 1 0 545229249 102486016 23463 4294967295 134512640 134672761 3221224624 3221223520 1075352369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25021 23463 603 41 0 24980 0 vsize: 100084 [startup+1150.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 23796 0 0 0 114911 104 0 0 25 0 1 0 545229249 102486016 23463 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25021 23463 603 41 0 24980 0 vsize: 100084 [startup+1160.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 23796 0 0 0 115911 104 0 0 25 0 1 0 545229249 102486016 23463 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25021 23463 603 41 0 24980 0 vsize: 100084 [startup+1170.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 23796 0 0 0 116911 104 0 0 25 0 1 0 545229249 102486016 23463 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25021 23463 603 41 0 24980 0 vsize: 100084 [startup+1180.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 23796 0 0 0 117912 104 0 0 25 0 1 0 545229249 102486016 23463 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25021 23463 603 41 0 24980 0 vsize: 100084 [startup+1190.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 23796 0 0 0 118912 104 0 0 25 0 1 0 545229249 102486016 23463 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25021 23463 603 41 0 24980 0 vsize: 100084 [startup+1200.03 s] Raw data (loadavg): 1.00 0.99 0.91 2/55 866 Raw data (stat): 799 (minisat+) R 798 22929 22928 0 -1 0 23796 0 0 0 119912 104 0 0 25 0 1 0 545229249 102486016 23463 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25021 23463 603 41 0 24980 0 vsize: 100084 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 1.00 0.99 0.91 1/55 866 Raw data (stat): 799 (minisat+) Z 798 22929 22928 0 -1 12 23798 0 0 0 119912 108 0 0 25 0 1 0 545229249 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.08 CPU time (s): 1200.22 CPU user time (s): 1199.13 CPU system time (s): 1.08983 CPU usage (%): 100.011 Max. virtual memory (Kb): 100084 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####