Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-vpm1.opb |
MD5SUM | eb50800dc2fc522dd2f29a347fbab1da |
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 | 1250.11 |
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 wulflinc27 THE 2005-09-19 18:16:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3013 boxname=wulflinc27 idbench=669 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: eb50800dc2fc522dd2f29a347fbab1da /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-vpm1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-vpm1.opb IDLAUNCH: 3013 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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.169 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: 875272 kB Buffers: 33856 kB Cached: 93028 kB SwapCached: 752 kB Active: 69352 kB Inactive: 60136 kB HighTotal: 131008 kB HighFree: 42532 kB LowTotal: 903652 kB LowFree: 832740 kB SwapTotal: 2097892 kB SwapFree: 2096628 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5728 kB Slab: 24360 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 18:36:45 (client local time) WITH STATUS 0 IN 1208.93 SECONDS stats: 3013 7 1208.93 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/18391/stat): 18391 (minisat+_script) R 18390 18391 28974 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1851970754 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/18391/statm): 174 3 169 147 0 27 0 [pid=18391] 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=18392 New process pid=18393 New process pid=18394 execve syscall for /bin/sed executable One traced child (pid=18393) 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=18394) exited with status: 0 One traced child (pid=18392) exited with status: 0 New process pid=18395 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-vpm1.opb [startup+10.0033 s] Raw data (loadavg): 0.93 0.95 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 3829 0 0 0 965 15 0 0 25 0 1 0 1851970759 17580032 3665 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 4292 3665 145 145 0 4147 0 [pid=18395] vsize: 17168 Current children cumulated CPU time (s) 9.82 Current children cumulated vsize (Kb) 19292 [startup+20.0051 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 4192 0 0 0 1958 19 0 0 25 0 1 0 1851970759 19103744 4028 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 4664 4028 145 145 0 4519 0 [pid=18395] vsize: 18656 Current children cumulated CPU time (s) 19.79 Current children cumulated vsize (Kb) 20780 [startup+30.007 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 4662 0 0 0 2950 22 0 0 25 0 1 0 1851970759 21094400 4498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 5150 4498 145 145 0 5005 0 [pid=18395] vsize: 20600 Current children cumulated CPU time (s) 29.74 Current children cumulated vsize (Kb) 22724 [startup+40.0078 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 5187 0 0 0 3940 27 0 0 25 0 1 0 1851970759 23183360 5023 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 5660 5023 145 145 0 5515 0 [pid=18395] vsize: 22640 Current children cumulated CPU time (s) 39.69 Current children cumulated vsize (Kb) 24764 [startup+50.0096 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 5602 0 0 0 4931 31 0 0 25 0 1 0 1851970759 24838144 5438 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 6064 5438 145 145 0 5919 0 [pid=18395] vsize: 24256 Current children cumulated CPU time (s) 49.64 Current children cumulated vsize (Kb) 26380 [startup+60.0105 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 6077 0 0 0 5923 35 0 0 25 0 1 0 1851970759 27000832 5913 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 6592 5913 145 145 0 6447 0 [pid=18395] vsize: 26368 Current children cumulated CPU time (s) 59.6 Current children cumulated vsize (Kb) 28492 [startup+70.0123 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 6375 0 0 0 6917 38 0 0 25 0 1 0 1851970759 28205056 6211 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 6886 6211 145 145 0 6741 0 [pid=18395] vsize: 27544 Current children cumulated CPU time (s) 69.57 Current children cumulated vsize (Kb) 29668 [startup+80.0141 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 6697 0 0 0 7912 41 0 0 25 0 1 0 1851970759 29523968 6533 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 7208 6533 145 145 0 7063 0 [pid=18395] vsize: 28832 Current children cumulated CPU time (s) 79.55 Current children cumulated vsize (Kb) 30956 [startup+90.0149 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7021 0 0 0 8906 43 0 0 25 0 1 0 1851970759 30834688 6857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 7528 6857 145 145 0 7383 0 [pid=18395] vsize: 30112 Current children cumulated CPU time (s) 89.51 Current children cumulated vsize (Kb) 32236 [startup+100.016 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7309 0 0 0 9901 45 0 0 25 0 1 0 1851970759 31993856 7145 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 7811 7145 145 145 0 7666 0 [pid=18395] vsize: 31244 Current children cumulated CPU time (s) 99.48 Current children cumulated vsize (Kb) 33368 [startup+110.017 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7551 0 0 0 10897 47 0 0 25 0 1 0 1851970759 32956416 7387 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 8046 7387 145 145 0 7901 0 [pid=18395] vsize: 32184 Current children cumulated CPU time (s) 109.46 Current children cumulated vsize (Kb) 34308 [startup+120.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7783 0 0 0 11894 48 0 0 25 0 1 0 1851970759 33918976 7619 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 8281 7619 145 145 0 8136 0 [pid=18395] vsize: 33124 Current children cumulated CPU time (s) 119.44 Current children cumulated vsize (Kb) 35248 [startup+130.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 7965 0 0 0 12891 49 0 0 25 0 1 0 1851970759 34664448 7801 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 8463 7801 145 145 0 8318 0 [pid=18395] vsize: 33852 Current children cumulated CPU time (s) 129.42 Current children cumulated vsize (Kb) 35976 [startup+140.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 8140 0 0 0 13889 50 0 0 25 0 1 0 1851970759 35368960 7976 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 8635 7976 145 145 0 8490 0 [pid=18395] vsize: 34540 Current children cumulated CPU time (s) 139.41 Current children cumulated vsize (Kb) 36664 [startup+150.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 8304 0 0 0 14887 51 0 0 25 0 1 0 1851970759 36016128 8140 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 8793 8140 145 145 0 8648 0 [pid=18395] vsize: 35172 Current children cumulated CPU time (s) 149.4 Current children cumulated vsize (Kb) 37296 [startup+160.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 8549 0 0 0 15883 52 0 0 25 0 1 0 1851970759 37564416 8385 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 9171 8385 145 145 0 9026 0 [pid=18395] vsize: 36684 Current children cumulated CPU time (s) 159.37 Current children cumulated vsize (Kb) 38808 [startup+170.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 8846 0 0 0 16878 55 0 0 25 0 1 0 1851970759 38756352 8682 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 9462 8682 145 145 0 9317 0 [pid=18395] vsize: 37848 Current children cumulated CPU time (s) 169.35 Current children cumulated vsize (Kb) 39972 [startup+180.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9189 0 0 0 17871 57 0 0 25 0 1 0 1851970759 40148992 9025 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 9802 9025 145 145 0 9657 0 [pid=18395] vsize: 39208 Current children cumulated CPU time (s) 179.3 Current children cumulated vsize (Kb) 41332 [startup+190.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9409 0 0 0 18868 58 0 0 25 0 1 0 1851970759 41017344 9245 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 10014 9245 145 145 0 9869 0 [pid=18395] vsize: 40056 Current children cumulated CPU time (s) 189.28 Current children cumulated vsize (Kb) 42180 [startup+200.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9563 0 0 0 19866 59 0 0 25 0 1 0 1851970759 41635840 9399 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 10165 9399 145 145 0 10020 0 [pid=18395] vsize: 40660 Current children cumulated CPU time (s) 199.27 Current children cumulated vsize (Kb) 42784 [startup+210.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9722 0 0 0 20864 60 0 0 25 0 1 0 1851970759 42266624 9558 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 10319 9558 145 145 0 10174 0 [pid=18395] vsize: 41276 Current children cumulated CPU time (s) 209.26 Current children cumulated vsize (Kb) 43400 [startup+220.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 9875 0 0 0 21862 60 0 0 25 0 1 0 1851970759 42889216 9711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 10471 9711 145 145 0 10326 0 [pid=18395] vsize: 41884 Current children cumulated CPU time (s) 219.24 Current children cumulated vsize (Kb) 44008 [startup+230.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10031 0 0 0 22860 61 0 0 25 0 1 0 1851970759 43532288 9867 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 10628 9867 145 145 0 10483 0 [pid=18395] vsize: 42512 Current children cumulated CPU time (s) 229.23 Current children cumulated vsize (Kb) 44636 [startup+240.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10166 0 0 0 23859 62 0 0 25 0 1 0 1851970759 44068864 10002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 10759 10002 145 145 0 10614 0 [pid=18395] vsize: 43036 Current children cumulated CPU time (s) 239.23 Current children cumulated vsize (Kb) 45160 [startup+250.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10300 0 0 0 24857 63 0 0 25 0 1 0 1851970759 44634112 10136 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 10897 10136 145 145 0 10752 0 [pid=18395] vsize: 43588 Current children cumulated CPU time (s) 249.22 Current children cumulated vsize (Kb) 45712 [startup+260.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10412 0 0 0 25854 64 0 0 25 0 1 0 1851970759 45092864 10248 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 11009 10248 145 145 0 10864 0 [pid=18395] vsize: 44036 Current children cumulated CPU time (s) 259.2 Current children cumulated vsize (Kb) 46160 [startup+270.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10527 0 0 0 26852 65 0 0 25 0 1 0 1851970759 45551616 10363 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 11121 10363 145 145 0 10976 0 [pid=18395] vsize: 44484 Current children cumulated CPU time (s) 269.19 Current children cumulated vsize (Kb) 46608 [startup+280.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10650 0 0 0 27850 67 0 0 25 0 1 0 1851970759 46067712 10486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 11247 10486 145 145 0 11102 0 [pid=18395] vsize: 44988 Current children cumulated CPU time (s) 279.19 Current children cumulated vsize (Kb) 47112 [startup+290.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10768 0 0 0 28848 67 0 0 25 0 1 0 1851970759 46563328 10604 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 11368 10604 145 145 0 11223 0 [pid=18395] vsize: 45472 Current children cumulated CPU time (s) 289.17 Current children cumulated vsize (Kb) 47596 [startup+300.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 10893 0 0 0 29847 68 0 0 25 0 1 0 1851970759 47054848 10729 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 11488 10729 145 145 0 11343 0 [pid=18395] vsize: 45952 Current children cumulated CPU time (s) 299.17 Current children cumulated vsize (Kb) 48076 [startup+310.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11007 0 0 0 30845 69 0 0 25 0 1 0 1851970759 47554560 10843 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 11610 10843 145 145 0 11465 0 [pid=18395] vsize: 46440 Current children cumulated CPU time (s) 309.16 Current children cumulated vsize (Kb) 48564 [startup+320.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11104 0 0 0 31844 69 0 0 25 0 1 0 1851970759 47927296 10940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 11701 10940 145 145 0 11556 0 [pid=18395] vsize: 46804 Current children cumulated CPU time (s) 319.15 Current children cumulated vsize (Kb) 48928 [startup+330.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11202 0 0 0 32842 70 0 0 25 0 1 0 1851970759 48312320 11038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 11795 11038 145 145 0 11650 0 [pid=18395] vsize: 47180 Current children cumulated CPU time (s) 329.14 Current children cumulated vsize (Kb) 49304 [startup+340.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11436 0 0 0 33838 71 0 0 25 0 1 0 1851970759 49295360 11272 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 12035 11272 145 145 0 11890 0 [pid=18395] vsize: 48140 Current children cumulated CPU time (s) 339.11 Current children cumulated vsize (Kb) 50264 [startup+350.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11671 0 0 0 34835 73 0 0 25 0 1 0 1851970759 50323456 11507 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 12286 11507 145 145 0 12141 0 [pid=18395] vsize: 49144 Current children cumulated CPU time (s) 349.1 Current children cumulated vsize (Kb) 51268 [startup+360.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 11885 0 0 0 35830 74 0 0 25 0 1 0 1851970759 51216384 11721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 12504 11721 145 145 0 12359 0 [pid=18395] vsize: 50016 Current children cumulated CPU time (s) 359.06 Current children cumulated vsize (Kb) 52140 [startup+370.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12085 0 0 0 36826 76 0 0 25 0 1 0 1851970759 52035584 11921 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 12704 11921 145 145 0 12559 0 [pid=18395] vsize: 50816 Current children cumulated CPU time (s) 369.04 Current children cumulated vsize (Kb) 52940 [startup+380.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12280 0 0 0 37821 78 0 0 25 0 1 0 1851970759 52854784 12116 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 12904 12116 145 145 0 12759 0 [pid=18395] vsize: 51616 Current children cumulated CPU time (s) 379.01 Current children cumulated vsize (Kb) 53740 [startup+390.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12567 0 0 0 38816 81 0 0 25 0 1 0 1851970759 54001664 12403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 13184 12403 145 145 0 13039 0 [pid=18395] vsize: 52736 Current children cumulated CPU time (s) 388.99 Current children cumulated vsize (Kb) 54860 [startup+400.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12772 0 0 0 39813 82 0 0 25 0 1 0 1851970759 54816768 12608 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 13383 12608 145 145 0 13238 0 [pid=18395] vsize: 53532 Current children cumulated CPU time (s) 398.97 Current children cumulated vsize (Kb) 55656 [startup+410.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12806 0 0 0 40813 83 0 0 25 0 1 0 1851970759 54956032 12642 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12642 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 408.98 Current children cumulated vsize (Kb) 55792 [startup+420.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12806 0 0 0 41813 83 0 0 25 0 1 0 1851970759 54956032 12642 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12642 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 418.98 Current children cumulated vsize (Kb) 55792 [startup+430.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12806 0 0 0 42813 83 0 0 25 0 1 0 1851970759 54956032 12642 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12642 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 428.98 Current children cumulated vsize (Kb) 55792 [startup+440.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12807 0 0 0 43814 83 0 0 25 0 1 0 1851970759 54956032 12643 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12643 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 438.99 Current children cumulated vsize (Kb) 55792 [startup+450.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12807 0 0 0 44814 83 0 0 25 0 1 0 1851970759 54956032 12643 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12643 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 448.99 Current children cumulated vsize (Kb) 55792 [startup+460.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 45814 83 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 458.99 Current children cumulated vsize (Kb) 55792 [startup+470.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 46814 83 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 468.99 Current children cumulated vsize (Kb) 55792 [startup+480.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 47814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 479 Current children cumulated vsize (Kb) 55792 [startup+490.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 48813 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 488.99 Current children cumulated vsize (Kb) 55792 [startup+500.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 49814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 499 Current children cumulated vsize (Kb) 55792 [startup+510.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 50814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 509 Current children cumulated vsize (Kb) 55792 [startup+520.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 51814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 519 Current children cumulated vsize (Kb) 55792 [startup+530.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12808 0 0 0 52814 84 0 0 25 0 1 0 1851970759 54956032 12644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12644 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 529 Current children cumulated vsize (Kb) 55792 [startup+540.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 53815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 539.01 Current children cumulated vsize (Kb) 55792 [startup+550.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 54815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 549.01 Current children cumulated vsize (Kb) 55792 [startup+560.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 55815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 559.01 Current children cumulated vsize (Kb) 55792 [startup+570.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 56815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 569.01 Current children cumulated vsize (Kb) 55792 [startup+580.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12810 0 0 0 57815 84 0 0 25 0 1 0 1851970759 54956032 12646 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12646 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 579.01 Current children cumulated vsize (Kb) 55792 [startup+590.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12811 0 0 0 58816 84 0 0 25 0 1 0 1851970759 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12647 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 589.02 Current children cumulated vsize (Kb) 55792 [startup+600.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12811 0 0 0 59816 85 0 0 25 0 1 0 1851970759 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12647 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 599.03 Current children cumulated vsize (Kb) 55792 [startup+610.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12811 0 0 0 60816 85 0 0 25 0 1 0 1851970759 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12647 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 609.03 Current children cumulated vsize (Kb) 55792 [startup+620.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12811 0 0 0 61816 85 0 0 25 0 1 0 1851970759 54956032 12647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12647 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 619.03 Current children cumulated vsize (Kb) 55792 [startup+630.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12812 0 0 0 62816 85 0 0 25 0 1 0 1851970759 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12648 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 629.03 Current children cumulated vsize (Kb) 55792 [startup+640.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12812 0 0 0 63817 85 0 0 25 0 1 0 1851970759 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12648 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 639.04 Current children cumulated vsize (Kb) 55792 [startup+650.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12812 0 0 0 64817 85 0 0 25 0 1 0 1851970759 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12648 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 649.04 Current children cumulated vsize (Kb) 55792 [startup+660.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12812 0 0 0 65817 85 0 0 25 0 1 0 1851970759 54956032 12648 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12648 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 659.04 Current children cumulated vsize (Kb) 55792 [startup+670.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12814 0 0 0 66817 85 0 0 25 0 1 0 1851970759 54956032 12650 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12650 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 669.04 Current children cumulated vsize (Kb) 55792 [startup+680.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12814 0 0 0 67817 85 0 0 25 0 1 0 1851970759 54956032 12650 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12650 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 679.04 Current children cumulated vsize (Kb) 55792 [startup+690.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12815 0 0 0 68818 85 0 0 25 0 1 0 1851970759 54956032 12651 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13417 12651 145 145 0 13272 0 [pid=18395] vsize: 53668 Current children cumulated CPU time (s) 689.05 Current children cumulated vsize (Kb) 55792 [startup+700.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 12840 0 0 0 69818 85 0 0 25 0 1 0 1851970759 55050240 12676 4294967295 134512640 135094434 3221224432 3221223088 134555980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13440 12676 145 145 0 13295 0 [pid=18395] vsize: 53760 Current children cumulated CPU time (s) 699.05 Current children cumulated vsize (Kb) 55884 [startup+710.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13002 0 0 0 70815 87 0 0 25 0 1 0 1851970759 55726080 12838 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13605 12838 145 145 0 13460 0 [pid=18395] vsize: 54420 Current children cumulated CPU time (s) 709.04 Current children cumulated vsize (Kb) 56544 [startup+720.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13116 0 0 0 71813 88 0 0 25 0 1 0 1851970759 56193024 12952 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13719 12952 145 145 0 13574 0 [pid=18395] vsize: 54876 Current children cumulated CPU time (s) 719.03 Current children cumulated vsize (Kb) 57000 [startup+730.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13280 0 0 0 72810 89 0 0 25 0 1 0 1851970759 56918016 13116 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 13896 13116 145 145 0 13751 0 [pid=18395] vsize: 55584 Current children cumulated CPU time (s) 729.01 Current children cumulated vsize (Kb) 57708 [startup+740.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13410 0 0 0 73808 90 0 0 25 0 1 0 1851970759 57487360 13246 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 14035 13246 145 145 0 13890 0 [pid=18395] vsize: 56140 Current children cumulated CPU time (s) 739 Current children cumulated vsize (Kb) 58264 [startup+750.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13532 0 0 0 74807 90 0 0 25 0 1 0 1851970759 57987072 13368 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 14157 13368 145 145 0 14012 0 [pid=18395] vsize: 56628 Current children cumulated CPU time (s) 748.99 Current children cumulated vsize (Kb) 58752 [startup+760.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13717 0 0 0 75804 92 0 0 25 0 1 0 1851970759 58765312 13553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 14347 13553 145 145 0 14202 0 [pid=18395] vsize: 57388 Current children cumulated CPU time (s) 758.98 Current children cumulated vsize (Kb) 59512 [startup+770.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 13850 0 0 0 76802 92 0 0 25 0 1 0 1851970759 59305984 13686 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 14479 13686 145 145 0 14334 0 [pid=18395] vsize: 57916 Current children cumulated CPU time (s) 768.96 Current children cumulated vsize (Kb) 60040 [startup+780.088 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) T 18391 18391 28974 0 -1 0 14129 0 0 0 77797 95 0 0 25 0 1 0 1851970759 60444672 13965 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/18395/statm): 14757 13965 145 145 0 14612 0 [pid=18395] vsize: 59028 Current children cumulated CPU time (s) 778.94 Current children cumulated vsize (Kb) 61152 [startup+790.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14283 0 0 0 78795 95 0 0 25 0 1 0 1851970759 61095936 14119 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 14916 14119 145 145 0 14771 0 [pid=18395] vsize: 59664 Current children cumulated CPU time (s) 788.92 Current children cumulated vsize (Kb) 61788 [startup+800.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14376 0 0 0 79794 96 0 0 25 0 1 0 1851970759 61489152 14212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 15012 14212 145 145 0 14867 0 [pid=18395] vsize: 60048 Current children cumulated CPU time (s) 798.92 Current children cumulated vsize (Kb) 62172 [startup+810.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14484 0 0 0 80792 97 0 0 25 0 1 0 1851970759 61919232 14320 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 15117 14320 145 145 0 14972 0 [pid=18395] vsize: 60468 Current children cumulated CPU time (s) 808.91 Current children cumulated vsize (Kb) 62592 [startup+820.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14584 0 0 0 81790 98 0 0 25 0 1 0 1851970759 62308352 14420 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 15212 14420 145 145 0 15067 0 [pid=18395] vsize: 60848 Current children cumulated CPU time (s) 818.9 Current children cumulated vsize (Kb) 62972 [startup+830.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14672 0 0 0 82788 98 0 0 25 0 1 0 1851970759 62676992 14508 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 15302 14508 145 145 0 15157 0 [pid=18395] vsize: 61208 Current children cumulated CPU time (s) 828.88 Current children cumulated vsize (Kb) 63332 [startup+840.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14769 0 0 0 83786 99 0 0 25 0 1 0 1851970759 63066112 14605 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 15397 14605 145 145 0 15252 0 [pid=18395] vsize: 61588 Current children cumulated CPU time (s) 838.87 Current children cumulated vsize (Kb) 63712 [startup+850.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 14901 0 0 0 84785 100 0 0 25 0 1 0 1851970759 64700416 14737 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 15796 14737 145 145 0 15651 0 [pid=18395] vsize: 63184 Current children cumulated CPU time (s) 848.87 Current children cumulated vsize (Kb) 65308 [startup+860.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15304 0 0 0 85778 103 0 0 25 0 1 0 1851970759 66314240 15140 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16190 15140 145 145 0 16045 0 [pid=18395] vsize: 64760 Current children cumulated CPU time (s) 858.83 Current children cumulated vsize (Kb) 66884 [startup+870.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15354 0 0 0 86778 104 0 0 25 0 1 0 1851970759 66519040 15190 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16240 15190 145 145 0 16095 0 [pid=18395] vsize: 64960 Current children cumulated CPU time (s) 868.84 Current children cumulated vsize (Kb) 67084 [startup+880.101 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15354 0 0 0 87778 104 0 0 25 0 1 0 1851970759 66519040 15190 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16240 15190 145 145 0 16095 0 [pid=18395] vsize: 64960 Current children cumulated CPU time (s) 878.84 Current children cumulated vsize (Kb) 67084 [startup+890.101 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15354 0 0 0 88779 104 0 0 25 0 1 0 1851970759 66519040 15190 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16240 15190 145 145 0 16095 0 [pid=18395] vsize: 64960 Current children cumulated CPU time (s) 888.85 Current children cumulated vsize (Kb) 67084 [startup+900.102 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 89779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0 [pid=18395] vsize: 64960 Current children cumulated CPU time (s) 898.85 Current children cumulated vsize (Kb) 67084 [startup+910.103 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 90779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223056 134557633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0 [pid=18395] vsize: 64960 Current children cumulated CPU time (s) 908.85 Current children cumulated vsize (Kb) 67084 [startup+920.104 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 91779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0 [pid=18395] vsize: 64960 Current children cumulated CPU time (s) 918.85 Current children cumulated vsize (Kb) 67084 [startup+930.105 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 92779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0 [pid=18395] vsize: 64960 Current children cumulated CPU time (s) 928.85 Current children cumulated vsize (Kb) 67084 [startup+940.106 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15355 0 0 0 93779 104 0 0 25 0 1 0 1851970759 66519040 15191 4294967295 134512640 135094434 3221224432 3221223024 134551918 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16240 15191 145 145 0 16095 0 [pid=18395] vsize: 64960 Current children cumulated CPU time (s) 938.85 Current children cumulated vsize (Kb) 67084 [startup+950.106 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15365 0 0 0 94779 104 0 0 25 0 1 0 1851970759 66584576 15201 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16256 15201 145 145 0 16111 0 [pid=18395] vsize: 65024 Current children cumulated CPU time (s) 948.85 Current children cumulated vsize (Kb) 67148 [startup+960.107 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15365 0 0 0 95779 104 0 0 25 0 1 0 1851970759 66584576 15201 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16256 15201 145 145 0 16111 0 [pid=18395] vsize: 65024 Current children cumulated CPU time (s) 958.85 Current children cumulated vsize (Kb) 67148 [startup+970.108 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15377 0 0 0 96778 105 0 0 25 0 1 0 1851970759 66646016 15213 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15213 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 968.85 Current children cumulated vsize (Kb) 67208 [startup+980.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15377 0 0 0 97778 106 0 0 25 0 1 0 1851970759 66646016 15213 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15213 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 978.86 Current children cumulated vsize (Kb) 67208 [startup+990.112 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 98778 106 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 988.86 Current children cumulated vsize (Kb) 67208 [startup+1000.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 99778 106 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 998.86 Current children cumulated vsize (Kb) 67208 [startup+1010.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 100778 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1008.87 Current children cumulated vsize (Kb) 67208 [startup+1020.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 101779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1018.88 Current children cumulated vsize (Kb) 67208 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 102778 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1028.87 Current children cumulated vsize (Kb) 67208 [startup+1040.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 103779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1038.88 Current children cumulated vsize (Kb) 67208 [startup+1050.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 104779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1048.88 Current children cumulated vsize (Kb) 67208 [startup+1060.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 105779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1058.88 Current children cumulated vsize (Kb) 67208 [startup+1070.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15379 0 0 0 106779 107 0 0 25 0 1 0 1851970759 66646016 15215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15215 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1068.88 Current children cumulated vsize (Kb) 67208 [startup+1080.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 107779 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1078.89 Current children cumulated vsize (Kb) 67208 [startup+1090.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 108779 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1088.89 Current children cumulated vsize (Kb) 67208 [startup+1100.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 109780 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1098.9 Current children cumulated vsize (Kb) 67208 [startup+1110.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 110780 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1108.9 Current children cumulated vsize (Kb) 67208 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 111780 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1118.9 Current children cumulated vsize (Kb) 67208 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15381 0 0 0 112780 108 0 0 25 0 1 0 1851970759 66646016 15217 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16271 15217 145 145 0 16126 0 [pid=18395] vsize: 65084 Current children cumulated CPU time (s) 1128.9 Current children cumulated vsize (Kb) 67208 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 113780 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0 [pid=18395] vsize: 65148 Current children cumulated CPU time (s) 1138.9 Current children cumulated vsize (Kb) 67272 [startup+1150.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 114780 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0 [pid=18395] vsize: 65148 Current children cumulated CPU time (s) 1148.9 Current children cumulated vsize (Kb) 67272 [startup+1160.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 115781 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0 [pid=18395] vsize: 65148 Current children cumulated CPU time (s) 1158.91 Current children cumulated vsize (Kb) 67272 [startup+1170.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 116781 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0 [pid=18395] vsize: 65148 Current children cumulated CPU time (s) 1168.91 Current children cumulated vsize (Kb) 67272 [startup+1180.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15392 0 0 0 117781 108 0 0 25 0 1 0 1851970759 66711552 15228 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16287 15228 145 145 0 16142 0 [pid=18395] vsize: 65148 Current children cumulated CPU time (s) 1178.91 Current children cumulated vsize (Kb) 67272 [startup+1190.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15404 0 0 0 118781 108 0 0 25 0 1 0 1851970759 66777088 15240 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18395/statm): 16303 15240 145 145 0 16158 0 [pid=18395] vsize: 65212 Current children cumulated CPU time (s) 1188.91 Current children cumulated vsize (Kb) 67336 [startup+1200.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15404 0 0 0 119780 109 0 0 25 0 1 0 1851970759 66777088 15240 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16303 15240 145 145 0 16158 0 [pid=18395] vsize: 65212 Current children cumulated CPU time (s) 1198.91 Current children cumulated vsize (Kb) 67336 [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15414 0 0 0 120781 109 0 0 25 0 1 0 1851970759 66842624 15250 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16319 15250 145 145 0 16174 0 [pid=18395] vsize: 65276 Current children cumulated CPU time (s) 1208.92 Current children cumulated vsize (Kb) 67400 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 18395 Raw data (/proc/18391/stat): 18391 (minisat+_script) S 18390 18391 28974 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1851970754 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18391/statm): 531 226 485 147 0 384 0 [pid=18391] vsize: 2124 Raw data (/proc/18395/stat): 18395 (minisat+_64-bit) R 18391 18391 28974 0 -1 0 15414 0 0 0 120781 109 0 0 25 0 1 0 1851970759 66842624 15250 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18395/statm): 16319 15250 145 145 0 16174 0 [pid=18395] vsize: 65276 Current children cumulated CPU time (s) 1208.92 Current children cumulated vsize (Kb) 67400 Sending SIGTERM to -18391 Sleeping 2 seconds One traced child (pid=18391) ended because it received signal 15 (SIGTERM) One traced child (pid=18395) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.17 CPU time (s): 1208.93 CPU user time (s): 1207.81 CPU system time (s): 1.11883 CPU usage (%): 99.898 Max. virtual memory (cumulated for all children) (Kb): 67400
ERROR: no interpretation found !