Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-vpm2.opb |
MD5SUM | 8c44064d4224b1d41c28f152218dd39f |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 121 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 168 |
Biggest coefficient in the objective function | 5 |
Number of bits for the biggest coefficient in the objective function | 3 |
Sum of the numbers in the objective function | 504 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 102400 |
Number of bits of the biggest number in a constraint | 17 |
Biggest sum of numbers in a constraint | 615983 |
Number of bits of the biggest sum of numbers | 20 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 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 wulflinc5 THE 2005-09-20 04:04:11 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3335 boxname=wulflinc5 idbench=991 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 8c44064d4224b1d41c28f152218dd39f /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-vpm2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-vpm2.opb IDLAUNCH: 3335 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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: 913072 kB Buffers: 8176 kB Cached: 89068 kB SwapCached: 744 kB Active: 25080 kB Inactive: 74852 kB HighTotal: 131008 kB HighFree: 37716 kB LowTotal: 903652 kB LowFree: 875356 kB SwapTotal: 2097136 kB SwapFree: 2095884 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5756 kB Slab: 16024 kB Committed_AS: 64264 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:24:23 (client local time) WITH STATUS 0 IN 1206.25 SECONDS stats: 3335 7 1206.25 0
c Parsing PB file... c Converting 486 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################## c -- Clauses(.)/Splits(s): (none) c ---[ 485]---> BDD-cost: 7 c ---[ 484]---> BDD-cost: 7 c ---[ 483]---> BDD-cost: 7 c ---[ 482]---> BDD-cost: 7 c ---[ 481]---> BDD-cost: 7 c ---[ 480]---> BDD-cost: 7 c ---[ 479]---> BDD-cost: 7 c ---[ 478]---> BDD-cost: 7 c ---[ 477]---> BDD-cost: 7 c ---[ 474]---> BDD-cost: 7 c ---[ 473]---> BDD-cost: 7 c ---[ 472]---> BDD-cost: 7 c ---[ 471]---> BDD-cost: 7 c ---[ 468]---> BDD-cost: 7 c ---[ 467]---> BDD-cost: 7 c ---[ 466]---> BDD-cost: 7 c ---[ 465]---> BDD-cost: 7 c ---[ 462]---> BDD-cost: 7 c ---[ 459]---> BDD-cost: 7 c ---[ 458]---> BDD-cost: 7 c ---[ 457]---> BDD-cost: 7 c ---[ 454]---> BDD-cost: 7 c ---[ 453]---> BDD-cost: 7 c ---[ 452]---> BDD-cost: 7 c ---[ 451]---> BDD-cost: 7 c ---[ 450]---> BDD-cost: 7 c ---[ 448]---> BDD-cost: 7 c ---[ 447]---> BDD-cost: 7 c ---[ 446]---> BDD-cost: 7 c ---[ 445]---> BDD-cost: 7 c ---[ 444]---> BDD-cost: 7 c ---[ 441]---> BDD-cost: 7 c ---[ 440]---> BDD-cost: 7 c ---[ 439]---> BDD-cost: 7 c ---[ 433]---> BDD-cost: 7 c ---[ 427]---> BDD-cost: 7 c ---[ 422]---> BDD-cost: 7 c ---[ 421]---> BDD-cost: 7 c ---[ 415]---> BDD-cost: 7 c ---[ 409]---> BDD-cost: 7 c ---[ 408]---> BDD-cost: 7 c ---[ 402]---> BDD-cost: 7 c ---[ 397]---> BDD-cost: 7 c ---[ 396]---> BDD-cost: 7 c ---[ 391]---> BDD-cost: 7 c ---[ 390]---> BDD-cost: 7 c ---[ 386]---> BDD-cost: 7 c ---[ 385]---> BDD-cost: 7 c ---[ 384]---> BDD-cost: 7 c ---[ 380]---> BDD-cost: 7 c ---[ 379]---> BDD-cost: 7 c ---[ 378]---> BDD-cost: 7 c ---[ 374]---> BDD-cost: 7 c ---[ 373]---> BDD-cost: 7 c ---[ 372]---> BDD-cost: 7 c ---[ 368]---> BDD-cost: 7 c ---[ 367]---> BDD-cost: 7 c ---[ 366]---> BDD-cost: 7 c ---[ 365]---> BDD-cost: 7 c ---[ 364]---> BDD-cost: 7 c ---[ 359]---> BDD-cost: 7 c ---[ 353]---> BDD-cost: 7 c ---[ 347]---> BDD-cost: 7 c ---[ 339]---> BDD-cost: 7 c ---[ 333]---> BDD-cost: 7 c ---[ 327]---> BDD-cost: 7 c ---[ 321]---> BDD-cost: 7 c ---[ 317]---> BDD-cost: 14 c ---[ 316]---> BDD-cost: 14 c ---[ 315]---> BDD-cost: 14 c ---[ 314]---> BDD-cost: 14 c ---[ 313]---> BDD-cost: 14 c ---[ 312]---> BDD-cost: 14 c ---[ 310]---> BDD-cost: 14 c ---[ 309]---> BDD-cost: 14 c ---[ 308]---> BDD-cost: 14 c ---[ 307]---> BDD-cost: 14 c ---[ 306]---> BDD-cost: 14 c ---[ 302]---> BDD-cost: 13 c ---[ 301]---> BDD-cost: 13 c ---[ 300]---> BDD-cost: 13 c ---[ 295]---> BDD-cost: 13 c ---[ 294]---> BDD-cost: 13 c ---[ 290]---> BDD-cost: 15 c ---[ 289]---> BDD-cost: 15 c ---[ 288]---> BDD-cost: 15 c ---[ 287]---> BDD-cost: 13 c ---[ 286]---> BDD-cost: 13 c ---[ 285]---> BDD-cost: 13 c ---[ 284]---> BDD-cost: 13 c ---[ 283]---> BDD-cost: 13 c ---[ 282]---> BDD-cost: 13 c ---[ 280]---> BDD-cost: 13 c ---[ 279]---> BDD-cost: 13 c ---[ 278]---> BDD-cost: 13 c ---[ 277]---> BDD-cost: 13 c ---[ 276]---> BDD-cost: 13 c ---[ 274]---> Adder-cost: 262 maxlim: 300367 bits: 19/19 c ---[ 272]---> Sorter-cost: 2159 Base: 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[ 271]---> BDD-cost: 3 c ---[ 270]---> BDD-cost: 3 c ---[ 269]---> BDD-cost: 3 c ---[ 267]---> BDD-cost: 3 c ---[ 266]---> BDD-cost: 3 c ---[ 265]---> BDD-cost: 3 c ---[ 264]---> BDD-cost: 3 c ---[ 263]---> BDD-cost: 3 c ---[ 259]---> BDD-cost: 7 c ---[ 258]---> BDD-cost: 3 c ---[ 257]---> BDD-cost: 3 c ---[ 256]---> BDD-cost: 3 c ---[ 255]---> BDD-cost: 7 c ---[ 251]---> BDD-cost: 7 c ---[ 250]---> BDD-cost: 3 c ---[ 247]---> BDD-cost: 6 c ---[ 243]---> BDD-cost: 7 c ---[ 242]---> BDD-cost: 3 c ---[ 241]---> BDD-cost: 6 c ---[ 236]---> Sorter-cost: 1318 Base: 2 2 2 2 5 5 2 2 2 2 2 c ---[ 235]---> BDD-cost: 3 c ---[ 234]---> BDD-cost: 3 c ---[ 233]---> BDD-cost: 6 c ---[ 229]---> BDD-cost: 7 c ---[ 228]---> BDD-cost: 3 c ---[ 227]---> BDD-cost: 6 c ---[ 224]---> Sorter-cost: 2540 Base: 2 2 2 2 5 5 2 2 2 2 2 2 c ---[ 220]---> BDD-cost: 3 c ---[ 219]---> BDD-cost: 3 c ---[ 214]---> BDD-cost: 7 c ---[ 212]---> Sorter-cost: 1902 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 211]---> BDD-cost: 3 c ---[ 206]---> BDD-cost: 3 c ---[ 205]---> BDD-cost: 3 c ---[ 198]---> BDD-cost: 3 c ---[ 197]---> BDD-cost: 3 c ---[ 193]---> BDD-cost: 3 c ---[ 192]---> BDD-cost: 3 c ---[ 191]---> BDD-cost: 3 c ---[ 185]---> BDD-cost: 3 c ---[ 184]---> BDD-cost: 3 c ---[ 183]---> BDD-cost: 3 c ---[ 179]---> BDD-cost: 3 c ---[ 178]---> BDD-cost: 3 c ---[ 175]---> BDD-cost: 3 c ---[ 171]---> BDD-cost: 3 c ---[ 170]---> BDD-cost: 3 c ---[ 169]---> BDD-cost: 3 c ---[ 168]---> BDD-cost: 3 c ---[ 167]---> BDD-cost: 3 c ---[ 166]---> BDD-cost: 6 c ---[ 164]---> Sorter-cost: 1580 Base: 2 2 2 5 5 2 2 2 2 2 3 c ---[ 163]---> BDD-cost: 6 c ---[ 162]---> BDD-cost: 6 c ---[ 161]---> BDD-cost: 6 c ---[ 160]---> BDD-cost: 3 c ---[ 159]---> BDD-cost: 7 c ---[ 158]---> BDD-cost: 6 c ---[ 157]---> BDD-cost: 6 c ---[ 156]---> BDD-cost: 6 c ---[ 155]---> BDD-cost: 6 c ---[ 154]---> BDD-cost: 3 c ---[ 152]---> Adder-cost: 262 maxlim: 300367 bits: 19/19 c ---[ 150]---> Adder-cost: 260 maxlim: 219983 bits: 19/18 c ---[ 149]---> BDD-cost: 7 c ---[ 148]---> BDD-cost: 5 c ---[ 147]---> BDD-cost: 5 c ---[ 146]---> BDD-cost: 5 c ---[ 145]---> BDD-cost: 5 c ---[ 144]---> BDD-cost: 3 c ---[ 143]---> BDD-cost: 7 c ---[ 142]---> BDD-cost: 5 c ---[ 141]---> BDD-cost: 5 c ---[ 140]---> BDD-cost: 5 c ---[ 137]---> BDD-cost: 5 c ---[ 135]---> BDD-cost: 7 c ---[ 134]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 6 c ---[ 132]---> BDD-cost: 6 c ---[ 131]---> BDD-cost: 6 c ---[ 129]---> BDD-cost: 7 c ---[ 128]---> BDD-cost: 3 c ---[ 125]---> BDD-cost: 6 c ---[ 124]---> BDD-cost: 6 c ---[ 123]---> BDD-cost: 6 c ---[ 121]---> BDD-cost: 7 c ---[ 120]---> BDD-cost: 3 c ---[ 119]---> BDD-cost: 6 c ---[ 118]---> BDD-cost: 6 c ---[ 117]---> BDD-cost: 6 c ---[ 114]---> Sorter-cost: 1742 Base: 2 2 2 5 5 2 2 2 2 2 2 c ---[ 113]---> BDD-cost: 7 c ---[ 112]---> BDD-cost: 3 c ---[ 111]---> BDD-cost: 5 c ---[ 110]---> BDD-cost: 5 c ---[ 109]---> BDD-cost: 5 c ---[ 107]---> Sorter-cost: 2471 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 105]---> Sorter-cost: 2473 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 103]---> Sorter-cost: 3095 Base: 2 2 2 2 2 3 5 2 2 2 5 c ---[ 101]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 99]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 97]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 95]---> Sorter-cost: 2565 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 93]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 91]---> Sorter-cost: 1881 Base: 2 2 2 2 5 5 2 2 2 5 c ---[ 89]---> Sorter-cost: 3211 Base: 2 2 2 2 5 5 2 2 2 2 5 c ---[ 87]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 85]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 83]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 81]---> Sorter-cost: 1988 Base: 2 2 2 5 5 2 2 2 2 2 3 c ---[ 73]---> Sorter-cost: 2565 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 69]---> Sorter-cost: 1824 Base: 2 2 2 5 5 2 2 2 3 2 2 2 c ---[ 66]---> BDD-cost: 136 c ---[ 65]---> BDD-cost: 283 c ---[ 64]---> BDD-cost: 282 c ---[ 63]---> BDD-cost: 470 c ---[ 62]---> BDD-cost: 579 c ---[ 61]---> BDD-cost: 572 c ---[ 60]---> Sorter-cost: 303 Base: 2 2 2 2 2 5 2 c ---[ 58]---> Adder-cost: 262 maxlim: 261967 bits: 19/18 c ---[ 57]---> Sorter-cost: 801 Base: 2 2 2 2 2 5 2 c ---[ 56]---> Sorter-cost: 819 Base: 2 2 2 2 2 5 2 c ---[ 55]---> Sorter-cost: 1035 Base: 5 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 1285 Base: 5 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 1289 Base: 5 2 2 2 2 2 2 c ---[ 52]---> Sorter-cost: 335 Base: 2 2 2 2 2 2 5 c ---[ 51]---> Sorter-cost: 867 Base: 2 2 5 2 2 2 2 c ---[ 50]---> Sorter-cost: 830 Base: 2 2 2 2 2 2 5 c ---[ 49]---> Sorter-cost: 1298 Base: 2 2 5 2 2 2 2 c ---[ 48]---> Sorter-cost: 1687 Base: 2 2 5 2 2 2 2 c ---[ 46]---> Sorter-cost: 1411 Base: 2 2 2 2 5 5 2 2 2 2 2 c ---[ 45]---> Sorter-cost: 1665 Base: 2 2 5 2 2 2 2 c ---[ 44]---> Sorter-cost: 196 Base: 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 473 Base: 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 421 Base: 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 764 Base: 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 884 Base: 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 1063 Base: 2 2 2 2 2 c ---[ 38]---> BDD-cost: 3 c ---[ 37]---> BDD-cost: 3 c ---[ 36]---> BDD-cost: 3 c ---[ 34]---> Sorter-cost: 2230 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 33]---> BDD-cost: 3 c ---[ 32]---> BDD-cost: 3 c ---[ 31]---> BDD-cost: 3 c ---[ 30]---> BDD-cost: 3 c ---[ 29]---> BDD-cost: 3 c ---[ 28]---> BDD-cost: 3 c ---[ 27]---> BDD-cost: 7 c ---[ 26]---> BDD-cost: 7 c ---[ 25]---> BDD-cost: 3 c ---[ 24]---> BDD-cost: 3 c ---[ 22]---> Sorter-cost: 2232 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 3 c ---[ 19]---> BDD-cost: 7 c ---[ 18]---> BDD-cost: 7 c ---[ 17]---> BDD-cost: 3 c ---[ 16]---> BDD-cost: 3 c ---[ 15]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 3 c ---[ 13]---> BDD-cost: 7 c ---[ 12]---> BDD-cost: 7 c ---[ 10]---> Sorter-cost: 2232 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 9]---> BDD-cost: 3 c ---[ 7]---> BDD-cost: 7 c ---[ 6]---> BDD-cost: 3 c ---[ 5]---> BDD-cost: 3 c ---[ 4]---> BDD-cost: 3 c ---[ 3]---> BDD-cost: 7 c ---[ 1]---> BDD-cost: 3 c ---[ 0]---> BDD-cost: 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 165694 413657 | 55231 0 0 nan | 0.000 % | c | 102 | 165616 413479 | 60754 99 1459 14.7 | 5.324 % | c | 252 | 165375 412930 | 66829 245 2721 11.1 | 5.428 % | c | 477 | 165357 412890 | 73512 469 6101 13.0 | 5.437 % | c | 814 | 165188 412504 | 80863 802 9398 11.7 | 5.516 % | c | 1320 | 164865 411746 | 88950 1267 13983 11.0 | 5.666 % | c | 2079 | 163978 409703 | 97845 1922 20743 10.8 | 6.104 % | c | 3218 | 163801 409297 | 107629 3060 52624 17.2 | 6.187 % | c | 4927 | 163739 409157 | 118392 4765 111807 23.5 | 6.219 % | c | 7493 | 163484 408561 | 130231 7305 169316 23.2 | 6.337 % | c | 11340 | 163364 408284 | 143254 11146 339381 30.4 | 6.392 % | c | 17107 | 162493 406293 | 157580 16863 525197 31.1 | 6.813 % | c | 25759 | 162097 405354 | 173338 25483 778910 30.6 | 7.013 % | c | 38733 | 161410 403789 | 190672 38387 1212692 31.6 | 7.343 % | c | 58194 | 160811 402413 | 209739 57805 2041019 35.3 | 7.645 % | c | 87386 | 159402 399021 | 230713 85832 3126290 36.4 | 8.285 % | c | 131175 | 158653 397316 | 253784 129543 4806879 37.1 | 8.645 % | c | 196859 | 157962 395566 | 279163 195169 6798047 34.8 | 8.947 % | c | 295386 | 157436 394369 | 307079 38965 1023168 26.3 | 9.228 % |
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/25192/stat): 25192 (minisat+_script) R 25191 25192 824 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797290153 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/25192/statm): 174 3 169 147 0 27 0 [pid=25192] 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=25193 New process pid=25194 New process pid=25195 execve syscall for /bin/sed executable One traced child (pid=25194) 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=25195) exited with status: 0 One traced child (pid=25193) exited with status: 0 New process pid=25196 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-vpm2.opb [startup+10.0037 s] Raw data (loadavg): 0.93 0.98 0.97 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5011 0 0 0 958 17 0 0 25 0 1 0 1797290158 22478848 4818 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 5488 4818 145 145 0 5343 0 [pid=25196] vsize: 21952 Current children cumulated CPU time (s) 9.75 Current children cumulated vsize (Kb) 24076 [startup+20.0055 s] Raw data (loadavg): 0.94 0.98 0.97 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5240 0 0 0 1953 19 0 0 25 0 1 0 1797290158 23420928 5047 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25196/statm): 5718 5047 145 145 0 5573 0 [pid=25196] vsize: 22872 Current children cumulated CPU time (s) 19.72 Current children cumulated vsize (Kb) 24996 [startup+31.2863 s] Raw data (loadavg): 1.03 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) T 25192 25192 824 0 -1 0 5408 0 0 0 2710 20 0 0 25 0 1 0 1797290158 24096768 5215 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/25196/statm): 5883 5215 145 145 0 5738 0 [pid=25196] vsize: 23532 Current children cumulated CPU time (s) 27.3 Current children cumulated vsize (Kb) 25656 [startup+41.2876 s] Raw data (loadavg): 1.03 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5604 0 0 0 3707 21 0 0 25 0 1 0 1797290158 24936448 5411 4294967295 134512640 135094434 3221224448 3221223120 134555413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 6088 5411 145 145 0 5943 0 [pid=25196] vsize: 24352 Current children cumulated CPU time (s) 37.28 Current children cumulated vsize (Kb) 26476 [startup+51.2883 s] Raw data (loadavg): 1.02 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5802 0 0 0 4703 22 0 0 25 0 1 0 1797290158 25726976 5609 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 6281 5609 145 145 0 6136 0 [pid=25196] vsize: 25124 Current children cumulated CPU time (s) 47.25 Current children cumulated vsize (Kb) 27248 [startup+61.2881 s] Raw data (loadavg): 1.02 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5993 0 0 0 5698 24 0 0 25 0 1 0 1797290158 26488832 5800 4294967295 134512640 135094434 3221224448 3221223072 134557642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25196/statm): 6467 5800 145 145 0 6322 0 [pid=25196] vsize: 25868 Current children cumulated CPU time (s) 57.22 Current children cumulated vsize (Kb) 27992 [startup+71.2898 s] Raw data (loadavg): 1.02 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 6180 0 0 0 6695 26 0 0 25 0 1 0 1797290158 27238400 5987 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 6650 5987 145 145 0 6505 0 [pid=25196] vsize: 26600 Current children cumulated CPU time (s) 67.21 Current children cumulated vsize (Kb) 28724 [startup+81.2905 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 6359 0 0 0 7692 28 0 0 25 0 1 0 1797290158 28090368 6166 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 6858 6166 145 145 0 6713 0 [pid=25196] vsize: 27432 Current children cumulated CPU time (s) 77.2 Current children cumulated vsize (Kb) 29556 [startup+91.2913 s] Raw data (loadavg): 1.01 1.00 0.98 3/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 6537 0 0 0 8689 30 0 0 25 0 1 0 1797290158 28803072 6344 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 7032 6344 145 145 0 6887 0 [pid=25196] vsize: 28128 Current children cumulated CPU time (s) 87.19 Current children cumulated vsize (Kb) 30252 [startup+101.292 s] Raw data (loadavg): 1.01 1.00 0.98 3/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7083 0 0 0 9681 33 0 0 25 0 1 0 1797290158 31002624 6890 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 7569 6890 145 145 0 7424 0 [pid=25196] vsize: 30276 Current children cumulated CPU time (s) 97.14 Current children cumulated vsize (Kb) 32400 [startup+111.293 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7265 0 0 0 10679 34 0 0 25 0 1 0 1797290158 31719424 7072 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 7744 7072 145 145 0 7599 0 [pid=25196] vsize: 30976 Current children cumulated CPU time (s) 107.13 Current children cumulated vsize (Kb) 33100 [startup+121.293 s] Raw data (loadavg): 1.01 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7535 0 0 0 11674 36 0 0 25 0 1 0 1797290158 32796672 7342 4294967295 134512640 135094434 3221224448 3221223060 134563061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 8007 7342 145 145 0 7862 0 [pid=25196] vsize: 32028 Current children cumulated CPU time (s) 117.1 Current children cumulated vsize (Kb) 34152 [startup+131.294 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7656 0 0 0 12672 37 0 0 25 0 1 0 1797290158 33284096 7463 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 8126 7463 145 145 0 7981 0 [pid=25196] vsize: 32504 Current children cumulated CPU time (s) 127.09 Current children cumulated vsize (Kb) 34628 [startup+141.296 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7841 0 0 0 13669 38 0 0 25 0 1 0 1797290158 34021376 7648 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 8306 7648 145 145 0 8161 0 [pid=25196] vsize: 33224 Current children cumulated CPU time (s) 137.07 Current children cumulated vsize (Kb) 35348 [startup+151.297 s] Raw data (loadavg): 1.00 1.00 0.98 3/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 8169 0 0 0 14661 41 0 0 25 0 1 0 1797290158 35598336 7976 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 8691 7976 145 145 0 8546 0 [pid=25196] vsize: 34764 Current children cumulated CPU time (s) 147.02 Current children cumulated vsize (Kb) 36888 [startup+161.296 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 8371 0 0 0 15658 43 0 0 25 0 1 0 1797290158 36401152 8178 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 8887 8178 145 145 0 8742 0 [pid=25196] vsize: 35548 Current children cumulated CPU time (s) 157.01 Current children cumulated vsize (Kb) 37672 [startup+171.297 s] Raw data (loadavg): 1.00 1.00 0.98 1/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) T 25192 25192 824 0 -1 0 8560 0 0 0 16653 45 0 0 25 0 1 0 1797290158 37167104 8367 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/25196/statm): 9074 8367 145 145 0 8929 0 [pid=25196] vsize: 36296 Current children cumulated CPU time (s) 166.98 Current children cumulated vsize (Kb) 38420 [startup+181.298 s] Raw data (loadavg): 1.00 1.00 0.98 3/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 8700 0 0 0 17651 46 0 0 25 0 1 0 1797290158 37728256 8507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 9211 8507 145 145 0 9066 0 [pid=25196] vsize: 36844 Current children cumulated CPU time (s) 176.97 Current children cumulated vsize (Kb) 38968 [startup+191.299 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 8856 0 0 0 18648 47 0 0 25 0 1 0 1797290158 38363136 8663 4294967295 134512640 135094434 3221224448 3221222976 134780540 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 9366 8663 145 145 0 9221 0 [pid=25196] vsize: 37464 Current children cumulated CPU time (s) 186.95 Current children cumulated vsize (Kb) 39588 [startup+201.299 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9011 0 0 0 19645 49 0 0 25 0 1 0 1797290158 38981632 8818 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 9517 8818 145 145 0 9372 0 [pid=25196] vsize: 38068 Current children cumulated CPU time (s) 196.94 Current children cumulated vsize (Kb) 40192 [startup+211.3 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9278 0 0 0 20641 50 0 0 25 0 1 0 1797290158 40030208 9085 4294967295 134512640 135094434 3221224448 3221223104 134557984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 9773 9085 145 145 0 9628 0 [pid=25196] vsize: 39092 Current children cumulated CPU time (s) 206.91 Current children cumulated vsize (Kb) 41216 [startup+221.301 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9446 0 0 0 21637 52 0 0 25 0 1 0 1797290158 40726528 9253 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 9943 9253 145 145 0 9798 0 [pid=25196] vsize: 39772 Current children cumulated CPU time (s) 216.89 Current children cumulated vsize (Kb) 41896 [startup+231.302 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9629 0 0 0 22634 53 0 0 25 0 1 0 1797290158 41455616 9436 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 10121 9436 145 145 0 9976 0 [pid=25196] vsize: 40484 Current children cumulated CPU time (s) 226.87 Current children cumulated vsize (Kb) 42608 [startup+241.302 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9905 0 0 0 23630 55 0 0 25 0 1 0 1797290158 42561536 9712 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 10391 9712 145 145 0 10246 0 [pid=25196] vsize: 41564 Current children cumulated CPU time (s) 236.85 Current children cumulated vsize (Kb) 43688 [startup+251.303 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10243 0 0 0 24623 58 0 0 25 0 1 0 1797290158 43921408 10050 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 10723 10050 145 145 0 10578 0 [pid=25196] vsize: 42892 Current children cumulated CPU time (s) 246.81 Current children cumulated vsize (Kb) 45016 [startup+261.304 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10395 0 0 0 25621 59 0 0 25 0 1 0 1797290158 44531712 10202 4294967295 134512640 135094434 3221224448 3221223120 134555399 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 10872 10202 145 145 0 10727 0 [pid=25196] vsize: 43488 Current children cumulated CPU time (s) 256.8 Current children cumulated vsize (Kb) 45612 [startup+271.305 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10518 0 0 0 26618 60 0 0 25 0 1 0 1797290158 45023232 10325 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 10992 10325 145 145 0 10847 0 [pid=25196] vsize: 43968 Current children cumulated CPU time (s) 266.78 Current children cumulated vsize (Kb) 46092 [startup+281.305 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10663 0 0 0 27615 61 0 0 25 0 1 0 1797290158 45608960 10470 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 11135 10470 145 145 0 10990 0 [pid=25196] vsize: 44540 Current children cumulated CPU time (s) 276.76 Current children cumulated vsize (Kb) 46664 [startup+291.307 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10820 0 0 0 28613 62 0 0 25 0 1 0 1797290158 46243840 10627 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 11290 10627 145 145 0 11145 0 [pid=25196] vsize: 45160 Current children cumulated CPU time (s) 286.75 Current children cumulated vsize (Kb) 47284 [startup+301.308 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11017 0 0 0 29609 64 0 0 25 0 1 0 1797290158 47042560 10824 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25196/statm): 11485 10824 145 145 0 11340 0 [pid=25196] vsize: 45940 Current children cumulated CPU time (s) 296.73 Current children cumulated vsize (Kb) 48064 [startup+311.309 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11132 0 0 0 30607 65 0 0 25 0 1 0 1797290158 48037888 10939 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 11728 10939 145 145 0 11583 0 [pid=25196] vsize: 46912 Current children cumulated CPU time (s) 306.72 Current children cumulated vsize (Kb) 49036 [startup+321.309 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11407 0 0 0 31602 66 0 0 25 0 1 0 1797290158 49139712 11214 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 11997 11214 145 145 0 11852 0 [pid=25196] vsize: 47988 Current children cumulated CPU time (s) 316.68 Current children cumulated vsize (Kb) 50112 [startup+331.31 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11562 0 0 0 32600 68 0 0 25 0 1 0 1797290158 49758208 11369 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 12148 11369 145 145 0 12003 0 [pid=25196] vsize: 48592 Current children cumulated CPU time (s) 326.68 Current children cumulated vsize (Kb) 50716 [startup+341.311 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11722 0 0 0 33597 69 0 0 25 0 1 0 1797290158 50405376 11529 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 12306 11529 145 145 0 12161 0 [pid=25196] vsize: 49224 Current children cumulated CPU time (s) 336.66 Current children cumulated vsize (Kb) 51348 [startup+351.312 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11873 0 0 0 34595 70 0 0 25 0 1 0 1797290158 51023872 11680 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 12457 11680 145 145 0 12312 0 [pid=25196] vsize: 49828 Current children cumulated CPU time (s) 346.65 Current children cumulated vsize (Kb) 51952 [startup+361.312 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12098 0 0 0 35591 71 0 0 25 0 1 0 1797290158 51924992 11905 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 12677 11905 145 145 0 12532 0 [pid=25196] vsize: 50708 Current children cumulated CPU time (s) 356.62 Current children cumulated vsize (Kb) 52832 [startup+371.313 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12296 0 0 0 36587 74 0 0 25 0 1 0 1797290158 52723712 12103 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 12872 12103 145 145 0 12727 0 [pid=25196] vsize: 51488 Current children cumulated CPU time (s) 366.61 Current children cumulated vsize (Kb) 53612 [startup+381.314 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12486 0 0 0 37584 75 0 0 25 0 1 0 1797290158 53481472 12293 4294967295 134512640 135094434 3221224448 3221223088 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 13057 12293 145 145 0 12912 0 [pid=25196] vsize: 52228 Current children cumulated CPU time (s) 376.59 Current children cumulated vsize (Kb) 54352 [startup+391.315 s] Raw data (loadavg): 1.00 1.00 0.98 3/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12683 0 0 0 38580 77 0 0 25 0 1 0 1797290158 54267904 12490 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 13249 12490 145 145 0 13104 0 [pid=25196] vsize: 52996 Current children cumulated CPU time (s) 386.57 Current children cumulated vsize (Kb) 55120 [startup+401.316 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12867 0 0 0 39577 79 0 0 25 0 1 0 1797290158 55025664 12674 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 13434 12674 145 145 0 13289 0 [pid=25196] vsize: 53736 Current children cumulated CPU time (s) 396.56 Current children cumulated vsize (Kb) 55860 [startup+411.317 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12994 0 0 0 40575 80 0 0 25 0 1 0 1797290158 55549952 12801 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 13562 12801 145 145 0 13417 0 [pid=25196] vsize: 54248 Current children cumulated CPU time (s) 406.55 Current children cumulated vsize (Kb) 56372 [startup+421.318 s] Raw data (loadavg): 1.00 1.00 0.98 3/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13136 0 0 0 41573 81 0 0 25 0 1 0 1797290158 56131584 12943 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 13704 12943 145 145 0 13559 0 [pid=25196] vsize: 54816 Current children cumulated CPU time (s) 416.54 Current children cumulated vsize (Kb) 56940 [startup+431.318 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13258 0 0 0 42572 81 0 0 25 0 1 0 1797290158 56606720 13065 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 13820 13065 145 145 0 13675 0 [pid=25196] vsize: 55280 Current children cumulated CPU time (s) 426.53 Current children cumulated vsize (Kb) 57404 [startup+441.32 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13404 0 0 0 43571 82 0 0 25 0 1 0 1797290158 57180160 13211 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 13960 13211 145 145 0 13815 0 [pid=25196] vsize: 55840 Current children cumulated CPU time (s) 436.53 Current children cumulated vsize (Kb) 57964 [startup+451.321 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13580 0 0 0 44568 83 0 0 25 0 1 0 1797290158 57896960 13387 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 14135 13387 145 145 0 13990 0 [pid=25196] vsize: 56540 Current children cumulated CPU time (s) 446.51 Current children cumulated vsize (Kb) 58664 [startup+461.322 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) T 25192 25192 824 0 -1 0 13697 0 0 0 45566 84 0 0 25 0 1 0 1797290158 58388480 13504 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/25196/statm): 14255 13504 145 145 0 14110 0 [pid=25196] vsize: 57020 Current children cumulated CPU time (s) 456.5 Current children cumulated vsize (Kb) 59144 [startup+471.322 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13837 0 0 0 46562 86 0 0 25 0 1 0 1797290158 58953728 13644 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25196/statm): 14393 13644 145 145 0 14248 0 [pid=25196] vsize: 57572 Current children cumulated CPU time (s) 466.48 Current children cumulated vsize (Kb) 59696 [startup+481.323 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13964 0 0 0 47559 87 0 0 25 0 1 0 1797290158 59465728 13771 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25196/statm): 14518 13771 145 145 0 14373 0 [pid=25196] vsize: 58072 Current children cumulated CPU time (s) 476.46 Current children cumulated vsize (Kb) 60196 [startup+491.325 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14086 0 0 0 48557 88 0 0 25 0 1 0 1797290158 59961344 13893 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 14639 13893 145 145 0 14494 0 [pid=25196] vsize: 58556 Current children cumulated CPU time (s) 486.45 Current children cumulated vsize (Kb) 60680 [startup+501.326 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14238 0 0 0 49554 89 0 0 25 0 1 0 1797290158 60575744 14045 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 14789 14045 145 145 0 14644 0 [pid=25196] vsize: 59156 Current children cumulated CPU time (s) 496.43 Current children cumulated vsize (Kb) 61280 [startup+511.326 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14406 0 0 0 50552 90 0 0 25 0 1 0 1797290158 61247488 14213 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 14953 14213 145 145 0 14808 0 [pid=25196] vsize: 59812 Current children cumulated CPU time (s) 506.42 Current children cumulated vsize (Kb) 61936 [startup+521.327 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14545 0 0 0 51550 90 0 0 25 0 1 0 1797290158 61857792 14352 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 15102 14352 145 145 0 14957 0 [pid=25196] vsize: 60408 Current children cumulated CPU time (s) 516.4 Current children cumulated vsize (Kb) 62532 [startup+531.328 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14645 0 0 0 52549 91 0 0 25 0 1 0 1797290158 62267392 14452 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 15202 14452 145 145 0 15057 0 [pid=25196] vsize: 60808 Current children cumulated CPU time (s) 526.4 Current children cumulated vsize (Kb) 62932 [startup+541.329 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14786 0 0 0 53547 92 0 0 25 0 1 0 1797290158 62840832 14593 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 15342 14593 145 145 0 15197 0 [pid=25196] vsize: 61368 Current children cumulated CPU time (s) 536.39 Current children cumulated vsize (Kb) 63492 [startup+551.329 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14874 0 0 0 54545 93 0 0 25 0 1 0 1797290158 63180800 14681 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 15425 14681 145 145 0 15280 0 [pid=25196] vsize: 61700 Current children cumulated CPU time (s) 546.38 Current children cumulated vsize (Kb) 63824 [startup+561.33 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14960 0 0 0 55544 93 0 0 25 0 1 0 1797290158 63524864 14767 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25196/statm): 15509 14767 145 145 0 15364 0 [pid=25196] vsize: 62036 Current children cumulated CPU time (s) 556.37 Current children cumulated vsize (Kb) 64160 [startup+571.331 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15050 0 0 0 56542 95 0 0 25 0 1 0 1797290158 63909888 14857 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 15603 14857 145 145 0 15458 0 [pid=25196] vsize: 62412 Current children cumulated CPU time (s) 566.37 Current children cumulated vsize (Kb) 64536 [startup+581.332 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15158 0 0 0 57540 95 0 0 25 0 1 0 1797290158 64335872 14965 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 15707 14965 145 145 0 15562 0 [pid=25196] vsize: 62828 Current children cumulated CPU time (s) 576.35 Current children cumulated vsize (Kb) 64952 [startup+591.332 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15363 0 0 0 58537 97 0 0 25 0 1 0 1797290158 65159168 15170 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 15908 15170 145 145 0 15763 0 [pid=25196] vsize: 63632 Current children cumulated CPU time (s) 586.34 Current children cumulated vsize (Kb) 65756 [startup+601.333 s] Raw data (loadavg): 1.00 1.00 0.98 1/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) T 25192 25192 824 0 -1 0 15606 0 0 0 59532 99 0 0 25 0 1 0 1797290158 66142208 15413 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/25196/statm): 16148 15413 145 145 0 16003 0 [pid=25196] vsize: 64592 Current children cumulated CPU time (s) 596.31 Current children cumulated vsize (Kb) 66716 [startup+611.334 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15729 0 0 0 60530 99 0 0 25 0 1 0 1797290158 66650112 15536 4294967295 134512640 135094434 3221224448 3221223104 134557832 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 16272 15536 145 145 0 16127 0 [pid=25196] vsize: 65088 Current children cumulated CPU time (s) 606.29 Current children cumulated vsize (Kb) 67212 [startup+621.335 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15860 0 0 0 61528 100 0 0 25 0 1 0 1797290158 67182592 15667 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 16402 15667 145 145 0 16257 0 [pid=25196] vsize: 65608 Current children cumulated CPU time (s) 616.28 Current children cumulated vsize (Kb) 67732 [startup+631.335 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15961 0 0 0 62527 101 0 0 25 0 1 0 1797290158 67633152 15768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 16512 15768 145 145 0 16367 0 [pid=25196] vsize: 66048 Current children cumulated CPU time (s) 626.28 Current children cumulated vsize (Kb) 68172 [startup+641.336 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16070 0 0 0 63527 101 0 0 25 0 1 0 1797290158 68042752 15877 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 16612 15877 145 145 0 16467 0 [pid=25196] vsize: 66448 Current children cumulated CPU time (s) 636.28 Current children cumulated vsize (Kb) 68572 [startup+651.337 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16180 0 0 0 64525 102 0 0 25 0 1 0 1797290158 68501504 15987 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 16724 15987 145 145 0 16579 0 [pid=25196] vsize: 66896 Current children cumulated CPU time (s) 646.27 Current children cumulated vsize (Kb) 69020 [startup+661.336 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16282 0 0 0 65524 103 0 0 25 0 1 0 1797290158 68902912 16089 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 16822 16089 145 145 0 16677 0 [pid=25196] vsize: 67288 Current children cumulated CPU time (s) 656.27 Current children cumulated vsize (Kb) 69412 [startup+671.338 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16383 0 0 0 66523 103 0 0 25 0 1 0 1797290158 69320704 16190 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 16924 16190 145 145 0 16779 0 [pid=25196] vsize: 67696 Current children cumulated CPU time (s) 666.26 Current children cumulated vsize (Kb) 69820 [startup+681.339 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16480 0 0 0 67521 104 0 0 25 0 1 0 1797290158 69718016 16287 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 17021 16287 145 145 0 16876 0 [pid=25196] vsize: 68084 Current children cumulated CPU time (s) 676.25 Current children cumulated vsize (Kb) 70208 [startup+691.34 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16639 0 0 0 68518 106 0 0 25 0 1 0 1797290158 70365184 16446 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 17179 16446 145 145 0 17034 0 [pid=25196] vsize: 68716 Current children cumulated CPU time (s) 686.24 Current children cumulated vsize (Kb) 70840 [startup+701.34 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16809 0 0 0 69515 107 0 0 25 0 1 0 1797290158 71065600 16616 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 17350 16616 145 145 0 17205 0 [pid=25196] vsize: 69400 Current children cumulated CPU time (s) 696.22 Current children cumulated vsize (Kb) 71524 [startup+711.341 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17003 0 0 0 70510 109 0 0 25 0 1 0 1797290158 71852032 16810 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 17542 16810 145 145 0 17397 0 [pid=25196] vsize: 70168 Current children cumulated CPU time (s) 706.19 Current children cumulated vsize (Kb) 72292 [startup+721.342 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17100 0 0 0 71510 109 0 0 25 0 1 0 1797290158 72237056 16907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 17636 16907 145 145 0 17491 0 [pid=25196] vsize: 70544 Current children cumulated CPU time (s) 716.19 Current children cumulated vsize (Kb) 72668 [startup+731.343 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17206 0 0 0 72509 109 0 0 25 0 1 0 1797290158 73711616 17013 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 17996 17013 145 145 0 17851 0 [pid=25196] vsize: 71984 Current children cumulated CPU time (s) 726.18 Current children cumulated vsize (Kb) 74108 [startup+741.344 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17316 0 0 0 73507 110 0 0 25 0 1 0 1797290158 74137600 17123 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18100 17123 145 145 0 17955 0 [pid=25196] vsize: 72400 Current children cumulated CPU time (s) 736.17 Current children cumulated vsize (Kb) 74524 [startup+751.345 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17397 0 0 0 74506 111 0 0 25 0 1 0 1797290158 74481664 17204 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18184 17204 145 145 0 18039 0 [pid=25196] vsize: 72736 Current children cumulated CPU time (s) 746.17 Current children cumulated vsize (Kb) 74860 [startup+761.346 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17483 0 0 0 75504 112 0 0 25 0 1 0 1797290158 74825728 17290 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18268 17290 145 145 0 18123 0 [pid=25196] vsize: 73072 Current children cumulated CPU time (s) 756.16 Current children cumulated vsize (Kb) 75196 [startup+771.348 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17579 0 0 0 76503 113 0 0 25 0 1 0 1797290158 75218944 17386 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18364 17386 145 145 0 18219 0 [pid=25196] vsize: 73456 Current children cumulated CPU time (s) 766.16 Current children cumulated vsize (Kb) 75580 [startup+781.348 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17684 0 0 0 77501 114 0 0 25 0 1 0 1797290158 75677696 17491 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18476 17491 145 145 0 18331 0 [pid=25196] vsize: 73904 Current children cumulated CPU time (s) 776.15 Current children cumulated vsize (Kb) 76028 [startup+791.35 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17776 0 0 0 78500 115 0 0 25 0 1 0 1797290158 76042240 17583 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18565 17583 145 145 0 18420 0 [pid=25196] vsize: 74260 Current children cumulated CPU time (s) 786.15 Current children cumulated vsize (Kb) 76384 [startup+801.351 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17882 0 0 0 79498 115 0 0 25 0 1 0 1797290158 76464128 17689 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18668 17689 145 145 0 18523 0 [pid=25196] vsize: 74672 Current children cumulated CPU time (s) 796.13 Current children cumulated vsize (Kb) 76796 [startup+811.352 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17963 0 0 0 80496 116 0 0 25 0 1 0 1797290158 76779520 17770 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18745 17770 145 145 0 18600 0 [pid=25196] vsize: 74980 Current children cumulated CPU time (s) 806.12 Current children cumulated vsize (Kb) 77104 [startup+821.352 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18054 0 0 0 81496 117 0 0 25 0 1 0 1797290158 77172736 17861 4294967295 134512640 135094434 3221224448 3221223040 134557269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18841 17861 145 145 0 18696 0 [pid=25196] vsize: 75364 Current children cumulated CPU time (s) 816.13 Current children cumulated vsize (Kb) 77488 [startup+831.353 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18111 0 0 0 82495 117 0 0 25 0 1 0 1797290158 77459456 17918 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18911 17918 145 145 0 18766 0 [pid=25196] vsize: 75644 Current children cumulated CPU time (s) 826.12 Current children cumulated vsize (Kb) 77768 [startup+841.355 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 83494 118 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 836.12 Current children cumulated vsize (Kb) 78048 [startup+851.356 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 84495 118 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 846.13 Current children cumulated vsize (Kb) 78048 [startup+861.356 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 85495 118 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 856.13 Current children cumulated vsize (Kb) 78048 [startup+871.357 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 86494 118 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 866.12 Current children cumulated vsize (Kb) 78048 [startup+881.358 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 87493 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 876.12 Current children cumulated vsize (Kb) 78048 [startup+891.359 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 88493 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 886.12 Current children cumulated vsize (Kb) 78048 [startup+901.359 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 89493 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 896.12 Current children cumulated vsize (Kb) 78048 [startup+911.36 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 90494 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 906.13 Current children cumulated vsize (Kb) 78048 [startup+921.361 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 91494 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 916.13 Current children cumulated vsize (Kb) 78048 [startup+931.361 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 92494 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 926.13 Current children cumulated vsize (Kb) 78048 [startup+941.362 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18185 0 0 0 93494 119 0 0 25 0 1 0 1797290158 77746176 17992 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17992 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 936.13 Current children cumulated vsize (Kb) 78048 [startup+951.363 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18185 0 0 0 94495 119 0 0 25 0 1 0 1797290158 77746176 17992 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17992 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 946.14 Current children cumulated vsize (Kb) 78048 [startup+961.363 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18185 0 0 0 95495 119 0 0 25 0 1 0 1797290158 77746176 17992 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17992 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 956.14 Current children cumulated vsize (Kb) 78048 [startup+971.363 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18185 0 0 0 96495 119 0 0 25 0 1 0 1797290158 77746176 17992 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17992 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 966.14 Current children cumulated vsize (Kb) 78048 [startup+981.364 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18187 0 0 0 97495 119 0 0 25 0 1 0 1797290158 77746176 17994 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18981 17994 145 145 0 18836 0 [pid=25196] vsize: 75924 Current children cumulated CPU time (s) 976.14 Current children cumulated vsize (Kb) 78048 [startup+991.365 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18197 0 0 0 98496 119 0 0 25 0 1 0 1797290158 77811712 18004 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 18997 18004 145 145 0 18852 0 [pid=25196] vsize: 75988 Current children cumulated CPU time (s) 986.15 Current children cumulated vsize (Kb) 78112 [startup+1001.37 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18208 0 0 0 99496 119 0 0 25 0 1 0 1797290158 77877248 18015 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19013 18015 145 145 0 18868 0 [pid=25196] vsize: 76052 Current children cumulated CPU time (s) 996.15 Current children cumulated vsize (Kb) 78176 [startup+1011.37 s] Raw data (loadavg): 1.00 1.00 0.98 3/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18218 0 0 0 100496 119 0 0 25 0 1 0 1797290158 77942784 18025 4294967295 134512640 135094434 3221224448 3221223040 134551757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18025 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1006.15 Current children cumulated vsize (Kb) 78240 [startup+1021.37 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18221 0 0 0 101496 119 0 0 25 0 1 0 1797290158 77942784 18028 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18028 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1016.15 Current children cumulated vsize (Kb) 78240 [startup+1031.37 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18223 0 0 0 102497 119 0 0 25 0 1 0 1797290158 77942784 18030 4294967295 134512640 135094434 3221224448 3221223060 134563024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18030 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1026.16 Current children cumulated vsize (Kb) 78240 [startup+1041.37 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 103497 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1036.16 Current children cumulated vsize (Kb) 78240 [startup+1051.37 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 104497 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1046.16 Current children cumulated vsize (Kb) 78240 [startup+1061.37 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 105497 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1056.16 Current children cumulated vsize (Kb) 78240 [startup+1071.37 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 106498 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223120 134556517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1066.17 Current children cumulated vsize (Kb) 78240 [startup+1081.37 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 107498 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1076.17 Current children cumulated vsize (Kb) 78240 [startup+1091.37 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 108498 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1086.17 Current children cumulated vsize (Kb) 78240 [startup+1101.38 s] Raw data (loadavg): 1.00 1.00 0.98 3/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 109499 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1096.18 Current children cumulated vsize (Kb) 78240 [startup+1111.38 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 110499 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1106.18 Current children cumulated vsize (Kb) 78240 [startup+1121.38 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 111499 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1116.18 Current children cumulated vsize (Kb) 78240 [startup+1131.38 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 112499 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1126.18 Current children cumulated vsize (Kb) 78240 [startup+1141.38 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 113500 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223120 134555583 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1136.19 Current children cumulated vsize (Kb) 78240 [startup+1151.38 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18226 0 0 0 114500 119 0 0 25 0 1 0 1797290158 77942784 18033 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19029 18033 145 145 0 18884 0 [pid=25196] vsize: 76116 Current children cumulated CPU time (s) 1146.19 Current children cumulated vsize (Kb) 78240 [startup+1161.38 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18237 0 0 0 115500 119 0 0 25 0 1 0 1797290158 78008320 18044 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19045 18044 145 145 0 18900 0 [pid=25196] vsize: 76180 Current children cumulated CPU time (s) 1156.19 Current children cumulated vsize (Kb) 78304 [startup+1171.38 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18240 0 0 0 116500 119 0 0 25 0 1 0 1797290158 78008320 18047 4294967295 134512640 135094434 3221224448 3221223104 134558024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19045 18047 145 145 0 18900 0 [pid=25196] vsize: 76180 Current children cumulated CPU time (s) 1166.19 Current children cumulated vsize (Kb) 78304 [startup+1181.38 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18252 0 0 0 117500 119 0 0 25 0 1 0 1797290158 78073856 18059 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19061 18059 145 145 0 18916 0 [pid=25196] vsize: 76244 Current children cumulated CPU time (s) 1176.19 Current children cumulated vsize (Kb) 78368 [startup+1191.39 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18263 0 0 0 118501 119 0 0 25 0 1 0 1797290158 78139392 18070 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19077 18070 145 145 0 18932 0 [pid=25196] vsize: 76308 Current children cumulated CPU time (s) 1186.2 Current children cumulated vsize (Kb) 78432 [startup+1201.39 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18266 0 0 0 119501 119 0 0 25 0 1 0 1797290158 78139392 18073 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19077 18073 145 145 0 18932 0 [pid=25196] vsize: 76308 Current children cumulated CPU time (s) 1196.2 Current children cumulated vsize (Kb) 78432 [startup+1211.39 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18266 0 0 0 120501 119 0 0 25 0 1 0 1797290158 78139392 18073 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19077 18073 145 145 0 18932 0 [pid=25196] vsize: 76308 Current children cumulated CPU time (s) 1206.2 Current children cumulated vsize (Kb) 78432 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1211.39 s] Raw data (loadavg): 1.00 1.00 0.98 2/57 25196 Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25192/statm): 531 226 485 147 0 384 0 [pid=25192] vsize: 2124 Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18266 0 0 0 120501 119 0 0 25 0 1 0 1797290158 78139392 18073 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25196/statm): 19077 18073 145 145 0 18932 0 [pid=25196] vsize: 76308 Current children cumulated CPU time (s) 1206.2 Current children cumulated vsize (Kb) 78432 Sending SIGTERM to -25192 Sleeping 2 seconds One traced child (pid=25192) ended because it received signal 15 (SIGTERM) One traced child (pid=25196) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1211.43 CPU time (s): 1206.25 CPU user time (s): 1205.02 CPU system time (s): 1.23281 CPU usage (%): 99.5726 Max. virtual memory (cumulated for all children) (Kb): 78432
ERROR: no interpretation found !