Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-vpm1.opb |
MD5SUM | 9d68724ddc6098af63bcc619f21688cc |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 28 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 168 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 168 |
Number of bits of the sum of numbers in the objective function | 8 |
Biggest number in a constraint | 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 | 1249.78 |
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 | 82 |
LAUNCH ON wulflinc17 THE 2005-09-19 03:26:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2892 boxname=wulflinc17 idbench=548 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9d68724ddc6098af63bcc619f21688cc /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-vpm1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-vpm1.opb IDLAUNCH: 2892 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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 : 3 cpu MHz : 451.072 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: 913360 kB Buffers: 34776 kB Cached: 59364 kB SwapCached: 516 kB Active: 56748 kB Inactive: 39840 kB HighTotal: 131008 kB HighFree: 67592 kB LowTotal: 903652 kB LowFree: 845768 kB SwapTotal: 2097892 kB SwapFree: 2096672 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5680 kB Slab: 18968 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 03:46:39 (client local time) WITH STATUS 0 IN 1208.91 SECONDS stats: 2892 7 1208.91 0
c Parsing PB file... c Converting 486 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################## c -- Clauses(.)/Splits(s): (none) c ---[ 485]---> BDD-cost: 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]---> Sorter-cost: 3227 Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3 c ---[ 264]---> Sorter-cost: 3277 Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2 c ---[ 260]---> Adder-cost: 352 maxlim: 2411343 bits: 22/22 c ---[ 258]---> Adder-cost: 352 maxlim: 2411343 bits: 22/22 c ---[ 256]---> Adder-cost: 330 maxlim: 1694543 bits: 21/21 c ---[ 254]---> Adder-cost: 330 maxlim: 1694543 bits: 21/21 c ---[ 252]---> Adder-cost: 352 maxlim: 2104143 bits: 22/22 c ---[ 250]---> Sorter-cost: 2487 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 c ---[ 248]---> Adder-cost: 304 maxlim: 2309043 bits: 22/22 c ---[ 246]---> Adder-cost: 304 maxlim: 2104243 bits: 22/22 c ---[ 244]---> Adder-cost: 304 maxlim: 2104243 bits: 22/22 c ---[ 242]---> Adder-cost: 288 maxlim: 1694643 bits: 21/21 c ---[ 236]---> Sorter-cost: 2294 Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[ 234]---> Adder-cost: 312 maxlim: 2587171 bits: 22/22 c ---[ 232]---> Adder-cost: 260 maxlim: 897571 bits: 20/20 c ---[ 224]---> Sorter-cost: 2815 Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3 c ---[ 222]---> Adder-cost: 350 maxlim: 1768271 bits: 22/21 c ---[ 216]---> Adder-cost: 274 maxlim: 1228100 bits: 21/21 c ---[ 214]---> Adder-cost: 312 maxlim: 1957187 bits: 22/21 c ---[ 212]---> Adder-cost: 312 maxlim: 1854787 bits: 22/21 c ---[ 210]---> Adder-cost: 390 maxlim: 2279471 bits: 22/22 c ---[ 208]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 206]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 204]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 202]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 200]---> Sorter-cost: 3241 Base: 2 2 2 2 5 5 2 2 2 2 2 2 5 c ---[ 198]---> Adder-cost: 440 maxlim: 3713071 bits: 23/22 c ---[ 196]---> Adder-cost: 368 maxlim: 999471 bits: 21/20 c ---[ 194]---> Adder-cost: 368 maxlim: 999471 bits: 21/20 c ---[ 192]---> Adder-cost: 368 maxlim: 999471 bits: 21/20 c ---[ 191]---> BDD-cost: 48 c ---[ 190]---> Sorter-cost: 386 Base: 2 2 2 2 2 2 2 2 2 c ---[ 189]---> Sorter-cost: 400 Base: 2 2 2 2 2 2 2 2 2 c ---[ 188]---> Sorter-cost: 801 Base: 2 2 2 2 2 2 2 2 2 c ---[ 187]---> Sorter-cost: 1088 Base: 2 2 2 2 2 2 2 2 2 c ---[ 186]---> Sorter-cost: 982 Base: 2 2 2 2 2 2 2 2 2 c ---[ 185]---> BDD-cost: 48 c ---[ 184]---> Sorter-cost: 386 Base: 2 2 2 2 2 2 2 2 2 c ---[ 183]---> Sorter-cost: 400 Base: 2 2 2 2 2 2 2 2 2 c ---[ 182]---> Sorter-cost: 781 Base: 2 2 2 2 2 2 2 2 2 c ---[ 181]---> Sorter-cost: 1034 Base: 2 2 2 2 2 2 2 2 2 c ---[ 180]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 c ---[ 179]---> BDD-cost: 48 c ---[ 178]---> Sorter-cost: 386 Base: 2 2 2 2 2 2 2 2 2 c ---[ 177]---> Sorter-cost: 391 Base: 2 2 2 2 2 2 2 2 2 c ---[ 176]---> Sorter-cost: 788 Base: 2 2 2 2 2 2 2 2 2 c ---[ 175]---> Sorter-cost: 1047 Base: 2 2 2 2 2 2 2 2 2 c ---[ 174]---> Sorter-cost: 1019 Base: 2 2 2 2 2 2 2 2 2 c ---[ 173]---> BDD-cost: 48 c ---[ 172]---> Sorter-cost: 370 Base: 2 2 2 2 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 391 Base: 2 2 2 2 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 747 Base: 2 2 2 2 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 1022 Base: 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 952 Base: 2 2 2 2 2 2 2 2 2 c ---[ 167]---> BDD-cost: 3 c ---[ 166]---> BDD-cost: 3 c ---[ 165]---> BDD-cost: 3 c ---[ 164]---> BDD-cost: 3 c ---[ 163]---> BDD-cost: 3 c ---[ 162]---> BDD-cost: 3 c ---[ 161]---> BDD-cost: 3 c ---[ 160]---> BDD-cost: 3 c ---[ 159]---> BDD-cost: 3 c ---[ 158]---> BDD-cost: 10 c ---[ 157]---> BDD-cost: 10 c ---[ 156]---> BDD-cost: 3 c ---[ 155]---> BDD-cost: 3 c ---[ 154]---> BDD-cost: 3 c ---[ 153]---> BDD-cost: 3 c ---[ 152]---> BDD-cost: 10 c ---[ 151]---> BDD-cost: 10 c ---[ 150]---> BDD-cost: 3 c ---[ 149]---> BDD-cost: 3 c ---[ 148]---> BDD-cost: 3 c ---[ 147]---> BDD-cost: 3 c ---[ 146]---> BDD-cost: 10 c ---[ 145]---> BDD-cost: 10 c ---[ 144]---> BDD-cost: 3 c ---[ 142]---> BDD-cost: 10 c ---[ 141]---> BDD-cost: 3 c ---[ 140]---> BDD-cost: 3 c ---[ 139]---> BDD-cost: 3 c ---[ 138]---> BDD-cost: 10 c ---[ 136]---> BDD-cost: 3 c ---[ 135]---> BDD-cost: 3 c ---[ 134]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 3 c ---[ 132]---> BDD-cost: 3 c ---[ 130]---> BDD-cost: 3 c ---[ 129]---> BDD-cost: 3 c ---[ 128]---> BDD-cost: 3 c ---[ 127]---> BDD-cost: 3 c ---[ 126]---> BDD-cost: 3 c ---[ 124]---> BDD-cost: 10 c ---[ 123]---> BDD-cost: 3 c ---[ 122]---> BDD-cost: 3 c ---[ 121]---> BDD-cost: 3 c ---[ 120]---> BDD-cost: 10 c ---[ 116]---> BDD-cost: 10 c ---[ 115]---> BDD-cost: 3 c ---[ 114]---> BDD-cost: 9 c ---[ 110]---> BDD-cost: 10 c ---[ 109]---> BDD-cost: 3 c ---[ 108]---> BDD-cost: 9 c ---[ 104]---> BDD-cost: 3 c ---[ 103]---> BDD-cost: 3 c ---[ 102]---> BDD-cost: 9 c ---[ 98]---> BDD-cost: 10 c ---[ 97]---> BDD-cost: 3 c ---[ 96]---> BDD-cost: 9 c ---[ 91]---> BDD-cost: 3 c ---[ 90]---> BDD-cost: 3 c ---[ 85]---> BDD-cost: 10 c ---[ 84]---> BDD-cost: 3 c ---[ 79]---> BDD-cost: 3 c ---[ 78]---> BDD-cost: 3 c ---[ 73]---> BDD-cost: 3 c ---[ 72]---> BDD-cost: 3 c ---[ 68]---> BDD-cost: 3 c ---[ 67]---> BDD-cost: 3 c ---[ 66]---> BDD-cost: 3 c ---[ 62]---> BDD-cost: 3 c ---[ 61]---> BDD-cost: 3 c ---[ 60]---> BDD-cost: 3 c ---[ 56]---> BDD-cost: 3 c ---[ 55]---> BDD-cost: 3 c ---[ 54]---> BDD-cost: 3 c ---[ 50]---> BDD-cost: 3 c ---[ 49]---> BDD-cost: 3 c ---[ 48]---> BDD-cost: 3 c ---[ 47]---> BDD-cost: 3 c ---[ 46]---> BDD-cost: 3 c ---[ 45]---> BDD-cost: 9 c ---[ 44]---> BDD-cost: 9 c ---[ 43]---> BDD-cost: 9 c ---[ 42]---> BDD-cost: 9 c ---[ 41]---> BDD-cost: 3 c ---[ 40]---> BDD-cost: 10 c ---[ 39]---> BDD-cost: 9 c ---[ 38]---> BDD-cost: 9 c ---[ 37]---> BDD-cost: 9 c ---[ 36]---> BDD-cost: 9 c ---[ 35]---> BDD-cost: 3 c ---[ 34]---> BDD-cost: 10 c ---[ 33]---> BDD-cost: 8 c ---[ 32]---> BDD-cost: 8 c ---[ 31]---> BDD-cost: 8 c ---[ 30]---> BDD-cost: 8 c ---[ 29]---> BDD-cost: 3 c ---[ 28]---> BDD-cost: 10 c ---[ 27]---> BDD-cost: 8 c ---[ 26]---> BDD-cost: 8 c ---[ 25]---> BDD-cost: 8 c ---[ 24]---> BDD-cost: 8 c ---[ 22]---> BDD-cost: 10 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 9 c ---[ 19]---> BDD-cost: 9 c ---[ 18]---> BDD-cost: 9 c ---[ 16]---> BDD-cost: 10 c ---[ 15]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 9 c ---[ 13]---> BDD-cost: 9 c ---[ 12]---> BDD-cost: 9 c ---[ 10]---> BDD-cost: 10 c ---[ 9]---> BDD-cost: 3 c ---[ 8]---> BDD-cost: 9 c ---[ 7]---> BDD-cost: 9 c ---[ 6]---> BDD-cost: 9 c ---[ 4]---> BDD-cost: 9 c ---[ 3]---> BDD-cost: 3 c ---[ 2]---> BDD-cost: 8 c ---[ 1]---> BDD-cost: 8 c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 131984 372097 | 43994 0 0 nan | 0.000 % | c | 100 | 131893 371869 | 48393 95 337 3.5 | 6.825 % | c | 251 | 131833 371735 | 53232 243 1128 4.6 | 6.864 % | c | 477 | 131829 371726 | 58556 468 2452 5.2 | 6.866 % | c | 814 | 131829 371726 | 64411 805 5904 7.3 | 6.866 % | c | 1320 | 131829 371726 | 70852 1311 10060 7.7 | 6.866 % | c | 2080 | 131766 371585 | 77938 2067 16552 8.0 | 6.907 % | c | 3219 | 131743 371526 | 85731 3204 31361 9.8 | 6.920 % | c | 4927 | 131369 370664 | 94305 4894 54229 11.1 | 7.176 % | c | 7489 | 131191 370240 | 103735 7441 89422 12.0 | 7.292 % | c | 11334 | 130995 369791 | 114109 11272 134396 11.9 | 7.424 % | c | 17100 | 130634 368964 | 125520 17026 227613 13.4 | 7.656 % | c | 25749 | 130363 368341 | 138072 25650 343214 13.4 | 7.839 % | c | 38724 | 130286 368151 | 151879 38609 624446 16.2 | 7.891 % | c | 58185 | 130217 367957 | 167067 58063 1081641 18.6 | 7.930 % | c | 87378 | 129973 367396 | 183773 87223 2028744 23.3 | 8.121 % | c | 131167 | 129742 366846 | 202151 130997 3412336 26.0 | 8.296 % | c | 196851 | 129657 366617 | 222366 196649 5557731 28.3 | 8.350 % | c | 295378 | 129331 365820 | 244603 90242 2391247 26.5 | 8.577 % | c | 443167 | 128851 364608 | 269063 237959 7047781 29.6 | 8.910 % | c | 664850 | 128325 363313 | 295969 213696 6326538 29.6 | 9.280 % |
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/31050/stat): 31050 (minisat+_script) R 31049 31050 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846669924 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/31050/statm): 174 3 169 147 0 27 0 [pid=31050] 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=31051 New process pid=31052 New process pid=31053 execve syscall for /bin/sed executable One traced child (pid=31052) 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=31053) exited with status: 0 One traced child (pid=31051) exited with status: 0 New process pid=31054 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-vpm1.opb [startup+10.0032 s] Raw data (loadavg): 0.78 0.94 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 3832 0 0 0 962 17 0 0 25 0 1 0 1846669929 17592320 3668 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 4295 3668 145 145 0 4150 0 [pid=31054] vsize: 17180 Current children cumulated CPU time (s) 9.8 Current children cumulated vsize (Kb) 19304 [startup+20.0038 s] Raw data (loadavg): 0.81 0.94 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 4196 0 0 0 1957 20 0 0 25 0 1 0 1846669929 19120128 4032 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 4668 4032 145 145 0 4523 0 [pid=31054] vsize: 18672 Current children cumulated CPU time (s) 19.78 Current children cumulated vsize (Kb) 20796 [startup+30.0044 s] Raw data (loadavg): 0.84 0.94 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 4670 0 0 0 2948 23 0 0 25 0 1 0 1846669929 21131264 4506 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 5159 4506 145 145 0 5014 0 [pid=31054] vsize: 20636 Current children cumulated CPU time (s) 29.72 Current children cumulated vsize (Kb) 22760 [startup+40.0051 s] Raw data (loadavg): 0.86 0.94 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 5198 0 0 0 3938 27 0 0 25 0 1 0 1846669929 23228416 5034 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31054/statm): 5671 5034 145 145 0 5526 0 [pid=31054] vsize: 22684 Current children cumulated CPU time (s) 39.66 Current children cumulated vsize (Kb) 24808 [startup+50.0067 s] Raw data (loadavg): 0.88 0.94 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 5617 0 0 0 4928 31 0 0 25 0 1 0 1846669929 24899584 5453 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31054/statm): 6079 5453 145 145 0 5934 0 [pid=31054] vsize: 24316 Current children cumulated CPU time (s) 49.6 Current children cumulated vsize (Kb) 26440 [startup+60.0072 s] Raw data (loadavg): 0.90 0.94 0.98 1/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) T 31050 31050 19316 0 -1 0 6086 0 0 0 5920 34 0 0 25 0 1 0 1846669929 27041792 5922 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/31054/statm): 6602 5922 145 145 0 6457 0 [pid=31054] vsize: 26408 Current children cumulated CPU time (s) 59.55 Current children cumulated vsize (Kb) 28532 [startup+70.0078 s] Raw data (loadavg): 0.92 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 6382 0 0 0 6914 37 0 0 25 0 1 0 1846669929 28233728 6218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 6893 6218 145 145 0 6748 0 [pid=31054] vsize: 27572 Current children cumulated CPU time (s) 69.52 Current children cumulated vsize (Kb) 29696 [startup+80.0094 s] Raw data (loadavg): 0.93 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 6701 0 0 0 7909 38 0 0 25 0 1 0 1846669929 29540352 6537 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 7212 6537 145 145 0 7067 0 [pid=31054] vsize: 28848 Current children cumulated CPU time (s) 79.48 Current children cumulated vsize (Kb) 30972 [startup+90.01 s] Raw data (loadavg): 0.94 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7021 0 0 0 8903 41 0 0 25 0 1 0 1846669929 30834688 6857 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 7528 6857 145 145 0 7383 0 [pid=31054] vsize: 30112 Current children cumulated CPU time (s) 89.45 Current children cumulated vsize (Kb) 32236 [startup+100.011 s] Raw data (loadavg): 0.95 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7304 0 0 0 9898 43 0 0 25 0 1 0 1846669929 31977472 7140 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 7807 7140 145 145 0 7662 0 [pid=31054] vsize: 31228 Current children cumulated CPU time (s) 99.42 Current children cumulated vsize (Kb) 33352 [startup+110.012 s] Raw data (loadavg): 0.95 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7540 0 0 0 10894 44 0 0 25 0 1 0 1846669929 32911360 7376 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 8035 7376 145 145 0 7890 0 [pid=31054] vsize: 32140 Current children cumulated CPU time (s) 109.39 Current children cumulated vsize (Kb) 34264 [startup+120.013 s] Raw data (loadavg): 0.96 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7762 0 0 0 11890 46 0 0 25 0 1 0 1846669929 33824768 7598 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 8258 7598 145 145 0 8113 0 [pid=31054] vsize: 33032 Current children cumulated CPU time (s) 119.37 Current children cumulated vsize (Kb) 35156 [startup+130.013 s] Raw data (loadavg): 0.97 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 7954 0 0 0 12888 47 0 0 25 0 1 0 1846669929 34619392 7790 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 8452 7790 145 145 0 8307 0 [pid=31054] vsize: 33808 Current children cumulated CPU time (s) 129.36 Current children cumulated vsize (Kb) 35932 [startup+140.014 s] Raw data (loadavg): 0.97 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 8131 0 0 0 13886 47 0 0 25 0 1 0 1846669929 35332096 7967 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 8626 7967 145 145 0 8481 0 [pid=31054] vsize: 34504 Current children cumulated CPU time (s) 139.34 Current children cumulated vsize (Kb) 36628 [startup+150.016 s] Raw data (loadavg): 0.98 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 8291 0 0 0 14884 48 0 0 25 0 1 0 1846669929 35966976 8127 4294967295 134512640 135094434 3221224432 3221223104 134556085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 8781 8127 145 145 0 8636 0 [pid=31054] vsize: 35124 Current children cumulated CPU time (s) 149.33 Current children cumulated vsize (Kb) 37248 [startup+160.016 s] Raw data (loadavg): 0.98 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 8519 0 0 0 15880 50 0 0 25 0 1 0 1846669929 37441536 8355 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 9141 8355 145 145 0 8996 0 [pid=31054] vsize: 36564 Current children cumulated CPU time (s) 159.31 Current children cumulated vsize (Kb) 38688 [startup+170.017 s] Raw data (loadavg): 0.98 0.95 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 8823 0 0 0 16874 53 0 0 25 0 1 0 1846669929 38658048 8659 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 9438 8659 145 145 0 9293 0 [pid=31054] vsize: 37752 Current children cumulated CPU time (s) 169.28 Current children cumulated vsize (Kb) 39876 [startup+180.017 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9159 0 0 0 17869 55 0 0 25 0 1 0 1846669929 40038400 8995 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 9775 8995 145 145 0 9630 0 [pid=31054] vsize: 39100 Current children cumulated CPU time (s) 179.25 Current children cumulated vsize (Kb) 41224 [startup+190.018 s] Raw data (loadavg): 0.99 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9381 0 0 0 18865 57 0 0 25 0 1 0 1846669929 40910848 9217 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 9988 9217 145 145 0 9843 0 [pid=31054] vsize: 39952 Current children cumulated CPU time (s) 189.23 Current children cumulated vsize (Kb) 42076 [startup+200.019 s] Raw data (loadavg): 0.99 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9538 0 0 0 19863 58 0 0 25 0 1 0 1846669929 41533440 9374 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 10140 9374 145 145 0 9995 0 [pid=31054] vsize: 40560 Current children cumulated CPU time (s) 199.22 Current children cumulated vsize (Kb) 42684 [startup+210.019 s] Raw data (loadavg): 0.99 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9695 0 0 0 20860 59 0 0 25 0 1 0 1846669929 42160128 9531 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 10293 9531 145 145 0 10148 0 [pid=31054] vsize: 41172 Current children cumulated CPU time (s) 209.2 Current children cumulated vsize (Kb) 43296 [startup+220.02 s] Raw data (loadavg): 0.99 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 9848 0 0 0 21857 61 0 0 25 0 1 0 1846669929 42782720 9684 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 10445 9684 145 145 0 10300 0 [pid=31054] vsize: 41780 Current children cumulated CPU time (s) 219.19 Current children cumulated vsize (Kb) 43904 [startup+230.02 s] Raw data (loadavg): 0.99 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10003 0 0 0 22855 62 0 0 25 0 1 0 1846669929 43417600 9839 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 10600 9839 145 145 0 10455 0 [pid=31054] vsize: 42400 Current children cumulated CPU time (s) 229.18 Current children cumulated vsize (Kb) 44524 [startup+240.021 s] Raw data (loadavg): 0.99 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10138 0 0 0 23853 64 0 0 25 0 1 0 1846669929 43958272 9974 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 10732 9974 145 145 0 10587 0 [pid=31054] vsize: 42928 Current children cumulated CPU time (s) 239.18 Current children cumulated vsize (Kb) 45052 [startup+250.022 s] Raw data (loadavg): 0.99 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10267 0 0 0 24850 65 0 0 25 0 1 0 1846669929 44486656 10103 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 10861 10103 145 145 0 10716 0 [pid=31054] vsize: 43444 Current children cumulated CPU time (s) 249.16 Current children cumulated vsize (Kb) 45568 [startup+260.022 s] Raw data (loadavg): 0.99 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10386 0 0 0 25849 66 0 0 25 0 1 0 1846669929 44990464 10222 4294967295 134512640 135094434 3221224432 3221223104 134556170 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 10984 10222 145 145 0 10839 0 [pid=31054] vsize: 43936 Current children cumulated CPU time (s) 259.16 Current children cumulated vsize (Kb) 46060 [startup+270.023 s] Raw data (loadavg): 0.99 0.96 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10498 0 0 0 26847 66 0 0 25 0 1 0 1846669929 45441024 10334 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 11094 10334 145 145 0 10949 0 [pid=31054] vsize: 44376 Current children cumulated CPU time (s) 269.14 Current children cumulated vsize (Kb) 46500 [startup+280.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10619 0 0 0 27846 67 0 0 25 0 1 0 1846669929 45944832 10455 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 11217 10455 145 145 0 11072 0 [pid=31054] vsize: 44868 Current children cumulated CPU time (s) 279.14 Current children cumulated vsize (Kb) 46992 [startup+290.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10736 0 0 0 28845 68 0 0 25 0 1 0 1846669929 46440448 10572 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 11338 10572 145 145 0 11193 0 [pid=31054] vsize: 45352 Current children cumulated CPU time (s) 289.14 Current children cumulated vsize (Kb) 47476 [startup+300.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10857 0 0 0 29843 69 0 0 25 0 1 0 1846669929 46911488 10693 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 11453 10693 145 145 0 11308 0 [pid=31054] vsize: 45812 Current children cumulated CPU time (s) 299.13 Current children cumulated vsize (Kb) 47936 [startup+310.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 10973 0 0 0 30841 70 0 0 25 0 1 0 1846669929 47374336 10809 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 11566 10809 145 145 0 11421 0 [pid=31054] vsize: 46264 Current children cumulated CPU time (s) 309.12 Current children cumulated vsize (Kb) 48388 [startup+320.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11075 0 0 0 31840 70 0 0 25 0 1 0 1846669929 47816704 10911 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 11674 10911 145 145 0 11529 0 [pid=31054] vsize: 46696 Current children cumulated CPU time (s) 319.11 Current children cumulated vsize (Kb) 48820 [startup+330.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11172 0 0 0 32839 71 0 0 25 0 1 0 1846669929 48193536 11008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 11766 11008 145 145 0 11621 0 [pid=31054] vsize: 47064 Current children cumulated CPU time (s) 329.11 Current children cumulated vsize (Kb) 49188 [startup+340.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11328 0 0 0 33835 72 0 0 25 0 1 0 1846669929 48828416 11164 4294967295 134512640 135094434 3221224432 3221223104 134555957 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31054/statm): 11921 11164 145 145 0 11776 0 [pid=31054] vsize: 47684 Current children cumulated CPU time (s) 339.08 Current children cumulated vsize (Kb) 49808 [startup+350.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11588 0 0 0 34831 75 0 0 25 0 1 0 1846669929 49934336 11424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 12191 11424 145 145 0 12046 0 [pid=31054] vsize: 48764 Current children cumulated CPU time (s) 349.07 Current children cumulated vsize (Kb) 50888 [startup+360.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 11807 0 0 0 35828 76 0 0 25 0 1 0 1846669929 50892800 11643 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 12425 11643 145 145 0 12280 0 [pid=31054] vsize: 49700 Current children cumulated CPU time (s) 359.05 Current children cumulated vsize (Kb) 51824 [startup+370.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12017 0 0 0 36824 78 0 0 25 0 1 0 1846669929 51773440 11853 4294967295 134512640 135094434 3221224432 3221223120 134554751 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 12640 11853 145 145 0 12495 0 [pid=31054] vsize: 50560 Current children cumulated CPU time (s) 369.03 Current children cumulated vsize (Kb) 52684 [startup+380.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12219 0 0 0 37821 80 0 0 25 0 1 0 1846669929 52604928 12055 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 12843 12055 145 145 0 12698 0 [pid=31054] vsize: 51372 Current children cumulated CPU time (s) 379.02 Current children cumulated vsize (Kb) 53496 [startup+390.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12468 0 0 0 38817 81 0 0 25 0 1 0 1846669929 53604352 12304 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13087 12304 145 145 0 12942 0 [pid=31054] vsize: 52348 Current children cumulated CPU time (s) 388.99 Current children cumulated vsize (Kb) 54472 [startup+400.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12708 0 0 0 39813 83 0 0 25 0 1 0 1846669929 54571008 12544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13323 12544 145 145 0 13178 0 [pid=31054] vsize: 53292 Current children cumulated CPU time (s) 398.97 Current children cumulated vsize (Kb) 55416 [startup+410.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12806 0 0 0 40811 84 0 0 25 0 1 0 1846669929 54956032 12642 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12642 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 408.96 Current children cumulated vsize (Kb) 55792 [startup+420.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12806 0 0 0 41811 84 0 0 25 0 1 0 1846669929 54956032 12642 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12642 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 418.96 Current children cumulated vsize (Kb) 55792 [startup+430.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12806 0 0 0 42811 85 0 0 25 0 1 0 1846669929 54956032 12642 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12642 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 428.97 Current children cumulated vsize (Kb) 55792 [startup+440.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12806 0 0 0 43811 85 0 0 25 0 1 0 1846669929 54956032 12642 4294967295 134512640 135094434 3221224432 3221223024 134557336 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12642 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 438.97 Current children cumulated vsize (Kb) 55792 [startup+450.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12807 0 0 0 44812 85 0 0 25 0 1 0 1846669929 54956032 12643 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12643 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 448.98 Current children cumulated vsize (Kb) 55792 [startup+460.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 45812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 458.98 Current children cumulated vsize (Kb) 55792 [startup+470.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 46812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 468.98 Current children cumulated vsize (Kb) 55792 [startup+480.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 47812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 478.98 Current children cumulated vsize (Kb) 55792 [startup+490.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 48812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223056 134557665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 488.98 Current children cumulated vsize (Kb) 55792 [startup+500.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 49812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 498.98 Current children cumulated vsize (Kb) 55792 [startup+510.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 50812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 508.98 Current children cumulated vsize (Kb) 55792 [startup+520.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 51812 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 518.98 Current children cumulated vsize (Kb) 55792 [startup+530.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12808 0 0 0 52813 85 0 0 25 0 1 0 1846669929 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12644 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 528.99 Current children cumulated vsize (Kb) 55792 [startup+540.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 53813 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 538.99 Current children cumulated vsize (Kb) 55792 [startup+550.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 54813 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 548.99 Current children cumulated vsize (Kb) 55792 [startup+560.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 55813 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223056 134557655 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 558.99 Current children cumulated vsize (Kb) 55792 [startup+570.043 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 56813 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 568.99 Current children cumulated vsize (Kb) 55792 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12810 0 0 0 57814 85 0 0 25 0 1 0 1846669929 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12646 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 579 Current children cumulated vsize (Kb) 55792 [startup+590.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 58814 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 589 Current children cumulated vsize (Kb) 55792 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 59814 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 599 Current children cumulated vsize (Kb) 55792 [startup+610.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 60814 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 609 Current children cumulated vsize (Kb) 55792 [startup+620.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 61815 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 619.01 Current children cumulated vsize (Kb) 55792 [startup+630.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12811 0 0 0 62815 85 0 0 25 0 1 0 1846669929 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12647 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 629.01 Current children cumulated vsize (Kb) 55792 [startup+640.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12812 0 0 0 63815 85 0 0 25 0 1 0 1846669929 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12648 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 639.01 Current children cumulated vsize (Kb) 55792 [startup+650.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12812 0 0 0 64815 85 0 0 25 0 1 0 1846669929 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12648 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 649.01 Current children cumulated vsize (Kb) 55792 [startup+660.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12812 0 0 0 65816 85 0 0 25 0 1 0 1846669929 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12648 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 659.02 Current children cumulated vsize (Kb) 55792 [startup+670.05 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12812 0 0 0 66816 85 0 0 25 0 1 0 1846669929 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12648 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 669.02 Current children cumulated vsize (Kb) 55792 [startup+680.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12814 0 0 0 67816 86 0 0 25 0 1 0 1846669929 54956032 12650 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12650 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 679.03 Current children cumulated vsize (Kb) 55792 [startup+690.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12814 0 0 0 68816 86 0 0 25 0 1 0 1846669929 54956032 12650 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12650 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 689.03 Current children cumulated vsize (Kb) 55792 [startup+700.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12815 0 0 0 69816 86 0 0 25 0 1 0 1846669929 54956032 12651 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13417 12651 145 145 0 13272 0 [pid=31054] vsize: 53668 Current children cumulated CPU time (s) 699.03 Current children cumulated vsize (Kb) 55792 [startup+710.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 12848 0 0 0 70816 86 0 0 25 0 1 0 1846669929 55083008 12684 4294967295 134512640 135094434 3221224432 3221223072 134562139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13448 12684 145 145 0 13303 0 [pid=31054] vsize: 53792 Current children cumulated CPU time (s) 709.03 Current children cumulated vsize (Kb) 55916 [startup+720.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13011 0 0 0 71812 87 0 0 25 0 1 0 1846669929 55767040 12847 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13615 12847 145 145 0 13470 0 [pid=31054] vsize: 54460 Current children cumulated CPU time (s) 719 Current children cumulated vsize (Kb) 56584 [startup+730.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13123 0 0 0 72810 88 0 0 25 0 1 0 1846669929 56221696 12959 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13726 12959 145 145 0 13581 0 [pid=31054] vsize: 54904 Current children cumulated CPU time (s) 728.99 Current children cumulated vsize (Kb) 57028 [startup+740.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13284 0 0 0 73807 90 0 0 25 0 1 0 1846669929 56930304 13120 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 13899 13120 145 145 0 13754 0 [pid=31054] vsize: 55596 Current children cumulated CPU time (s) 738.98 Current children cumulated vsize (Kb) 57720 [startup+750.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13410 0 0 0 74806 91 0 0 25 0 1 0 1846669929 57487360 13246 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 14035 13246 145 145 0 13890 0 [pid=31054] vsize: 56140 Current children cumulated CPU time (s) 748.98 Current children cumulated vsize (Kb) 58264 [startup+760.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13528 0 0 0 75803 92 0 0 25 0 1 0 1846669929 57970688 13364 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 14153 13364 145 145 0 14008 0 [pid=31054] vsize: 56612 Current children cumulated CPU time (s) 758.96 Current children cumulated vsize (Kb) 58736 [startup+770.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 13710 0 0 0 76801 93 0 0 25 0 1 0 1846669929 58740736 13546 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 14341 13546 145 145 0 14196 0 [pid=31054] vsize: 57364 Current children cumulated CPU time (s) 768.95 Current children cumulated vsize (Kb) 59488 [startup+780.057 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) T 31050 31050 19316 0 -1 0 13842 0 0 0 77799 94 0 0 25 0 1 0 1846669929 59273216 13678 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/31054/statm): 14471 13678 145 145 0 14326 0 [pid=31054] vsize: 57884 Current children cumulated CPU time (s) 778.94 Current children cumulated vsize (Kb) 60008 [startup+790.057 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14043 0 0 0 78795 95 0 0 25 0 1 0 1846669929 60100608 13879 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 14673 13879 145 145 0 14528 0 [pid=31054] vsize: 58692 Current children cumulated CPU time (s) 788.91 Current children cumulated vsize (Kb) 60816 [startup+800.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14269 0 0 0 79792 97 0 0 25 0 1 0 1846669929 61042688 14105 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 14903 14105 145 145 0 14758 0 [pid=31054] vsize: 59612 Current children cumulated CPU time (s) 798.9 Current children cumulated vsize (Kb) 61736 [startup+810.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14367 0 0 0 80791 98 0 0 25 0 1 0 1846669929 61452288 14203 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 15003 14203 145 145 0 14858 0 [pid=31054] vsize: 60012 Current children cumulated CPU time (s) 808.9 Current children cumulated vsize (Kb) 62136 [startup+820.059 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14474 0 0 0 81789 98 0 0 25 0 1 0 1846669929 61878272 14310 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 15107 14310 145 145 0 14962 0 [pid=31054] vsize: 60428 Current children cumulated CPU time (s) 818.88 Current children cumulated vsize (Kb) 62552 [startup+830.06 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14564 0 0 0 82788 99 0 0 25 0 1 0 1846669929 62230528 14400 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 15193 14400 145 145 0 15048 0 [pid=31054] vsize: 60772 Current children cumulated CPU time (s) 828.88 Current children cumulated vsize (Kb) 62896 [startup+840.06 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14655 0 0 0 83786 100 0 0 25 0 1 0 1846669929 62607360 14491 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 15285 14491 145 145 0 15140 0 [pid=31054] vsize: 61140 Current children cumulated CPU time (s) 838.87 Current children cumulated vsize (Kb) 63264 [startup+850.061 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14754 0 0 0 84785 100 0 0 25 0 1 0 1846669929 63004672 14590 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 15382 14590 145 145 0 15237 0 [pid=31054] vsize: 61528 Current children cumulated CPU time (s) 848.86 Current children cumulated vsize (Kb) 63652 [startup+860.061 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 14861 0 0 0 85784 101 0 0 25 0 1 0 1846669929 64520192 14697 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 15752 14697 145 145 0 15607 0 [pid=31054] vsize: 63008 Current children cumulated CPU time (s) 858.86 Current children cumulated vsize (Kb) 65132 [startup+870.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15266 0 0 0 86777 103 0 0 25 0 1 0 1846669929 66162688 15102 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16153 15102 145 145 0 16008 0 [pid=31054] vsize: 64612 Current children cumulated CPU time (s) 868.81 Current children cumulated vsize (Kb) 66736 [startup+880.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15354 0 0 0 87775 104 0 0 25 0 1 0 1846669929 66519040 15190 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16240 15190 145 145 0 16095 0 [pid=31054] vsize: 64960 Current children cumulated CPU time (s) 878.8 Current children cumulated vsize (Kb) 67084 [startup+890.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15354 0 0 0 88775 104 0 0 25 0 1 0 1846669929 66519040 15190 4294967295 134512640 135094434 3221224432 3221223104 134556302 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16240 15190 145 145 0 16095 0 [pid=31054] vsize: 64960 Current children cumulated CPU time (s) 888.8 Current children cumulated vsize (Kb) 67084 [startup+900.064 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15354 0 0 0 89775 104 0 0 25 0 1 0 1846669929 66519040 15190 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16240 15190 145 145 0 16095 0 [pid=31054] vsize: 64960 Current children cumulated CPU time (s) 898.8 Current children cumulated vsize (Kb) 67084 [startup+910.064 s] Raw data (loadavg): 0.99 0.97 0.98 3/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 90775 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0 [pid=31054] vsize: 64960 Current children cumulated CPU time (s) 908.8 Current children cumulated vsize (Kb) 67084 [startup+920.065 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 91776 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0 [pid=31054] vsize: 64960 Current children cumulated CPU time (s) 918.81 Current children cumulated vsize (Kb) 67084 [startup+930.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 92776 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0 [pid=31054] vsize: 64960 Current children cumulated CPU time (s) 928.81 Current children cumulated vsize (Kb) 67084 [startup+940.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 93776 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0 [pid=31054] vsize: 64960 Current children cumulated CPU time (s) 938.81 Current children cumulated vsize (Kb) 67084 [startup+950.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 94776 104 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0 [pid=31054] vsize: 64960 Current children cumulated CPU time (s) 948.81 Current children cumulated vsize (Kb) 67084 [startup+960.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15355 0 0 0 95776 105 0 0 25 0 1 0 1846669929 66519040 15191 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16240 15191 145 145 0 16095 0 [pid=31054] vsize: 64960 Current children cumulated CPU time (s) 958.82 Current children cumulated vsize (Kb) 67084 [startup+970.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15365 0 0 0 96777 105 0 0 25 0 1 0 1846669929 66584576 15201 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16256 15201 145 145 0 16111 0 [pid=31054] vsize: 65024 Current children cumulated CPU time (s) 968.83 Current children cumulated vsize (Kb) 67148 [startup+980.069 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15370 0 0 0 97777 105 0 0 25 0 1 0 1846669929 66613248 15206 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16263 15206 145 145 0 16118 0 [pid=31054] vsize: 65052 Current children cumulated CPU time (s) 978.83 Current children cumulated vsize (Kb) 67176 [startup+990.069 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15377 0 0 0 98777 105 0 0 25 0 1 0 1846669929 66646016 15213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15213 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 988.83 Current children cumulated vsize (Kb) 67208 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15377 0 0 0 99777 105 0 0 25 0 1 0 1846669929 66646016 15213 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15213 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 998.83 Current children cumulated vsize (Kb) 67208 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 100778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1008.84 Current children cumulated vsize (Kb) 67208 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 101778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1018.84 Current children cumulated vsize (Kb) 67208 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 102778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1028.84 Current children cumulated vsize (Kb) 67208 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 103778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1038.84 Current children cumulated vsize (Kb) 67208 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 104778 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1048.84 Current children cumulated vsize (Kb) 67208 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 105779 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1058.85 Current children cumulated vsize (Kb) 67208 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 106779 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1068.85 Current children cumulated vsize (Kb) 67208 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 107779 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1078.85 Current children cumulated vsize (Kb) 67208 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15379 0 0 0 108779 105 0 0 25 0 1 0 1846669929 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15215 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1088.85 Current children cumulated vsize (Kb) 67208 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 109780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1098.86 Current children cumulated vsize (Kb) 67208 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 110780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1108.86 Current children cumulated vsize (Kb) 67208 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 111780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223120 134554667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1118.86 Current children cumulated vsize (Kb) 67208 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 112780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1128.86 Current children cumulated vsize (Kb) 67208 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 113780 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1138.86 Current children cumulated vsize (Kb) 67208 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15381 0 0 0 114781 105 0 0 25 0 1 0 1846669929 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16271 15217 145 145 0 16126 0 [pid=31054] vsize: 65084 Current children cumulated CPU time (s) 1148.87 Current children cumulated vsize (Kb) 67208 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 115781 105 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0 [pid=31054] vsize: 65148 Current children cumulated CPU time (s) 1158.87 Current children cumulated vsize (Kb) 67272 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 116781 105 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0 [pid=31054] vsize: 65148 Current children cumulated CPU time (s) 1168.87 Current children cumulated vsize (Kb) 67272 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 117781 105 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0 [pid=31054] vsize: 65148 Current children cumulated CPU time (s) 1178.87 Current children cumulated vsize (Kb) 67272 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 118781 106 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0 [pid=31054] vsize: 65148 Current children cumulated CPU time (s) 1188.88 Current children cumulated vsize (Kb) 67272 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15392 0 0 0 119781 106 0 0 25 0 1 0 1846669929 66711552 15228 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16287 15228 145 145 0 16142 0 [pid=31054] vsize: 65148 Current children cumulated CPU time (s) 1198.88 Current children cumulated vsize (Kb) 67272 [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15404 0 0 0 120781 106 0 0 25 0 1 0 1846669929 66777088 15240 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16303 15240 145 145 0 16158 0 [pid=31054] vsize: 65212 Current children cumulated CPU time (s) 1208.88 Current children cumulated vsize (Kb) 67336 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 31054 Raw data (/proc/31050/stat): 31050 (minisat+_script) S 31049 31050 19316 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846669924 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/31050/statm): 531 226 485 147 0 384 0 [pid=31050] vsize: 2124 Raw data (/proc/31054/stat): 31054 (minisat+_64-bit) R 31050 31050 19316 0 -1 0 15404 0 0 0 120781 106 0 0 25 0 1 0 1846669929 66777088 15240 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/31054/statm): 16303 15240 145 145 0 16158 0 [pid=31054] vsize: 65212 Current children cumulated CPU time (s) 1208.88 Current children cumulated vsize (Kb) 67336 Sending SIGTERM to -31050 Sleeping 2 seconds One traced child (pid=31050) ended because it received signal 15 (SIGTERM) One traced child (pid=31054) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.12 CPU time (s): 1208.91 CPU user time (s): 1207.82 CPU system time (s): 1.09583 CPU usage (%): 99.9003 Max. virtual memory (cumulated for all children) (Kb): 67336
ERROR: no interpretation found !