Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-vpm2.opb |
MD5SUM | c1b4c3ad409db732d2b559e570b6f24c |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 138 |
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 | 819200 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 4941871 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.01 |
Number of variables | 2754 |
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 | 84 |
LAUNCH ON wulflinc2 THE 2005-09-19 17:42:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2951 boxname=wulflinc2 idbench=607 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c1b4c3ad409db732d2b559e570b6f24c /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-vpm2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-vpm2.opb IDLAUNCH: 2951 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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.191 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: 856892 kB Buffers: 39824 kB Cached: 110980 kB SwapCached: 1040 kB Active: 63888 kB Inactive: 89552 kB HighTotal: 131008 kB HighFree: 27496 kB LowTotal: 903652 kB LowFree: 829396 kB SwapTotal: 2097136 kB SwapFree: 2095568 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 18548 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 18:02:11 (client local time) WITH STATUS 0 IN 1208.5 SECONDS stats: 2951 7 1208.5 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: 10 c ---[ 484]---> BDD-cost: 10 c ---[ 483]---> BDD-cost: 10 c ---[ 482]---> BDD-cost: 10 c ---[ 481]---> BDD-cost: 10 c ---[ 480]---> BDD-cost: 10 c ---[ 479]---> BDD-cost: 10 c ---[ 478]---> BDD-cost: 10 c ---[ 477]---> BDD-cost: 10 c ---[ 474]---> BDD-cost: 10 c ---[ 473]---> BDD-cost: 10 c ---[ 472]---> BDD-cost: 10 c ---[ 471]---> BDD-cost: 10 c ---[ 468]---> BDD-cost: 10 c ---[ 467]---> BDD-cost: 10 c ---[ 466]---> BDD-cost: 10 c ---[ 465]---> BDD-cost: 10 c ---[ 462]---> BDD-cost: 10 c ---[ 459]---> BDD-cost: 10 c ---[ 458]---> BDD-cost: 10 c ---[ 457]---> BDD-cost: 10 c ---[ 454]---> BDD-cost: 10 c ---[ 453]---> BDD-cost: 10 c ---[ 452]---> BDD-cost: 10 c ---[ 451]---> BDD-cost: 10 c ---[ 450]---> BDD-cost: 10 c ---[ 448]---> BDD-cost: 10 c ---[ 447]---> BDD-cost: 10 c ---[ 446]---> BDD-cost: 10 c ---[ 445]---> BDD-cost: 10 c ---[ 444]---> BDD-cost: 10 c ---[ 441]---> BDD-cost: 10 c ---[ 440]---> BDD-cost: 10 c ---[ 439]---> BDD-cost: 10 c ---[ 433]---> BDD-cost: 10 c ---[ 427]---> BDD-cost: 10 c ---[ 422]---> BDD-cost: 10 c ---[ 421]---> BDD-cost: 10 c ---[ 415]---> BDD-cost: 10 c ---[ 409]---> BDD-cost: 10 c ---[ 408]---> BDD-cost: 10 c ---[ 402]---> BDD-cost: 10 c ---[ 397]---> BDD-cost: 10 c ---[ 396]---> BDD-cost: 10 c ---[ 391]---> BDD-cost: 10 c ---[ 390]---> BDD-cost: 10 c ---[ 386]---> BDD-cost: 10 c ---[ 385]---> BDD-cost: 10 c ---[ 384]---> BDD-cost: 10 c ---[ 380]---> BDD-cost: 10 c ---[ 379]---> BDD-cost: 10 c ---[ 378]---> BDD-cost: 10 c ---[ 374]---> BDD-cost: 10 c ---[ 373]---> BDD-cost: 10 c ---[ 372]---> BDD-cost: 10 c ---[ 368]---> BDD-cost: 10 c ---[ 367]---> BDD-cost: 10 c ---[ 366]---> BDD-cost: 10 c ---[ 365]---> BDD-cost: 10 c ---[ 364]---> BDD-cost: 10 c ---[ 359]---> BDD-cost: 10 c ---[ 353]---> BDD-cost: 10 c ---[ 347]---> BDD-cost: 10 c ---[ 339]---> BDD-cost: 10 c ---[ 333]---> BDD-cost: 10 c ---[ 327]---> BDD-cost: 10 c ---[ 321]---> BDD-cost: 10 c ---[ 317]---> BDD-cost: 17 c ---[ 316]---> BDD-cost: 17 c ---[ 315]---> BDD-cost: 17 c ---[ 314]---> BDD-cost: 17 c ---[ 313]---> BDD-cost: 17 c ---[ 312]---> BDD-cost: 17 c ---[ 310]---> BDD-cost: 17 c ---[ 309]---> BDD-cost: 17 c ---[ 308]---> BDD-cost: 17 c ---[ 307]---> BDD-cost: 17 c ---[ 306]---> BDD-cost: 17 c ---[ 302]---> BDD-cost: 16 c ---[ 301]---> BDD-cost: 16 c ---[ 300]---> BDD-cost: 16 c ---[ 295]---> BDD-cost: 16 c ---[ 294]---> BDD-cost: 16 c ---[ 290]---> BDD-cost: 18 c ---[ 289]---> BDD-cost: 18 c ---[ 288]---> BDD-cost: 18 c ---[ 287]---> BDD-cost: 16 c ---[ 286]---> BDD-cost: 16 c ---[ 285]---> BDD-cost: 16 c ---[ 284]---> BDD-cost: 16 c ---[ 283]---> BDD-cost: 16 c ---[ 282]---> BDD-cost: 16 c ---[ 280]---> BDD-cost: 16 c ---[ 279]---> BDD-cost: 16 c ---[ 278]---> BDD-cost: 16 c ---[ 277]---> BDD-cost: 16 c ---[ 276]---> BDD-cost: 16 c ---[ 274]---> Adder-cost: 352 maxlim: 2411343 bits: 22/22 c ---[ 272]---> Adder-cost: 288 maxlim: 1694643 bits: 21/21 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: 10 c ---[ 258]---> BDD-cost: 3 c ---[ 257]---> BDD-cost: 3 c ---[ 256]---> BDD-cost: 3 c ---[ 255]---> BDD-cost: 10 c ---[ 251]---> BDD-cost: 10 c ---[ 250]---> BDD-cost: 3 c ---[ 247]---> BDD-cost: 9 c ---[ 243]---> BDD-cost: 10 c ---[ 242]---> BDD-cost: 3 c ---[ 241]---> BDD-cost: 9 c ---[ 236]---> Sorter-cost: 2294 Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[ 235]---> BDD-cost: 3 c ---[ 234]---> BDD-cost: 3 c ---[ 233]---> BDD-cost: 9 c ---[ 229]---> BDD-cost: 10 c ---[ 228]---> BDD-cost: 3 c ---[ 227]---> BDD-cost: 9 c ---[ 224]---> Adder-cost: 312 maxlim: 2587171 bits: 22/22 c ---[ 220]---> BDD-cost: 3 c ---[ 219]---> BDD-cost: 3 c ---[ 214]---> BDD-cost: 10 c ---[ 212]---> Adder-cost: 260 maxlim: 897571 bits: 20/20 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: 9 c ---[ 164]---> Sorter-cost: 2815 Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3 c ---[ 163]---> BDD-cost: 9 c ---[ 162]---> BDD-cost: 9 c ---[ 161]---> BDD-cost: 9 c ---[ 160]---> BDD-cost: 3 c ---[ 159]---> BDD-cost: 10 c ---[ 158]---> BDD-cost: 9 c ---[ 157]---> BDD-cost: 9 c ---[ 156]---> BDD-cost: 9 c ---[ 155]---> BDD-cost: 9 c ---[ 154]---> BDD-cost: 3 c ---[ 152]---> Adder-cost: 352 maxlim: 2411343 bits: 22/22 c ---[ 150]---> Adder-cost: 350 maxlim: 1768271 bits: 22/21 c ---[ 149]---> BDD-cost: 10 c ---[ 148]---> BDD-cost: 8 c ---[ 147]---> BDD-cost: 8 c ---[ 146]---> BDD-cost: 8 c ---[ 145]---> BDD-cost: 8 c ---[ 144]---> BDD-cost: 3 c ---[ 143]---> BDD-cost: 10 c ---[ 142]---> BDD-cost: 8 c ---[ 141]---> BDD-cost: 8 c ---[ 140]---> BDD-cost: 8 c ---[ 137]---> BDD-cost: 8 c ---[ 135]---> BDD-cost: 10 c ---[ 134]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 9 c ---[ 132]---> BDD-cost: 9 c ---[ 131]---> BDD-cost: 9 c ---[ 129]---> BDD-cost: 10 c ---[ 128]---> BDD-cost: 3 c ---[ 125]---> BDD-cost: 9 c ---[ 124]---> BDD-cost: 9 c ---[ 123]---> BDD-cost: 9 c ---[ 121]---> BDD-cost: 10 c ---[ 120]---> BDD-cost: 3 c ---[ 119]---> BDD-cost: 9 c ---[ 118]---> BDD-cost: 9 c ---[ 117]---> BDD-cost: 9 c ---[ 114]---> Adder-cost: 274 maxlim: 1228100 bits: 21/21 c ---[ 113]---> BDD-cost: 10 c ---[ 112]---> BDD-cost: 3 c ---[ 111]---> BDD-cost: 8 c ---[ 110]---> BDD-cost: 8 c ---[ 109]---> BDD-cost: 8 c ---[ 107]---> Adder-cost: 312 maxlim: 1957187 bits: 22/21 c ---[ 105]---> Adder-cost: 312 maxlim: 1854787 bits: 22/21 c ---[ 103]---> Adder-cost: 390 maxlim: 2279471 bits: 22/22 c ---[ 101]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 99]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 97]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 95]---> Adder-cost: 330 maxlim: 1694543 bits: 21/21 c ---[ 93]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 91]---> Sorter-cost: 3240 Base: 2 2 2 2 5 5 2 2 2 2 2 2 5 c ---[ 89]---> Adder-cost: 440 maxlim: 3713071 bits: 23/22 c ---[ 87]---> Adder-cost: 368 maxlim: 999471 bits: 21/20 c ---[ 85]---> Adder-cost: 368 maxlim: 999471 bits: 21/20 c ---[ 83]---> Adder-cost: 368 maxlim: 999471 bits: 21/20 c ---[ 81]---> Sorter-cost: 3227 Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3 c ---[ 73]---> Adder-cost: 330 maxlim: 1694543 bits: 21/21 c ---[ 69]---> Sorter-cost: 3277 Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2 c ---[ 66]---> BDD-cost: 230 c ---[ 65]---> BDD-cost: 661 c ---[ 64]---> BDD-cost: 660 c ---[ 63]---> Sorter-cost: 1990 Base: 5 5 5 2 2 2 2 2 2 2 2 2 c ---[ 62]---> Sorter-cost: 2375 Base: 5 5 5 2 2 2 2 2 2 2 2 2 c ---[ 61]---> Sorter-cost: 2299 Base: 5 5 5 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 414 Base: 2 2 2 2 2 2 2 2 5 2 c ---[ 58]---> Adder-cost: 352 maxlim: 2104143 bits: 22/22 c ---[ 57]---> Sorter-cost: 1128 Base: 5 2 2 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 1146 Base: 5 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 1625 Base: 5 2 2 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 1905 Base: 5 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 1909 Base: 5 2 2 2 2 2 2 2 2 2 c ---[ 52]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 5 c ---[ 51]---> Sorter-cost: 1242 Base: 2 2 2 2 2 5 2 2 2 2 c ---[ 50]---> Sorter-cost: 1199 Base: 2 2 2 2 2 2 2 2 2 5 c ---[ 49]---> Sorter-cost: 1719 Base: 5 2 2 2 2 2 2 2 2 2 c ---[ 48]---> Sorter-cost: 2067 Base: 5 2 2 2 2 2 2 2 2 2 c ---[ 46]---> Sorter-cost: 2487 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 c ---[ 45]---> Sorter-cost: 2045 Base: 5 2 2 2 2 2 2 2 2 2 c ---[ 44]---> Sorter-cost: 223 Base: 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 590 Base: 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 538 Base: 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 1025 Base: 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 1211 Base: 2 2 2 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 1390 Base: 2 2 2 2 2 2 2 2 c ---[ 38]---> BDD-cost: 3 c ---[ 37]---> BDD-cost: 3 c ---[ 36]---> BDD-cost: 3 c ---[ 34]---> Adder-cost: 304 maxlim: 2309043 bits: 22/22 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: 10 c ---[ 26]---> BDD-cost: 10 c ---[ 25]---> BDD-cost: 3 c ---[ 24]---> BDD-cost: 3 c ---[ 22]---> Adder-cost: 304 maxlim: 2104243 bits: 22/22 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 3 c ---[ 19]---> BDD-cost: 10 c ---[ 18]---> BDD-cost: 10 c ---[ 17]---> BDD-cost: 3 c ---[ 16]---> BDD-cost: 3 c ---[ 15]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 3 c ---[ 13]---> BDD-cost: 10 c ---[ 12]---> BDD-cost: 10 c ---[ 10]---> Adder-cost: 304 maxlim: 2104243 bits: 22/22 c ---[ 9]---> BDD-cost: 3 c ---[ 7]---> BDD-cost: 10 c ---[ 6]---> BDD-cost: 3 c ---[ 5]---> BDD-cost: 3 c ---[ 4]---> BDD-cost: 3 c ---[ 3]---> BDD-cost: 10 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 | 171008 465207 | 57002 0 0 nan | 0.000 % | c | 100 | 171008 465207 | 62702 100 499 5.0 | 5.013 % | c | 250 | 170886 464914 | 68972 244 1124 4.6 | 5.070 % | c | 475 | 170813 464741 | 75869 466 2110 4.5 | 5.105 % | c | 812 | 170740 464545 | 83456 796 3945 5.0 | 5.135 % | c | 1318 | 170629 464285 | 91802 1296 7491 5.8 | 5.187 % | c | 2077 | 170483 463926 | 100982 2041 14010 6.9 | 5.252 % | c | 3217 | 170393 463696 | 111080 3174 25960 8.2 | 5.288 % | c | 4925 | 170357 463613 | 122188 4875 45072 9.2 | 5.309 % | c | 7488 | 170331 463525 | 134407 7437 85705 11.5 | 5.313 % | c | 11333 | 170217 463181 | 147848 11272 148411 13.2 | 5.346 % | c | 17099 | 169976 462627 | 162633 16981 268977 15.8 | 5.479 % | c | 25748 | 169586 461746 | 178896 25600 514983 20.1 | 5.667 % | c | 38723 | 169146 460673 | 196786 38534 879620 22.8 | 5.892 % | c | 58186 | 168711 459667 | 216465 57904 1288588 22.3 | 6.129 % | c | 87379 | 168291 458443 | 238111 87052 2301755 26.4 | 6.272 % | c | 131168 | 167638 456662 | 261922 130676 3553582 27.2 | 6.548 % | c | 196853 | 167418 456154 | 288114 196348 5992264 30.5 | 6.660 % | c | 295383 | 167029 455103 | 316926 25590 607141 23.7 | 6.815 % | c | 443173 | 166301 453298 | 348619 173304 6043059 34.9 | 7.176 % |
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/28362/stat): 28362 (minisat+_script) R 28361 28362 6872 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793563661 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/28362/statm): 174 3 169 147 0 27 0 [pid=28362] 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=28363 New process pid=28364 New process pid=28365 execve syscall for /bin/sed executable One traced child (pid=28364) 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=28365) exited with status: 0 One traced child (pid=28363) exited with status: 0 New process pid=28366 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-vpm2.opb [startup+10.0042 s] Raw data (loadavg): 0.49 0.53 0.40 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 4791 0 2 0 941 22 0 0 25 0 1 0 1793563667 21004288 4594 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 5128 4594 145 145 0 4983 0 [pid=28366] vsize: 20512 Current children cumulated CPU time (s) 9.64 Current children cumulated vsize (Kb) 22636 [startup+20.005 s] Raw data (loadavg): 0.57 0.54 0.40 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 5229 0 2 0 1934 25 0 0 25 0 1 0 1793563667 22843392 5032 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 5577 5032 145 145 0 5432 0 [pid=28366] vsize: 22308 Current children cumulated CPU time (s) 19.6 Current children cumulated vsize (Kb) 24432 [startup+30.0057 s] Raw data (loadavg): 0.64 0.56 0.41 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 5627 0 2 0 2925 29 0 0 25 0 1 0 1793563667 24432640 5430 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 5965 5430 145 145 0 5820 0 [pid=28366] vsize: 23860 Current children cumulated CPU time (s) 29.55 Current children cumulated vsize (Kb) 25984 [startup+40.0073 s] Raw data (loadavg): 0.69 0.57 0.41 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 5997 0 2 0 3919 31 0 0 25 0 1 0 1793563667 26034176 5800 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 6356 5800 145 145 0 6211 0 [pid=28366] vsize: 25424 Current children cumulated CPU time (s) 39.51 Current children cumulated vsize (Kb) 27548 [startup+50.008 s] Raw data (loadavg): 0.74 0.59 0.42 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 6349 0 2 0 4912 34 0 0 25 0 1 0 1793563667 27418624 6152 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 6694 6152 145 145 0 6549 0 [pid=28366] vsize: 26776 Current children cumulated CPU time (s) 49.47 Current children cumulated vsize (Kb) 28900 [startup+60.0087 s] Raw data (loadavg): 0.78 0.60 0.43 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 6805 0 2 0 5906 37 0 0 25 0 1 0 1793563667 29229056 6608 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 7136 6608 145 145 0 6991 0 [pid=28366] vsize: 28544 Current children cumulated CPU time (s) 59.44 Current children cumulated vsize (Kb) 30668 [startup+70.0094 s] Raw data (loadavg): 0.81 0.61 0.43 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 7136 0 2 0 6900 39 0 0 25 0 1 0 1793563667 30826496 6939 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 7526 6939 145 145 0 7381 0 [pid=28366] vsize: 30104 Current children cumulated CPU time (s) 69.4 Current children cumulated vsize (Kb) 32228 [startup+80.0101 s] Raw data (loadavg): 0.84 0.62 0.44 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 7405 0 2 0 7896 42 0 0 25 0 1 0 1793563667 31899648 7208 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 7788 7208 145 145 0 7643 0 [pid=28366] vsize: 31152 Current children cumulated CPU time (s) 79.39 Current children cumulated vsize (Kb) 33276 [startup+90.0108 s] Raw data (loadavg): 0.86 0.64 0.44 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 7701 0 2 0 8890 44 0 0 25 0 1 0 1793563667 33099776 7504 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 8081 7504 145 145 0 7936 0 [pid=28366] vsize: 32324 Current children cumulated CPU time (s) 89.35 Current children cumulated vsize (Kb) 34448 [startup+100.012 s] Raw data (loadavg): 0.89 0.65 0.45 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 7990 0 2 0 9885 46 0 0 25 0 1 0 1793563667 34254848 7793 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 8363 7793 145 145 0 8218 0 [pid=28366] vsize: 33452 Current children cumulated CPU time (s) 99.32 Current children cumulated vsize (Kb) 35576 [startup+110.013 s] Raw data (loadavg): 0.90 0.66 0.46 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 8264 0 2 0 10880 49 0 0 25 0 1 0 1793563667 35348480 8067 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 8630 8067 145 145 0 8485 0 [pid=28366] vsize: 34520 Current children cumulated CPU time (s) 109.3 Current children cumulated vsize (Kb) 36644 [startup+120.014 s] Raw data (loadavg): 0.92 0.67 0.46 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 8474 0 2 0 11877 51 0 0 25 0 1 0 1793563667 36196352 8277 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 8837 8277 145 145 0 8692 0 [pid=28366] vsize: 35348 Current children cumulated CPU time (s) 119.29 Current children cumulated vsize (Kb) 37472 [startup+130.015 s] Raw data (loadavg): 0.93 0.68 0.47 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 8733 0 2 0 12874 52 0 0 25 0 1 0 1793563667 37216256 8536 4294967295 134512640 135094434 3221224448 3221223108 134553487 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 9086 8536 145 145 0 8941 0 [pid=28366] vsize: 36344 Current children cumulated CPU time (s) 129.27 Current children cumulated vsize (Kb) 38468 [startup+140.015 s] Raw data (loadavg): 0.94 0.69 0.47 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 9067 0 2 0 13868 55 0 0 25 0 1 0 1793563667 38539264 8870 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 9409 8870 145 145 0 9264 0 [pid=28366] vsize: 37636 Current children cumulated CPU time (s) 139.24 Current children cumulated vsize (Kb) 39760 [startup+150.016 s] Raw data (loadavg): 0.95 0.70 0.48 1/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) T 28362 28362 6872 0 -1 0 9332 0 2 0 14863 56 0 0 25 0 1 0 1793563667 39600128 9135 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/28366/statm): 9668 9135 145 145 0 9523 0 [pid=28366] vsize: 38672 Current children cumulated CPU time (s) 149.2 Current children cumulated vsize (Kb) 40796 [startup+160.018 s] Raw data (loadavg): 0.96 0.71 0.48 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 9563 0 2 0 15858 59 0 0 25 0 1 0 1793563667 40521728 9366 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 9893 9366 145 145 0 9748 0 [pid=28366] vsize: 39572 Current children cumulated CPU time (s) 159.18 Current children cumulated vsize (Kb) 41696 [startup+170.018 s] Raw data (loadavg): 0.96 0.72 0.49 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 9750 0 2 0 16854 61 0 0 25 0 1 0 1793563667 41816064 9553 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 10209 9553 145 145 0 10064 0 [pid=28366] vsize: 40836 Current children cumulated CPU time (s) 169.16 Current children cumulated vsize (Kb) 42960 [startup+180.018 s] Raw data (loadavg): 0.97 0.73 0.49 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 9987 0 2 0 17850 63 0 0 25 0 1 0 1793563667 42770432 9790 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 10442 9790 145 145 0 10297 0 [pid=28366] vsize: 41768 Current children cumulated CPU time (s) 179.14 Current children cumulated vsize (Kb) 43892 [startup+190.02 s] Raw data (loadavg): 0.97 0.74 0.50 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10131 0 2 0 18847 64 0 0 25 0 1 0 1793563667 43356160 9934 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 10585 9934 145 145 0 10440 0 [pid=28366] vsize: 42340 Current children cumulated CPU time (s) 189.12 Current children cumulated vsize (Kb) 44464 [startup+200.021 s] Raw data (loadavg): 0.98 0.74 0.50 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10348 0 2 0 19843 66 0 0 25 0 1 0 1793563667 44228608 10151 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 10798 10151 145 145 0 10653 0 [pid=28366] vsize: 43192 Current children cumulated CPU time (s) 199.1 Current children cumulated vsize (Kb) 45316 [startup+210.021 s] Raw data (loadavg): 0.98 0.75 0.50 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10636 0 2 0 20837 70 0 0 25 0 1 0 1793563667 45379584 10439 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 11079 10439 145 145 0 10934 0 [pid=28366] vsize: 44316 Current children cumulated CPU time (s) 209.08 Current children cumulated vsize (Kb) 46440 [startup+220.023 s] Raw data (loadavg): 0.98 0.76 0.51 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10804 0 2 0 21833 72 0 0 25 0 1 0 1793563667 46067712 10607 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 11247 10607 145 145 0 11102 0 [pid=28366] vsize: 44988 Current children cumulated CPU time (s) 219.06 Current children cumulated vsize (Kb) 47112 [startup+230.024 s] Raw data (loadavg): 0.98 0.77 0.51 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10960 0 2 0 22830 74 0 0 25 0 1 0 1793563667 46702592 10763 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 11402 10763 145 145 0 11257 0 [pid=28366] vsize: 45608 Current children cumulated CPU time (s) 229.05 Current children cumulated vsize (Kb) 47732 [startup+240.024 s] Raw data (loadavg): 0.99 0.77 0.52 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 11124 0 2 0 23826 75 0 0 25 0 1 0 1793563667 47374336 10927 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 11566 10927 145 145 0 11421 0 [pid=28366] vsize: 46264 Current children cumulated CPU time (s) 239.02 Current children cumulated vsize (Kb) 48388 [startup+250.025 s] Raw data (loadavg): 0.99 0.78 0.52 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 11314 0 2 0 24822 76 0 0 25 0 1 0 1793563667 48136192 11117 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 11752 11117 145 145 0 11607 0 [pid=28366] vsize: 47008 Current children cumulated CPU time (s) 248.99 Current children cumulated vsize (Kb) 49132 [startup+260.026 s] Raw data (loadavg): 0.99 0.79 0.53 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 11543 0 2 0 25818 79 0 0 25 0 1 0 1793563667 49061888 11346 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 11978 11346 145 145 0 11833 0 [pid=28366] vsize: 47912 Current children cumulated CPU time (s) 258.98 Current children cumulated vsize (Kb) 50036 [startup+270.026 s] Raw data (loadavg): 0.99 0.79 0.53 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 11709 0 2 0 26815 80 0 0 25 0 1 0 1793563667 49717248 11512 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 12138 11512 145 145 0 11993 0 [pid=28366] vsize: 48552 Current children cumulated CPU time (s) 268.96 Current children cumulated vsize (Kb) 50676 [startup+280.027 s] Raw data (loadavg): 0.99 0.80 0.54 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12027 0 2 0 27809 83 0 0 25 0 1 0 1793563667 50991104 11830 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 12449 11830 145 145 0 12304 0 [pid=28366] vsize: 49796 Current children cumulated CPU time (s) 278.93 Current children cumulated vsize (Kb) 51920 [startup+290.028 s] Raw data (loadavg): 0.99 0.81 0.54 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12288 0 2 0 28805 85 0 0 25 0 1 0 1793563667 52043776 12091 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 12706 12091 145 145 0 12561 0 [pid=28366] vsize: 50824 Current children cumulated CPU time (s) 288.91 Current children cumulated vsize (Kb) 52948 [startup+300.027 s] Raw data (loadavg): 0.99 0.81 0.55 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12496 0 2 0 29801 86 0 0 25 0 1 0 1793563667 52899840 12299 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 12915 12299 145 145 0 12770 0 [pid=28366] vsize: 51660 Current children cumulated CPU time (s) 298.88 Current children cumulated vsize (Kb) 53784 [startup+310.028 s] Raw data (loadavg): 0.99 0.82 0.55 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12689 0 2 0 30798 88 0 0 25 0 1 0 1793563667 53682176 12492 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 13106 12492 145 145 0 12961 0 [pid=28366] vsize: 52424 Current children cumulated CPU time (s) 308.87 Current children cumulated vsize (Kb) 54548 [startup+320.029 s] Raw data (loadavg): 0.99 0.82 0.56 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12888 0 2 0 31794 89 0 0 25 0 1 0 1793563667 54489088 12691 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 13303 12691 145 145 0 13158 0 [pid=28366] vsize: 53212 Current children cumulated CPU time (s) 318.84 Current children cumulated vsize (Kb) 55336 [startup+330.029 s] Raw data (loadavg): 0.99 0.83 0.56 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13046 0 2 0 32792 91 0 0 25 0 1 0 1793563667 55132160 12849 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 13460 12849 145 145 0 13315 0 [pid=28366] vsize: 53840 Current children cumulated CPU time (s) 328.84 Current children cumulated vsize (Kb) 55964 [startup+340.029 s] Raw data (loadavg): 0.99 0.83 0.56 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13227 0 2 0 33789 92 0 0 25 0 1 0 1793563667 55840768 13030 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 13633 13030 145 145 0 13488 0 [pid=28366] vsize: 54532 Current children cumulated CPU time (s) 338.82 Current children cumulated vsize (Kb) 56656 [startup+350.03 s] Raw data (loadavg): 0.99 0.84 0.57 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13342 0 2 0 34787 93 0 0 25 0 1 0 1793563667 56299520 13145 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 13745 13145 145 145 0 13600 0 [pid=28366] vsize: 54980 Current children cumulated CPU time (s) 348.81 Current children cumulated vsize (Kb) 57104 [startup+360.031 s] Raw data (loadavg): 0.99 0.84 0.57 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13499 0 2 0 35785 94 0 0 25 0 1 0 1793563667 56946688 13302 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 13903 13302 145 145 0 13758 0 [pid=28366] vsize: 55612 Current children cumulated CPU time (s) 358.8 Current children cumulated vsize (Kb) 57736 [startup+370.031 s] Raw data (loadavg): 0.99 0.85 0.58 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13626 0 2 0 36783 95 0 0 25 0 1 0 1793563667 57462784 13429 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 14029 13429 145 145 0 13884 0 [pid=28366] vsize: 56116 Current children cumulated CPU time (s) 368.79 Current children cumulated vsize (Kb) 58240 [startup+380.031 s] Raw data (loadavg): 0.99 0.85 0.58 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13859 0 2 0 37780 96 0 0 25 0 1 0 1793563667 58413056 13662 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 14261 13662 145 145 0 14116 0 [pid=28366] vsize: 57044 Current children cumulated CPU time (s) 378.77 Current children cumulated vsize (Kb) 59168 [startup+390.032 s] Raw data (loadavg): 0.99 0.86 0.58 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14098 0 2 0 38777 98 0 0 25 0 1 0 1793563667 59375616 13901 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 14496 13901 145 145 0 14351 0 [pid=28366] vsize: 57984 Current children cumulated CPU time (s) 388.76 Current children cumulated vsize (Kb) 60108 [startup+400.033 s] Raw data (loadavg): 0.99 0.86 0.59 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14386 0 2 0 39771 100 0 0 25 0 1 0 1793563667 60538880 14189 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 14780 14189 145 145 0 14635 0 [pid=28366] vsize: 59120 Current children cumulated CPU time (s) 398.72 Current children cumulated vsize (Kb) 61244 [startup+410.033 s] Raw data (loadavg): 0.99 0.87 0.59 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14671 0 2 0 40767 102 0 0 25 0 1 0 1793563667 61702144 14474 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 15064 14474 145 145 0 14919 0 [pid=28366] vsize: 60256 Current children cumulated CPU time (s) 408.7 Current children cumulated vsize (Kb) 62380 [startup+420.034 s] Raw data (loadavg): 0.99 0.87 0.60 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14872 0 2 0 41764 104 0 0 25 0 1 0 1793563667 62513152 14675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 15262 14675 145 145 0 15117 0 [pid=28366] vsize: 61048 Current children cumulated CPU time (s) 418.69 Current children cumulated vsize (Kb) 63172 [startup+430.035 s] Raw data (loadavg): 0.99 0.87 0.60 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14980 0 2 0 42762 105 0 0 25 0 1 0 1793563667 62971904 14783 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 15374 14783 145 145 0 15229 0 [pid=28366] vsize: 61496 Current children cumulated CPU time (s) 428.68 Current children cumulated vsize (Kb) 63620 [startup+440.035 s] Raw data (loadavg): 0.99 0.88 0.60 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15115 0 2 0 43761 106 0 0 25 0 1 0 1793563667 63508480 14918 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 15505 14918 145 145 0 15360 0 [pid=28366] vsize: 62020 Current children cumulated CPU time (s) 438.68 Current children cumulated vsize (Kb) 64144 [startup+450.036 s] Raw data (loadavg): 0.99 0.88 0.61 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15263 0 2 0 44759 107 0 0 25 0 1 0 1793563667 64139264 15066 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 15659 15066 145 145 0 15514 0 [pid=28366] vsize: 62636 Current children cumulated CPU time (s) 448.67 Current children cumulated vsize (Kb) 64760 [startup+460.038 s] Raw data (loadavg): 0.99 0.88 0.61 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15348 0 2 0 45757 108 0 0 25 0 1 0 1793563667 64499712 15151 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 15747 15151 145 145 0 15602 0 [pid=28366] vsize: 62988 Current children cumulated CPU time (s) 458.66 Current children cumulated vsize (Kb) 65112 [startup+470.038 s] Raw data (loadavg): 0.99 0.89 0.61 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15437 0 2 0 46756 109 0 0 25 0 1 0 1793563667 64872448 15240 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 15838 15240 145 145 0 15693 0 [pid=28366] vsize: 63352 Current children cumulated CPU time (s) 468.66 Current children cumulated vsize (Kb) 65476 [startup+480.038 s] Raw data (loadavg): 0.99 0.89 0.62 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15522 0 2 0 47755 109 0 0 25 0 1 0 1793563667 65224704 15325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 15924 15325 145 145 0 15779 0 [pid=28366] vsize: 63696 Current children cumulated CPU time (s) 478.65 Current children cumulated vsize (Kb) 65820 [startup+490.04 s] Raw data (loadavg): 0.99 0.89 0.62 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15607 0 2 0 48754 110 0 0 25 0 1 0 1793563667 65589248 15410 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 16013 15410 145 145 0 15868 0 [pid=28366] vsize: 64052 Current children cumulated CPU time (s) 488.65 Current children cumulated vsize (Kb) 66176 [startup+500.041 s] Raw data (loadavg): 0.99 0.90 0.63 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15746 0 2 0 49752 111 0 0 25 0 1 0 1793563667 66142208 15549 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 16148 15549 145 145 0 16003 0 [pid=28366] vsize: 64592 Current children cumulated CPU time (s) 498.64 Current children cumulated vsize (Kb) 66716 [startup+510.041 s] Raw data (loadavg): 0.99 0.90 0.63 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15893 0 2 0 50749 112 0 0 25 0 1 0 1793563667 66736128 15696 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 16293 15696 145 145 0 16148 0 [pid=28366] vsize: 65172 Current children cumulated CPU time (s) 508.62 Current children cumulated vsize (Kb) 67296 [startup+520.043 s] Raw data (loadavg): 0.99 0.90 0.63 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16033 0 2 0 51747 114 0 0 25 0 1 0 1793563667 67309568 15836 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 16433 15836 145 145 0 16288 0 [pid=28366] vsize: 65732 Current children cumulated CPU time (s) 518.62 Current children cumulated vsize (Kb) 67856 [startup+530.043 s] Raw data (loadavg): 0.99 0.90 0.64 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16179 0 2 0 52745 115 0 0 25 0 1 0 1793563667 67907584 15982 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 16579 15982 145 145 0 16434 0 [pid=28366] vsize: 66316 Current children cumulated CPU time (s) 528.61 Current children cumulated vsize (Kb) 68440 [startup+540.043 s] Raw data (loadavg): 0.99 0.91 0.64 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16460 0 2 0 53740 116 0 0 25 0 1 0 1793563667 70078464 16263 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 17109 16263 145 145 0 16964 0 [pid=28366] vsize: 68436 Current children cumulated CPU time (s) 538.57 Current children cumulated vsize (Kb) 70560 [startup+550.044 s] Raw data (loadavg): 0.99 0.91 0.64 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16617 0 2 0 54737 117 0 0 25 0 1 0 1793563667 70705152 16420 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 17262 16420 145 145 0 17117 0 [pid=28366] vsize: 69048 Current children cumulated CPU time (s) 548.55 Current children cumulated vsize (Kb) 71172 [startup+560.046 s] Raw data (loadavg): 0.99 0.91 0.65 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16719 0 2 0 55735 119 0 0 25 0 1 0 1793563667 71131136 16522 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 17366 16522 145 145 0 17221 0 [pid=28366] vsize: 69464 Current children cumulated CPU time (s) 558.55 Current children cumulated vsize (Kb) 71588 [startup+570.046 s] Raw data (loadavg): 0.99 0.91 0.65 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16912 0 2 0 56732 120 0 0 25 0 1 0 1793563667 71913472 16715 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 17557 16715 145 145 0 17412 0 [pid=28366] vsize: 70228 Current children cumulated CPU time (s) 568.53 Current children cumulated vsize (Kb) 72352 [startup+580.047 s] Raw data (loadavg): 0.99 0.92 0.65 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17087 0 2 0 57729 121 0 0 25 0 1 0 1793563667 72613888 16890 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 17728 16890 145 145 0 17583 0 [pid=28366] vsize: 70912 Current children cumulated CPU time (s) 578.51 Current children cumulated vsize (Kb) 73036 [startup+590.048 s] Raw data (loadavg): 0.99 0.92 0.66 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17260 0 2 0 58725 122 0 0 25 0 1 0 1793563667 73314304 17063 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 17899 17063 145 145 0 17754 0 [pid=28366] vsize: 71596 Current children cumulated CPU time (s) 588.48 Current children cumulated vsize (Kb) 73720 [startup+600.048 s] Raw data (loadavg): 0.99 0.92 0.66 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17445 0 2 0 59722 123 0 0 25 0 1 0 1793563667 74047488 17248 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18078 17248 145 145 0 17933 0 [pid=28366] vsize: 72312 Current children cumulated CPU time (s) 598.46 Current children cumulated vsize (Kb) 74436 [startup+610.048 s] Raw data (loadavg): 0.99 0.92 0.66 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17579 0 2 0 60719 124 0 0 25 0 1 0 1793563667 74588160 17382 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18210 17382 145 145 0 18065 0 [pid=28366] vsize: 72840 Current children cumulated CPU time (s) 608.44 Current children cumulated vsize (Kb) 74964 [startup+620.049 s] Raw data (loadavg): 0.99 0.92 0.66 1/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) T 28362 28362 6872 0 -1 0 17707 0 2 0 61717 125 0 0 25 0 1 0 1793563667 75128832 17510 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18342 17510 145 145 0 18197 0 [pid=28366] vsize: 73368 Current children cumulated CPU time (s) 618.43 Current children cumulated vsize (Kb) 75492 [startup+630.05 s] Raw data (loadavg): 0.99 0.93 0.67 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 62716 126 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 628.43 Current children cumulated vsize (Kb) 75696 [startup+640.05 s] Raw data (loadavg): 0.99 0.93 0.67 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 63716 126 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 638.43 Current children cumulated vsize (Kb) 75696 [startup+650.051 s] Raw data (loadavg): 0.99 0.93 0.67 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 64715 126 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 648.42 Current children cumulated vsize (Kb) 75696 [startup+660.053 s] Raw data (loadavg): 0.99 0.93 0.68 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 65715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 658.43 Current children cumulated vsize (Kb) 75696 [startup+670.053 s] Raw data (loadavg): 0.99 0.93 0.68 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 66715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 668.43 Current children cumulated vsize (Kb) 75696 [startup+680.053 s] Raw data (loadavg): 0.99 0.94 0.68 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 67715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 678.43 Current children cumulated vsize (Kb) 75696 [startup+690.054 s] Raw data (loadavg): 0.99 0.94 0.68 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 68715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 688.43 Current children cumulated vsize (Kb) 75696 [startup+700.054 s] Raw data (loadavg): 0.99 0.94 0.69 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 69715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 698.43 Current children cumulated vsize (Kb) 75696 [startup+710.055 s] Raw data (loadavg): 0.99 0.94 0.69 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 70716 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 708.44 Current children cumulated vsize (Kb) 75696 [startup+720.056 s] Raw data (loadavg): 0.99 0.94 0.69 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 71716 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 718.44 Current children cumulated vsize (Kb) 75696 [startup+730.057 s] Raw data (loadavg): 0.99 0.94 0.70 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 72716 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 728.44 Current children cumulated vsize (Kb) 75696 [startup+740.057 s] Raw data (loadavg): 0.99 0.94 0.70 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 73716 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 738.44 Current children cumulated vsize (Kb) 75696 [startup+750.058 s] Raw data (loadavg): 0.99 0.95 0.70 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 74717 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 748.45 Current children cumulated vsize (Kb) 75696 [startup+760.06 s] Raw data (loadavg): 0.99 0.95 0.71 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 75717 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 758.45 Current children cumulated vsize (Kb) 75696 [startup+770.06 s] Raw data (loadavg): 0.99 0.95 0.71 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17762 0 2 0 76717 127 0 0 25 0 1 0 1793563667 75337728 17565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17565 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 768.45 Current children cumulated vsize (Kb) 75696 [startup+780.061 s] Raw data (loadavg): 0.99 0.95 0.71 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17762 0 2 0 77717 127 0 0 25 0 1 0 1793563667 75337728 17565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17565 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 778.45 Current children cumulated vsize (Kb) 75696 [startup+790.062 s] Raw data (loadavg): 0.99 0.95 0.71 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17762 0 2 0 78718 127 0 0 25 0 1 0 1793563667 75337728 17565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17565 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 788.46 Current children cumulated vsize (Kb) 75696 [startup+800.062 s] Raw data (loadavg): 0.99 0.95 0.72 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 79718 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223072 134557653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 798.46 Current children cumulated vsize (Kb) 75696 [startup+810.063 s] Raw data (loadavg): 0.99 0.95 0.72 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 80718 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 808.46 Current children cumulated vsize (Kb) 75696 [startup+820.064 s] Raw data (loadavg): 0.99 0.95 0.72 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 81718 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 818.46 Current children cumulated vsize (Kb) 75696 [startup+830.065 s] Raw data (loadavg): 0.99 0.95 0.73 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 82719 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 828.47 Current children cumulated vsize (Kb) 75696 [startup+840.065 s] Raw data (loadavg): 0.99 0.95 0.73 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 83719 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223104 134558172 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 838.47 Current children cumulated vsize (Kb) 75696 [startup+850.066 s] Raw data (loadavg): 0.99 0.96 0.73 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17764 0 2 0 84719 127 0 0 25 0 1 0 1793563667 75337728 17567 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17567 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 848.47 Current children cumulated vsize (Kb) 75696 [startup+860.067 s] Raw data (loadavg): 0.99 0.96 0.73 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17764 0 2 0 85719 127 0 0 25 0 1 0 1793563667 75337728 17567 4294967295 134512640 135094434 3221224448 3221223060 134563069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17567 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 858.47 Current children cumulated vsize (Kb) 75696 [startup+870.067 s] Raw data (loadavg): 0.99 0.96 0.73 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 86720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 868.48 Current children cumulated vsize (Kb) 75696 [startup+880.068 s] Raw data (loadavg): 0.99 0.96 0.74 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 87720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 878.48 Current children cumulated vsize (Kb) 75696 [startup+890.069 s] Raw data (loadavg): 0.99 0.96 0.74 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 88720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223104 134557829 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 888.48 Current children cumulated vsize (Kb) 75696 [startup+900.07 s] Raw data (loadavg): 0.99 0.96 0.74 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 89720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 898.48 Current children cumulated vsize (Kb) 75696 [startup+910.071 s] Raw data (loadavg): 0.99 0.96 0.74 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 90720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 908.48 Current children cumulated vsize (Kb) 75696 [startup+920.072 s] Raw data (loadavg): 0.99 0.96 0.74 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 91720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 918.48 Current children cumulated vsize (Kb) 75696 [startup+930.073 s] Raw data (loadavg): 0.99 0.96 0.75 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17766 0 2 0 92720 127 0 0 25 0 1 0 1793563667 75337728 17569 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17569 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 928.48 Current children cumulated vsize (Kb) 75696 [startup+940.073 s] Raw data (loadavg): 0.99 0.96 0.75 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17768 0 2 0 93721 127 0 0 25 0 1 0 1793563667 75337728 17571 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17571 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 938.49 Current children cumulated vsize (Kb) 75696 [startup+950.074 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17768 0 2 0 94721 127 0 0 25 0 1 0 1793563667 75337728 17571 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17571 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 948.49 Current children cumulated vsize (Kb) 75696 [startup+960.075 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17768 0 2 0 95721 127 0 0 25 0 1 0 1793563667 75337728 17571 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17571 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 958.49 Current children cumulated vsize (Kb) 75696 [startup+970.075 s] Raw data (loadavg): 0.99 0.97 0.75 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 96721 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 968.49 Current children cumulated vsize (Kb) 75696 [startup+980.075 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 97722 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 978.5 Current children cumulated vsize (Kb) 75696 [startup+990.076 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 98722 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 988.5 Current children cumulated vsize (Kb) 75696 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 99722 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 998.5 Current children cumulated vsize (Kb) 75696 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 100722 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1008.5 Current children cumulated vsize (Kb) 75696 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.76 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 101723 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1018.51 Current children cumulated vsize (Kb) 75696 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 102723 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1028.51 Current children cumulated vsize (Kb) 75696 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17770 0 2 0 103723 127 0 0 25 0 1 0 1793563667 75337728 17573 4294967295 134512640 135094434 3221224448 3221223040 134557232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17573 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1038.51 Current children cumulated vsize (Kb) 75696 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 104723 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1048.51 Current children cumulated vsize (Kb) 75696 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 105724 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1058.52 Current children cumulated vsize (Kb) 75696 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.77 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 106724 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1068.52 Current children cumulated vsize (Kb) 75696 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 107724 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1078.52 Current children cumulated vsize (Kb) 75696 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 108724 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1088.52 Current children cumulated vsize (Kb) 75696 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17772 0 2 0 109725 127 0 0 25 0 1 0 1793563667 75337728 17575 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17575 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1098.53 Current children cumulated vsize (Kb) 75696 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17772 0 2 0 110725 127 0 0 25 0 1 0 1793563667 75337728 17575 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17575 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1108.53 Current children cumulated vsize (Kb) 75696 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.78 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17772 0 2 0 111725 127 0 0 25 0 1 0 1793563667 75337728 17575 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17575 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1118.53 Current children cumulated vsize (Kb) 75696 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17773 0 2 0 112725 127 0 0 25 0 1 0 1793563667 75337728 17576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17576 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1128.53 Current children cumulated vsize (Kb) 75696 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17773 0 2 0 113726 127 0 0 25 0 1 0 1793563667 75337728 17576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17576 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1138.54 Current children cumulated vsize (Kb) 75696 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17773 0 2 0 114726 127 0 0 25 0 1 0 1793563667 75337728 17576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17576 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1148.54 Current children cumulated vsize (Kb) 75696 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17773 0 2 0 115726 127 0 0 25 0 1 0 1793563667 75337728 17576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18393 17576 145 145 0 18248 0 [pid=28366] vsize: 73572 Current children cumulated CPU time (s) 1158.54 Current children cumulated vsize (Kb) 75696 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17851 0 2 0 116725 127 0 0 25 0 1 0 1793563667 75657216 17654 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18471 17654 145 145 0 18326 0 [pid=28366] vsize: 73884 Current children cumulated CPU time (s) 1168.53 Current children cumulated vsize (Kb) 76008 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.79 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17959 0 2 0 117723 129 0 0 25 0 1 0 1793563667 76111872 17762 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18582 17762 145 145 0 18437 0 [pid=28366] vsize: 74328 Current children cumulated CPU time (s) 1178.53 Current children cumulated vsize (Kb) 76452 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 18059 0 2 0 118722 129 0 0 25 0 1 0 1793563667 76517376 17862 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18681 17862 145 145 0 18536 0 [pid=28366] vsize: 74724 Current children cumulated CPU time (s) 1188.52 Current children cumulated vsize (Kb) 76848 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 18235 0 2 0 119719 130 0 0 25 0 1 0 1793563667 77238272 18038 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 18857 18038 145 145 0 18712 0 [pid=28366] vsize: 75428 Current children cumulated CPU time (s) 1198.5 Current children cumulated vsize (Kb) 77552 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 18579 0 2 0 120714 132 0 0 25 0 1 0 1793563667 78647296 18382 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 19201 18382 145 145 0 19056 0 [pid=28366] vsize: 76804 Current children cumulated CPU time (s) 1208.47 Current children cumulated vsize (Kb) 78928 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.80 2/57 28366 Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28362/statm): 531 226 485 147 0 384 0 [pid=28362] vsize: 2124 Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 18579 0 2 0 120714 132 0 0 25 0 1 0 1793563667 78647296 18382 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28366/statm): 19201 18382 145 145 0 19056 0 [pid=28366] vsize: 76804 Current children cumulated CPU time (s) 1208.47 Current children cumulated vsize (Kb) 78928 Sending SIGTERM to -28362 Sleeping 2 seconds One traced child (pid=28362) ended because it received signal 15 (SIGTERM) One traced child (pid=28366) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1208.5 CPU user time (s): 1207.14 CPU system time (s): 1.35579 CPU usage (%): 99.8651 Max. virtual memory (cumulated for all children) (Kb): 78928
ERROR: no interpretation found !