Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm1.opb |
MD5SUM | ec9e3281577e2d3f7b25c1cc88cac9ea |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 29 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 168 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 168 |
Number of bits of the sum of numbers in the objective function | 8 |
Biggest number in a constraint | 102400 |
Number of bits of the biggest number in a constraint | 17 |
Biggest sum of numbers in a constraint | 615983 |
Number of bits of the biggest sum of numbers | 20 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.02 |
Number of variables | 2124 |
Total number of constraints | 612 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 168 |
Number of constraints which are nor clauses,nor cardinality constraints | 444 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 64 |
LAUNCH ON wulflinc22 THE 2005-09-20 04:44:25 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3404 boxname=wulflinc22 idbench=1060 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ec9e3281577e2d3f7b25c1cc88cac9ea /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-vpm1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-vpm1.opb IDLAUNCH: 3404 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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.031 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: 889212 kB Buffers: 12392 kB Cached: 106328 kB SwapCached: 552 kB Active: 16880 kB Inactive: 104464 kB HighTotal: 131008 kB HighFree: 23772 kB LowTotal: 903652 kB LowFree: 865440 kB SwapTotal: 2097892 kB SwapFree: 2096768 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5788 kB Slab: 18484 kB Committed_AS: 64300 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 05:04:35 (client local time) WITH STATUS 0 IN 1208.63 SECONDS stats: 3404 7 1208.63 0
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]---> Sorter-cost: 1988 Base: 2 2 2 5 5 2 2 2 2 2 3 c ---[ 264]---> Sorter-cost: 1824 Base: 2 2 2 5 5 2 2 2 3 2 2 2 c ---[ 260]---> Adder-cost: 262 maxlim: 300367 bits: 19/19 c ---[ 258]---> Adder-cost: 262 maxlim: 300367 bits: 19/19 c ---[ 256]---> Sorter-cost: 2565 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 254]---> Sorter-cost: 2565 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 252]---> Adder-cost: 262 maxlim: 261967 bits: 19/18 c ---[ 250]---> Sorter-cost: 1411 Base: 2 2 2 2 5 5 2 2 2 2 2 c ---[ 248]---> Sorter-cost: 2230 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 246]---> Sorter-cost: 2232 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 244]---> Sorter-cost: 2232 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 242]---> Sorter-cost: 2159 Base: 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[ 236]---> Sorter-cost: 1318 Base: 2 2 2 2 5 5 2 2 2 2 2 c ---[ 234]---> Sorter-cost: 2540 Base: 2 2 2 2 5 5 2 2 2 2 2 2 c ---[ 232]---> Sorter-cost: 1903 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 224]---> Sorter-cost: 1580 Base: 2 2 2 5 5 2 2 2 2 2 3 c ---[ 222]---> Adder-cost: 260 maxlim: 219983 bits: 19/18 c ---[ 216]---> Sorter-cost: 1742 Base: 2 2 2 5 5 2 2 2 2 2 2 c ---[ 214]---> Sorter-cost: 2471 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 212]---> Sorter-cost: 2473 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 210]---> Sorter-cost: 3095 Base: 2 2 2 2 2 3 5 2 2 2 5 c ---[ 208]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 206]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 204]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 202]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 200]---> Sorter-cost: 1882 Base: 2 2 2 2 5 5 2 2 2 5 c ---[ 198]---> Sorter-cost: 3211 Base: 2 2 2 2 5 5 2 2 2 2 5 c ---[ 196]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 194]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 192]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 191]---> BDD-cost: 33 c ---[ 190]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 c ---[ 189]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 c ---[ 188]---> Sorter-cost: 540 Base: 2 2 2 2 2 2 c ---[ 187]---> Sorter-cost: 761 Base: 2 2 2 2 2 2 c ---[ 186]---> Sorter-cost: 655 Base: 2 2 2 2 2 2 c ---[ 185]---> BDD-cost: 33 c ---[ 184]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 c ---[ 183]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 c ---[ 182]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 c ---[ 181]---> Sorter-cost: 707 Base: 2 2 2 2 2 2 c ---[ 180]---> Sorter-cost: 705 Base: 2 2 2 2 2 2 c ---[ 179]---> BDD-cost: 33 c ---[ 178]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 c ---[ 177]---> Sorter-cost: 274 Base: 2 2 2 2 2 2 c ---[ 176]---> Sorter-cost: 527 Base: 2 2 2 2 2 2 c ---[ 175]---> Sorter-cost: 720 Base: 2 2 2 2 2 2 c ---[ 174]---> Sorter-cost: 692 Base: 2 2 2 2 2 2 c ---[ 173]---> BDD-cost: 33 c ---[ 172]---> Sorter-cost: 253 Base: 2 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 274 Base: 2 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 486 Base: 2 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 695 Base: 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 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: 5 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: 6 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 | 144566 360910 | 48188 0 0 nan | 0.000 % | c | 100 | 144514 360784 | 53006 98 499 5.1 | 6.116 % | c | 251 | 144397 360518 | 58307 244 1686 6.9 | 6.175 % | c | 476 | 144397 360518 | 64138 469 3339 7.1 | 6.175 % | c | 813 | 144397 360518 | 70552 806 8685 10.8 | 6.175 % | c | 1319 | 144337 360381 | 77607 1311 24858 19.0 | 6.206 % | c | 2078 | 144191 360038 | 85367 2057 33401 16.2 | 6.281 % | c | 3218 | 143818 359196 | 93904 3178 50467 15.9 | 6.486 % | c | 4926 | 143287 357996 | 103295 4836 72661 15.0 | 6.777 % | c | 7488 | 143182 357750 | 113624 7385 155213 21.0 | 6.834 % | c | 11332 | 143082 357526 | 124987 11219 262443 23.4 | 6.886 % | c | 17098 | 142936 357200 | 137485 16976 448398 26.4 | 6.966 % | c | 25748 | 142359 355853 | 151234 25578 710280 27.8 | 7.281 % | c | 38722 | 142203 355504 | 166358 38542 1139672 29.6 | 7.368 % | c | 58183 | 141905 354826 | 182993 57975 1716418 29.6 | 7.528 % | c | 87377 | 141473 353854 | 201293 87113 2764142 31.7 | 7.764 % | c | 131169 | 140881 352461 | 221422 130846 4793681 36.6 | 8.089 % | c | 196854 | 140827 352341 | 243564 196515 8908564 45.3 | 8.122 % | c | 295381 | 139397 349113 | 267921 72533 2036665 28.1 | 8.941 % | c | 443170 | 138341 346669 | 294713 220188 7897187 35.9 | 9.552 % |
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/16662/stat): 16662 (minisat+_script) R 16661 16662 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855754514 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/16662/statm): 174 3 169 147 0 27 0 [pid=16662] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=16663 New process pid=16664 New process pid=16665 execve syscall for /bin/sed executable One traced child (pid=16664) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=16665) exited with status: 0 One traced child (pid=16663) exited with status: 0 New process pid=16666 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-vpm1.opb [startup+10.0038 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 4497 0 0 0 961 16 0 0 25 0 1 0 1855754519 19361792 4293 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 4727 4293 145 145 0 4582 0 [pid=16666] vsize: 18908 Current children cumulated CPU time (s) 9.78 Current children cumulated vsize (Kb) 21032 [startup+20.0055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 4858 0 0 0 1956 19 0 0 25 0 1 0 1855754519 20811776 4654 4294967295 134512640 135094434 3221224432 3221223056 134562095 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 5081 4654 145 145 0 4936 0 [pid=16666] vsize: 20324 Current children cumulated CPU time (s) 19.76 Current children cumulated vsize (Kb) 22448 [startup+30.0062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 5236 0 0 0 2949 21 0 0 25 0 1 0 1855754519 22388736 5032 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 5466 5032 145 145 0 5321 0 [pid=16666] vsize: 21864 Current children cumulated CPU time (s) 29.71 Current children cumulated vsize (Kb) 23988 [startup+40.0069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 5611 0 0 0 3944 24 0 0 25 0 1 0 1855754519 24018944 5407 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 5864 5407 145 145 0 5719 0 [pid=16666] vsize: 23456 Current children cumulated CPU time (s) 39.69 Current children cumulated vsize (Kb) 25580 [startup+50.0086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 5994 0 0 0 4936 28 0 0 25 0 1 0 1855754519 25554944 5790 4294967295 134512640 135094434 3221224432 3221223044 134563007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 6239 5790 145 145 0 6094 0 [pid=16666] vsize: 24956 Current children cumulated CPU time (s) 49.65 Current children cumulated vsize (Kb) 27080 [startup+60.0093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 6333 0 0 0 5932 30 0 0 25 0 1 0 1855754519 26923008 6129 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 6573 6129 145 145 0 6428 0 [pid=16666] vsize: 26292 Current children cumulated CPU time (s) 59.63 Current children cumulated vsize (Kb) 28416 [startup+70.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 6585 0 0 0 6927 33 0 0 25 0 1 0 1855754519 27922432 6381 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 6817 6381 145 145 0 6672 0 [pid=16666] vsize: 27268 Current children cumulated CPU time (s) 69.61 Current children cumulated vsize (Kb) 29392 [startup+80.0128 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 6955 0 0 0 7919 36 0 0 25 0 1 0 1855754519 29405184 6751 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 7179 6751 145 145 0 7034 0 [pid=16666] vsize: 28716 Current children cumulated CPU time (s) 79.56 Current children cumulated vsize (Kb) 30840 [startup+90.0135 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 7330 0 0 0 8911 39 0 0 25 0 1 0 1855754519 31182848 7126 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 7613 7126 145 145 0 7468 0 [pid=16666] vsize: 30452 Current children cumulated CPU time (s) 89.51 Current children cumulated vsize (Kb) 32576 [startup+100.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 7625 0 0 0 9906 42 0 0 25 0 1 0 1855754519 32358400 7421 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 7900 7421 145 145 0 7755 0 [pid=16666] vsize: 31600 Current children cumulated CPU time (s) 99.49 Current children cumulated vsize (Kb) 33724 [startup+110.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 7965 0 0 0 10898 45 0 0 25 0 1 0 1855754519 33726464 7761 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 8234 7761 145 145 0 8089 0 [pid=16666] vsize: 32936 Current children cumulated CPU time (s) 109.44 Current children cumulated vsize (Kb) 35060 [startup+120.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 8105 0 0 0 11896 47 0 0 25 0 1 0 1855754519 34295808 7901 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 8373 7901 145 145 0 8228 0 [pid=16666] vsize: 33492 Current children cumulated CPU time (s) 119.44 Current children cumulated vsize (Kb) 35616 [startup+130.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 8257 0 0 0 12894 48 0 0 25 0 1 0 1855754519 34906112 8053 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 8522 8053 145 145 0 8377 0 [pid=16666] vsize: 34088 Current children cumulated CPU time (s) 129.43 Current children cumulated vsize (Kb) 36212 [startup+140.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 8497 0 0 0 13889 49 0 0 25 0 1 0 1855754519 35872768 8293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 8758 8293 145 145 0 8613 0 [pid=16666] vsize: 35032 Current children cumulated CPU time (s) 139.39 Current children cumulated vsize (Kb) 37156 [startup+150.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 8806 0 0 0 14883 52 0 0 25 0 1 0 1855754519 37142528 8602 4294967295 134512640 135094434 3221224432 3221222944 134783376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 9068 8602 145 145 0 8923 0 [pid=16666] vsize: 36272 Current children cumulated CPU time (s) 149.36 Current children cumulated vsize (Kb) 38396 [startup+160.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 9047 0 0 0 15879 54 0 0 25 0 1 0 1855754519 38113280 8843 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 9305 8843 145 145 0 9160 0 [pid=16666] vsize: 37220 Current children cumulated CPU time (s) 159.34 Current children cumulated vsize (Kb) 39344 [startup+170.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 9421 0 0 0 16873 57 0 0 25 0 1 0 1855754519 39624704 9217 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 9674 9217 145 145 0 9529 0 [pid=16666] vsize: 38696 Current children cumulated CPU time (s) 169.31 Current children cumulated vsize (Kb) 40820 [startup+180.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 9852 0 0 0 17864 61 0 0 25 0 1 0 1855754519 41373696 9648 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 10101 9648 145 145 0 9956 0 [pid=16666] vsize: 40404 Current children cumulated CPU time (s) 179.26 Current children cumulated vsize (Kb) 42528 [startup+190.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 10417 0 0 0 18854 65 0 0 25 0 1 0 1855754519 43655168 10213 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 10658 10213 145 145 0 10513 0 [pid=16666] vsize: 42632 Current children cumulated CPU time (s) 189.2 Current children cumulated vsize (Kb) 44756 [startup+200.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 10790 0 0 0 19848 68 0 0 25 0 1 0 1855754519 45690880 10586 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 11155 10586 145 145 0 11010 0 [pid=16666] vsize: 44620 Current children cumulated CPU time (s) 199.17 Current children cumulated vsize (Kb) 46744 [startup+210.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 11112 0 0 0 20842 71 0 0 25 0 1 0 1855754519 46989312 10908 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 11472 10908 145 145 0 11327 0 [pid=16666] vsize: 45888 Current children cumulated CPU time (s) 209.14 Current children cumulated vsize (Kb) 48012 [startup+220.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 11409 0 0 0 21837 74 0 0 25 0 1 0 1855754519 48197632 11205 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 11767 11205 145 145 0 11622 0 [pid=16666] vsize: 47068 Current children cumulated CPU time (s) 219.12 Current children cumulated vsize (Kb) 49192 [startup+230.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 11680 0 0 0 22832 75 0 0 25 0 1 0 1855754519 49295360 11476 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 12035 11476 145 145 0 11890 0 [pid=16666] vsize: 48140 Current children cumulated CPU time (s) 229.08 Current children cumulated vsize (Kb) 50264 [startup+240.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 11946 0 0 0 23826 78 0 0 25 0 1 0 1855754519 50376704 11742 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 12299 11742 145 145 0 12154 0 [pid=16666] vsize: 49196 Current children cumulated CPU time (s) 239.05 Current children cumulated vsize (Kb) 51320 [startup+250.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 12180 0 0 0 24822 79 0 0 25 0 1 0 1855754519 51322880 11976 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 12530 11976 145 145 0 12385 0 [pid=16666] vsize: 50120 Current children cumulated CPU time (s) 249.02 Current children cumulated vsize (Kb) 52244 [startup+260.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 12411 0 0 0 25818 81 0 0 25 0 1 0 1855754519 52252672 12207 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 12757 12207 145 145 0 12612 0 [pid=16666] vsize: 51028 Current children cumulated CPU time (s) 259 Current children cumulated vsize (Kb) 53152 [startup+270.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 12666 0 0 0 26814 83 0 0 25 0 1 0 1855754519 53284864 12462 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 13009 12462 145 145 0 12864 0 [pid=16666] vsize: 52036 Current children cumulated CPU time (s) 268.98 Current children cumulated vsize (Kb) 54160 [startup+280.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 12901 0 0 0 27809 85 0 0 25 0 1 0 1855754519 54239232 12697 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 13242 12697 145 145 0 13097 0 [pid=16666] vsize: 52968 Current children cumulated CPU time (s) 278.95 Current children cumulated vsize (Kb) 55092 [startup+290.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13126 0 0 0 28805 87 0 0 25 0 1 0 1855754519 55160832 12922 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 13467 12922 145 145 0 13322 0 [pid=16666] vsize: 53868 Current children cumulated CPU time (s) 288.93 Current children cumulated vsize (Kb) 55992 [startup+300.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13376 0 0 0 29800 89 0 0 25 0 1 0 1855754519 56164352 13172 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 13712 13172 145 145 0 13567 0 [pid=16666] vsize: 54848 Current children cumulated CPU time (s) 298.9 Current children cumulated vsize (Kb) 56972 [startup+310.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13590 0 0 0 30795 91 0 0 25 0 1 0 1855754519 57032704 13386 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 13924 13386 145 145 0 13779 0 [pid=16666] vsize: 55696 Current children cumulated CPU time (s) 308.87 Current children cumulated vsize (Kb) 57820 [startup+320.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13772 0 0 0 31791 94 0 0 25 0 1 0 1855754519 57774080 13568 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 14105 13568 145 145 0 13960 0 [pid=16666] vsize: 56420 Current children cumulated CPU time (s) 318.86 Current children cumulated vsize (Kb) 58544 [startup+330.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 13952 0 0 0 32788 96 0 0 25 0 1 0 1855754519 58503168 13748 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 14283 13748 145 145 0 14138 0 [pid=16666] vsize: 57132 Current children cumulated CPU time (s) 328.85 Current children cumulated vsize (Kb) 59256 [startup+340.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14155 0 0 0 33783 98 0 0 25 0 1 0 1855754519 59346944 13951 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 14489 13951 145 145 0 14344 0 [pid=16666] vsize: 57956 Current children cumulated CPU time (s) 338.82 Current children cumulated vsize (Kb) 60080 [startup+350.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14366 0 0 0 34777 102 0 0 25 0 1 0 1855754519 60219392 14162 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 14702 14162 145 145 0 14557 0 [pid=16666] vsize: 58808 Current children cumulated CPU time (s) 348.8 Current children cumulated vsize (Kb) 60932 [startup+360.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14535 0 0 0 35774 103 0 0 25 0 1 0 1855754519 60923904 14331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 14874 14331 145 145 0 14729 0 [pid=16666] vsize: 59496 Current children cumulated CPU time (s) 358.78 Current children cumulated vsize (Kb) 61620 [startup+370.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14693 0 0 0 36771 105 0 0 25 0 1 0 1855754519 61587456 14489 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 15036 14489 145 145 0 14891 0 [pid=16666] vsize: 60144 Current children cumulated CPU time (s) 368.77 Current children cumulated vsize (Kb) 62268 [startup+380.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 14845 0 0 0 37768 106 0 0 25 0 1 0 1855754519 62189568 14641 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 15183 14641 145 145 0 15038 0 [pid=16666] vsize: 60732 Current children cumulated CPU time (s) 378.75 Current children cumulated vsize (Kb) 62856 [startup+390.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15079 0 0 0 38765 108 0 0 25 0 1 0 1855754519 63119360 14875 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 15410 14875 145 145 0 15265 0 [pid=16666] vsize: 61640 Current children cumulated CPU time (s) 388.74 Current children cumulated vsize (Kb) 63764 [startup+400.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15220 0 0 0 39762 110 0 0 25 0 1 0 1855754519 63692800 15016 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 15550 15016 145 145 0 15405 0 [pid=16666] vsize: 62200 Current children cumulated CPU time (s) 398.73 Current children cumulated vsize (Kb) 64324 [startup+410.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15374 0 0 0 40758 112 0 0 25 0 1 0 1855754519 64307200 15170 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 15700 15170 145 145 0 15555 0 [pid=16666] vsize: 62800 Current children cumulated CPU time (s) 408.71 Current children cumulated vsize (Kb) 64924 [startup+420.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15515 0 0 0 41756 112 0 0 25 0 1 0 1855754519 64872448 15311 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 15838 15311 145 145 0 15693 0 [pid=16666] vsize: 63352 Current children cumulated CPU time (s) 418.69 Current children cumulated vsize (Kb) 65476 [startup+430.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15681 0 0 0 42753 114 0 0 25 0 1 0 1855754519 65585152 15477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 16012 15477 145 145 0 15867 0 [pid=16666] vsize: 64048 Current children cumulated CPU time (s) 428.68 Current children cumulated vsize (Kb) 66172 [startup+440.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15823 0 0 0 43751 115 0 0 25 0 1 0 1855754519 66166784 15619 4294967295 134512640 135094434 3221224432 3221223056 134562092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 16154 15619 145 145 0 16009 0 [pid=16666] vsize: 64616 Current children cumulated CPU time (s) 438.67 Current children cumulated vsize (Kb) 66740 [startup+450.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 15956 0 0 0 44749 117 0 0 25 0 1 0 1855754519 66699264 15752 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 16284 15752 145 145 0 16139 0 [pid=16666] vsize: 65136 Current children cumulated CPU time (s) 448.67 Current children cumulated vsize (Kb) 67260 [startup+460.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16087 0 0 0 45746 119 0 0 25 0 1 0 1855754519 67223552 15883 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 16412 15883 145 145 0 16267 0 [pid=16666] vsize: 65648 Current children cumulated CPU time (s) 458.66 Current children cumulated vsize (Kb) 67772 [startup+470.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16201 0 0 0 46744 120 0 0 25 0 1 0 1855754519 67682304 15997 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 16524 15997 145 145 0 16379 0 [pid=16666] vsize: 66096 Current children cumulated CPU time (s) 468.65 Current children cumulated vsize (Kb) 68220 [startup+480.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16308 0 0 0 47742 120 0 0 25 0 1 0 1855754519 68104192 16104 4294967295 134512640 135094434 3221224432 3221223104 134556499 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 16627 16104 145 145 0 16482 0 [pid=16666] vsize: 66508 Current children cumulated CPU time (s) 478.63 Current children cumulated vsize (Kb) 68632 [startup+490.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16418 0 0 0 48740 122 0 0 25 0 1 0 1855754519 68571136 16214 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 16741 16214 145 145 0 16596 0 [pid=16666] vsize: 66964 Current children cumulated CPU time (s) 488.63 Current children cumulated vsize (Kb) 69088 [startup+500.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16545 0 0 0 49738 123 0 0 25 0 1 0 1855754519 69120000 16341 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 16875 16341 145 145 0 16730 0 [pid=16666] vsize: 67500 Current children cumulated CPU time (s) 498.62 Current children cumulated vsize (Kb) 69624 [startup+510.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16654 0 0 0 50735 125 0 0 25 0 1 0 1855754519 69566464 16450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 16984 16450 145 145 0 16839 0 [pid=16666] vsize: 67936 Current children cumulated CPU time (s) 508.61 Current children cumulated vsize (Kb) 70060 [startup+520.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16763 0 0 0 51733 125 0 0 25 0 1 0 1855754519 70000640 16559 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 17090 16559 145 145 0 16945 0 [pid=16666] vsize: 68360 Current children cumulated CPU time (s) 518.59 Current children cumulated vsize (Kb) 70484 [startup+530.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16868 0 0 0 52731 127 0 0 25 0 1 0 1855754519 70426624 16664 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 17194 16664 145 145 0 17049 0 [pid=16666] vsize: 68776 Current children cumulated CPU time (s) 528.59 Current children cumulated vsize (Kb) 70900 [startup+540.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 16971 0 0 0 53728 128 0 0 25 0 1 0 1855754519 70836224 16767 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 17294 16767 145 145 0 17149 0 [pid=16666] vsize: 69176 Current children cumulated CPU time (s) 538.57 Current children cumulated vsize (Kb) 71300 [startup+550.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17068 0 0 0 54727 129 0 0 25 0 1 0 1855754519 71225344 16864 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 17389 16864 145 145 0 17244 0 [pid=16666] vsize: 69556 Current children cumulated CPU time (s) 548.57 Current children cumulated vsize (Kb) 71680 [startup+560.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17193 0 0 0 55725 130 0 0 25 0 1 0 1855754519 71761920 16989 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 17520 16989 145 145 0 17375 0 [pid=16666] vsize: 70080 Current children cumulated CPU time (s) 558.56 Current children cumulated vsize (Kb) 72204 [startup+570.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17337 0 0 0 56721 132 0 0 25 0 1 0 1855754519 72335360 17133 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 17660 17133 145 145 0 17515 0 [pid=16666] vsize: 70640 Current children cumulated CPU time (s) 568.54 Current children cumulated vsize (Kb) 72764 [startup+580.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17495 0 0 0 57718 133 0 0 25 0 1 0 1855754519 73011200 17291 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 17825 17291 145 145 0 17680 0 [pid=16666] vsize: 71300 Current children cumulated CPU time (s) 578.52 Current children cumulated vsize (Kb) 73424 [startup+590.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17615 0 0 0 58716 134 0 0 25 0 1 0 1855754519 73494528 17411 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 17943 17411 145 145 0 17798 0 [pid=16666] vsize: 71772 Current children cumulated CPU time (s) 588.51 Current children cumulated vsize (Kb) 73896 [startup+600.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17773 0 0 0 59714 135 0 0 25 0 1 0 1855754519 74121216 17569 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18096 17569 145 145 0 17951 0 [pid=16666] vsize: 72384 Current children cumulated CPU time (s) 598.5 Current children cumulated vsize (Kb) 74508 [startup+610.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 17881 0 0 0 60712 137 0 0 25 0 1 0 1855754519 74551296 17677 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18201 17677 145 145 0 18056 0 [pid=16666] vsize: 72804 Current children cumulated CPU time (s) 608.5 Current children cumulated vsize (Kb) 74928 [startup+620.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18026 0 0 0 61711 137 0 0 25 0 1 0 1855754519 75161600 17822 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18350 17822 145 145 0 18205 0 [pid=16666] vsize: 73400 Current children cumulated CPU time (s) 618.49 Current children cumulated vsize (Kb) 75524 [startup+630.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18200 0 0 0 62709 138 0 0 25 0 1 0 1855754519 75870208 17996 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18523 17996 145 145 0 18378 0 [pid=16666] vsize: 74092 Current children cumulated CPU time (s) 628.48 Current children cumulated vsize (Kb) 76216 [startup+640.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 63707 139 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 638.47 Current children cumulated vsize (Kb) 76408 [startup+650.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 64707 140 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 648.48 Current children cumulated vsize (Kb) 76408 [startup+660.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 65707 140 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 658.48 Current children cumulated vsize (Kb) 76408 [startup+670.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 66707 140 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 668.48 Current children cumulated vsize (Kb) 76408 [startup+680.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 67706 141 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 678.48 Current children cumulated vsize (Kb) 76408 [startup+690.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 68706 142 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 688.49 Current children cumulated vsize (Kb) 76408 [startup+700.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 69705 142 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 698.48 Current children cumulated vsize (Kb) 76408 [startup+710.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18249 0 0 0 70704 143 0 0 25 0 1 0 1855754519 76066816 18045 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18571 18045 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 708.48 Current children cumulated vsize (Kb) 76408 [startup+720.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18250 0 0 0 71704 143 0 0 25 0 1 0 1855754519 76066816 18046 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16666/statm): 18571 18046 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 718.48 Current children cumulated vsize (Kb) 76408 [startup+730.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18250 0 0 0 72704 143 0 0 25 0 1 0 1855754519 76066816 18046 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18046 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 728.48 Current children cumulated vsize (Kb) 76408 [startup+740.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18250 0 0 0 73704 143 0 0 25 0 1 0 1855754519 76066816 18046 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18046 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 738.48 Current children cumulated vsize (Kb) 76408 [startup+750.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18250 0 0 0 74705 143 0 0 25 0 1 0 1855754519 76066816 18046 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18046 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 748.49 Current children cumulated vsize (Kb) 76408 [startup+760.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 75705 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 758.49 Current children cumulated vsize (Kb) 76408 [startup+770.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 76705 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 768.49 Current children cumulated vsize (Kb) 76408 [startup+780.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 77706 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 778.5 Current children cumulated vsize (Kb) 76408 [startup+790.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 78706 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 788.5 Current children cumulated vsize (Kb) 76408 [startup+800.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 79706 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 798.5 Current children cumulated vsize (Kb) 76408 [startup+810.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18252 0 0 0 80706 143 0 0 25 0 1 0 1855754519 76066816 18048 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18048 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 808.5 Current children cumulated vsize (Kb) 76408 [startup+820.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18253 0 0 0 81706 143 0 0 25 0 1 0 1855754519 76066816 18049 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18049 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 818.5 Current children cumulated vsize (Kb) 76408 [startup+830.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18254 0 0 0 82707 143 0 0 25 0 1 0 1855754519 76066816 18050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18571 18050 145 145 0 18426 0 [pid=16666] vsize: 74284 Current children cumulated CPU time (s) 828.51 Current children cumulated vsize (Kb) 76408 [startup+840.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18265 0 0 0 83707 143 0 0 25 0 1 0 1855754519 76132352 18061 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18587 18061 145 145 0 18442 0 [pid=16666] vsize: 74348 Current children cumulated CPU time (s) 838.51 Current children cumulated vsize (Kb) 76472 [startup+850.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18278 0 0 0 84707 143 0 0 25 0 1 0 1855754519 76197888 18074 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18603 18074 145 145 0 18458 0 [pid=16666] vsize: 74412 Current children cumulated CPU time (s) 848.51 Current children cumulated vsize (Kb) 76536 [startup+860.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18279 0 0 0 85707 143 0 0 25 0 1 0 1855754519 76197888 18075 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18603 18075 145 145 0 18458 0 [pid=16666] vsize: 74412 Current children cumulated CPU time (s) 858.51 Current children cumulated vsize (Kb) 76536 [startup+870.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18280 0 0 0 86708 143 0 0 25 0 1 0 1855754519 76197888 18076 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18603 18076 145 145 0 18458 0 [pid=16666] vsize: 74412 Current children cumulated CPU time (s) 868.52 Current children cumulated vsize (Kb) 76536 [startup+880.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 87708 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 878.52 Current children cumulated vsize (Kb) 76600 [startup+890.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 88708 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 888.52 Current children cumulated vsize (Kb) 76600 [startup+900.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 89708 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 898.52 Current children cumulated vsize (Kb) 76600 [startup+910.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 90709 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 908.53 Current children cumulated vsize (Kb) 76600 [startup+920.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 91709 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 918.53 Current children cumulated vsize (Kb) 76600 [startup+930.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18290 0 0 0 92709 143 0 0 25 0 1 0 1855754519 76263424 18086 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18086 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 928.53 Current children cumulated vsize (Kb) 76600 [startup+940.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18292 0 0 0 93709 143 0 0 25 0 1 0 1855754519 76263424 18088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18088 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 938.53 Current children cumulated vsize (Kb) 76600 [startup+950.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 94710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 948.54 Current children cumulated vsize (Kb) 76600 [startup+960.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 95710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223104 134556549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 958.54 Current children cumulated vsize (Kb) 76600 [startup+970.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 96710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 968.54 Current children cumulated vsize (Kb) 76600 [startup+980.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 97710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 978.54 Current children cumulated vsize (Kb) 76600 [startup+990.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 98710 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 988.54 Current children cumulated vsize (Kb) 76600 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 99711 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 998.55 Current children cumulated vsize (Kb) 76600 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 100711 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 1008.55 Current children cumulated vsize (Kb) 76600 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 101711 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 1018.55 Current children cumulated vsize (Kb) 76600 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 102711 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 1028.55 Current children cumulated vsize (Kb) 76600 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18293 0 0 0 103712 143 0 0 25 0 1 0 1855754519 76263424 18089 4294967295 134512640 135094434 3221224432 3221223104 134555957 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18089 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 1038.56 Current children cumulated vsize (Kb) 76600 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18294 0 0 0 104711 143 0 0 25 0 1 0 1855754519 76263424 18090 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18619 18090 145 145 0 18474 0 [pid=16666] vsize: 74476 Current children cumulated CPU time (s) 1048.55 Current children cumulated vsize (Kb) 76600 [startup+1060.1 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18313 0 0 0 105711 143 0 0 25 0 1 0 1855754519 76328960 18109 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18635 18109 145 145 0 18490 0 [pid=16666] vsize: 74540 Current children cumulated CPU time (s) 1058.55 Current children cumulated vsize (Kb) 76664 [startup+1070.1 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18316 0 0 0 106712 143 0 0 25 0 1 0 1855754519 76328960 18112 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18635 18112 145 145 0 18490 0 [pid=16666] vsize: 74540 Current children cumulated CPU time (s) 1068.56 Current children cumulated vsize (Kb) 76664 [startup+1080.1 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18316 0 0 0 107712 143 0 0 25 0 1 0 1855754519 76328960 18112 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18635 18112 145 145 0 18490 0 [pid=16666] vsize: 74540 Current children cumulated CPU time (s) 1078.56 Current children cumulated vsize (Kb) 76664 [startup+1090.1 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18328 0 0 0 108712 143 0 0 25 0 1 0 1855754519 76394496 18124 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18124 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1088.56 Current children cumulated vsize (Kb) 76728 [startup+1100.11 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 109712 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1098.56 Current children cumulated vsize (Kb) 76728 [startup+1110.11 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 110713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1108.57 Current children cumulated vsize (Kb) 76728 [startup+1120.11 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 111713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1118.57 Current children cumulated vsize (Kb) 76728 [startup+1130.11 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 112713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1128.57 Current children cumulated vsize (Kb) 76728 [startup+1140.11 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 113713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1138.57 Current children cumulated vsize (Kb) 76728 [startup+1150.11 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 114713 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1148.57 Current children cumulated vsize (Kb) 76728 [startup+1160.11 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18331 0 0 0 115714 143 0 0 25 0 1 0 1855754519 76394496 18127 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18127 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1158.58 Current children cumulated vsize (Kb) 76728 [startup+1170.11 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18333 0 0 0 116714 143 0 0 25 0 1 0 1855754519 76394496 18129 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18129 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1168.58 Current children cumulated vsize (Kb) 76728 [startup+1180.11 s] Raw data (loadavg): 1.09 1.00 0.92 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18336 0 0 0 117714 143 0 0 25 0 1 0 1855754519 76394496 18132 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18132 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1178.58 Current children cumulated vsize (Kb) 76728 [startup+1190.11 s] Raw data (loadavg): 1.07 1.00 0.92 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18338 0 0 0 118714 143 0 0 25 0 1 0 1855754519 76394496 18134 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18134 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1188.58 Current children cumulated vsize (Kb) 76728 [startup+1200.11 s] Raw data (loadavg): 1.06 1.00 0.92 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18341 0 0 0 119715 143 0 0 25 0 1 0 1855754519 76394496 18137 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18651 18137 145 145 0 18506 0 [pid=16666] vsize: 74604 Current children cumulated CPU time (s) 1198.59 Current children cumulated vsize (Kb) 76728 [startup+1210.11 s] Raw data (loadavg): 1.05 1.00 0.92 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18344 0 0 0 120715 143 0 0 25 0 1 0 1855754519 77443072 18140 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18907 18140 145 145 0 18762 0 [pid=16666] vsize: 75628 Current children cumulated CPU time (s) 1208.59 Current children cumulated vsize (Kb) 77752 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.05 1.00 0.92 2/57 16666 Raw data (/proc/16662/stat): 16662 (minisat+_script) S 16661 16662 21452 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855754514 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16662/statm): 531 226 485 147 0 384 0 [pid=16662] vsize: 2124 Raw data (/proc/16666/stat): 16666 (minisat+_64-bit) R 16662 16662 21452 0 -1 0 18344 0 0 0 120715 143 0 0 25 0 1 0 1855754519 77443072 18140 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16666/statm): 18907 18140 145 145 0 18762 0 [pid=16666] vsize: 75628 Current children cumulated CPU time (s) 1208.59 Current children cumulated vsize (Kb) 77752 Sending SIGTERM to -16662 Sleeping 2 seconds One traced child (pid=16662) ended because it received signal 15 (SIGTERM) One traced child (pid=16666) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.15 CPU time (s): 1208.63 CPU user time (s): 1207.15 CPU system time (s): 1.47178 CPU usage (%): 99.874 Max. virtual memory (cumulated for all children) (Kb): 77752
ERROR: no interpretation found !