Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm2.opb |
MD5SUM | fae1fae180d772ad3ee6c1acfa1c8b4f |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 130 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 168 |
Biggest coefficient in the objective function | 5 |
Number of bits for the biggest coefficient in the objective function | 3 |
Sum of the numbers in the objective function | 504 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 2000000 |
Number of bits of the biggest number in a constraint | 21 |
Biggest sum of numbers in a constraint | 30041153 |
Number of bits of the biggest sum of numbers | 25 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.02 |
Number of variables | 2124 |
Total number of constraints | 444 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 444 |
Minimum length of a constraint | 8 |
Maximum length of a constraint | 64 |
LAUNCH ON wulflinc20 THE 2005-09-20 04:41:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3397 boxname=wulflinc20 idbench=1053 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fae1fae180d772ad3ee6c1acfa1c8b4f /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-vpm2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-vpm2.opb IDLAUNCH: 3397 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 914672 kB Buffers: 11964 kB Cached: 79000 kB SwapCached: 904 kB Active: 21068 kB Inactive: 72592 kB HighTotal: 131008 kB HighFree: 47824 kB LowTotal: 903652 kB LowFree: 866848 kB SwapTotal: 2097892 kB SwapFree: 2096536 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 20696 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 05:01:27 (client local time) WITH STATUS 0 IN 1208.65 SECONDS stats: 3397 7 1208.65 0
c Parsing PB file... c Converting 486 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################## c -- Clauses(.)/Splits(s): (none) c ---[ 485]---> BDD-cost: 7 c ---[ 484]---> BDD-cost: 7 c ---[ 483]---> BDD-cost: 7 c ---[ 482]---> BDD-cost: 7 c ---[ 481]---> BDD-cost: 7 c ---[ 480]---> BDD-cost: 7 c ---[ 479]---> BDD-cost: 7 c ---[ 478]---> BDD-cost: 7 c ---[ 477]---> BDD-cost: 7 c ---[ 474]---> BDD-cost: 7 c ---[ 473]---> BDD-cost: 7 c ---[ 472]---> BDD-cost: 7 c ---[ 471]---> BDD-cost: 7 c ---[ 468]---> BDD-cost: 7 c ---[ 467]---> BDD-cost: 7 c ---[ 466]---> BDD-cost: 7 c ---[ 465]---> BDD-cost: 7 c ---[ 462]---> BDD-cost: 7 c ---[ 459]---> BDD-cost: 7 c ---[ 458]---> BDD-cost: 7 c ---[ 457]---> BDD-cost: 7 c ---[ 454]---> BDD-cost: 7 c ---[ 453]---> BDD-cost: 7 c ---[ 452]---> BDD-cost: 7 c ---[ 451]---> BDD-cost: 7 c ---[ 450]---> BDD-cost: 7 c ---[ 448]---> BDD-cost: 7 c ---[ 447]---> BDD-cost: 7 c ---[ 446]---> BDD-cost: 7 c ---[ 445]---> BDD-cost: 7 c ---[ 444]---> BDD-cost: 7 c ---[ 441]---> BDD-cost: 7 c ---[ 440]---> BDD-cost: 7 c ---[ 439]---> BDD-cost: 7 c ---[ 433]---> BDD-cost: 7 c ---[ 427]---> BDD-cost: 7 c ---[ 422]---> BDD-cost: 7 c ---[ 421]---> BDD-cost: 7 c ---[ 415]---> BDD-cost: 7 c ---[ 409]---> BDD-cost: 7 c ---[ 408]---> BDD-cost: 7 c ---[ 402]---> BDD-cost: 7 c ---[ 397]---> BDD-cost: 7 c ---[ 396]---> BDD-cost: 7 c ---[ 391]---> BDD-cost: 7 c ---[ 390]---> BDD-cost: 7 c ---[ 386]---> BDD-cost: 7 c ---[ 385]---> BDD-cost: 7 c ---[ 384]---> BDD-cost: 7 c ---[ 380]---> BDD-cost: 7 c ---[ 379]---> BDD-cost: 7 c ---[ 378]---> BDD-cost: 7 c ---[ 374]---> BDD-cost: 7 c ---[ 373]---> BDD-cost: 7 c ---[ 372]---> BDD-cost: 7 c ---[ 368]---> BDD-cost: 7 c ---[ 367]---> BDD-cost: 7 c ---[ 366]---> BDD-cost: 7 c ---[ 365]---> BDD-cost: 7 c ---[ 364]---> BDD-cost: 7 c ---[ 359]---> BDD-cost: 7 c ---[ 353]---> BDD-cost: 7 c ---[ 347]---> BDD-cost: 7 c ---[ 339]---> BDD-cost: 7 c ---[ 333]---> BDD-cost: 7 c ---[ 327]---> BDD-cost: 7 c ---[ 321]---> BDD-cost: 7 c ---[ 317]---> BDD-cost: 14 c ---[ 316]---> BDD-cost: 14 c ---[ 315]---> BDD-cost: 14 c ---[ 314]---> BDD-cost: 14 c ---[ 313]---> BDD-cost: 14 c ---[ 312]---> BDD-cost: 14 c ---[ 310]---> BDD-cost: 14 c ---[ 309]---> BDD-cost: 14 c ---[ 308]---> BDD-cost: 14 c ---[ 307]---> BDD-cost: 14 c ---[ 306]---> BDD-cost: 14 c ---[ 302]---> BDD-cost: 13 c ---[ 301]---> BDD-cost: 13 c ---[ 300]---> BDD-cost: 13 c ---[ 295]---> BDD-cost: 13 c ---[ 294]---> BDD-cost: 13 c ---[ 290]---> BDD-cost: 15 c ---[ 289]---> BDD-cost: 15 c ---[ 288]---> BDD-cost: 15 c ---[ 287]---> BDD-cost: 13 c ---[ 286]---> BDD-cost: 13 c ---[ 285]---> BDD-cost: 13 c ---[ 284]---> BDD-cost: 13 c ---[ 283]---> BDD-cost: 13 c ---[ 282]---> BDD-cost: 13 c ---[ 280]---> BDD-cost: 13 c ---[ 279]---> BDD-cost: 13 c ---[ 278]---> BDD-cost: 13 c ---[ 277]---> BDD-cost: 13 c ---[ 276]---> BDD-cost: 13 c ---[ 274]---> Sorter-cost: 1988 Base: 2 2 2 5 5 2 2 2 2 2 3 c ---[ 264]---> Sorter-cost: 1824 Base: 2 2 2 5 5 2 2 2 3 2 2 2 c ---[ 260]---> Adder-cost: 262 maxlim: 300367 bits: 19/19 c ---[ 258]---> Adder-cost: 262 maxlim: 300367 bits: 19/19 c ---[ 256]---> Sorter-cost: 2565 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 254]---> Sorter-cost: 2565 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 252]---> Adder-cost: 262 maxlim: 261967 bits: 19/18 c ---[ 250]---> Sorter-cost: 1411 Base: 2 2 2 2 5 5 2 2 2 2 2 c ---[ 248]---> Sorter-cost: 2230 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 246]---> Sorter-cost: 2232 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 244]---> Sorter-cost: 2232 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 242]---> Sorter-cost: 2159 Base: 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[ 236]---> Sorter-cost: 1318 Base: 2 2 2 2 5 5 2 2 2 2 2 c ---[ 234]---> Sorter-cost: 2540 Base: 2 2 2 2 5 5 2 2 2 2 2 2 c ---[ 232]---> Sorter-cost: 1903 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 224]---> Sorter-cost: 1580 Base: 2 2 2 5 5 2 2 2 2 2 3 c ---[ 222]---> Adder-cost: 260 maxlim: 219983 bits: 19/18 c ---[ 216]---> Sorter-cost: 1742 Base: 2 2 2 5 5 2 2 2 2 2 2 c ---[ 214]---> Sorter-cost: 2471 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 212]---> Sorter-cost: 2473 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 c ---[ 210]---> Sorter-cost: 3095 Base: 2 2 2 2 2 3 5 2 2 2 5 c ---[ 208]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 206]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 204]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 202]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 200]---> Sorter-cost: 1882 Base: 2 2 2 2 5 5 2 2 2 5 c ---[ 198]---> Sorter-cost: 3211 Base: 2 2 2 2 5 5 2 2 2 2 5 c ---[ 196]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 194]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 192]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 191]---> BDD-cost: 110 c ---[ 190]---> BDD-cost: 237 c ---[ 189]---> BDD-cost: 236 c ---[ 188]---> BDD-cost: 393 c ---[ 187]---> BDD-cost: 495 c ---[ 186]---> BDD-cost: 488 c ---[ 185]---> BDD-cost: 131 c ---[ 184]---> BDD-cost: 262 c ---[ 183]---> BDD-cost: 261 c ---[ 182]---> BDD-cost: 448 c ---[ 181]---> BDD-cost: 550 c ---[ 180]---> BDD-cost: 549 c ---[ 179]---> Sorter-cost: 335 Base: 2 2 2 2 2 2 5 c ---[ 178]---> Sorter-cost: 867 Base: 2 2 5 2 2 2 2 c ---[ 177]---> Sorter-cost: 830 Base: 2 2 2 2 2 2 5 c ---[ 176]---> Sorter-cost: 1298 Base: 2 2 5 2 2 2 2 c ---[ 175]---> Sorter-cost: 1687 Base: 2 2 5 2 2 2 2 c ---[ 174]---> Sorter-cost: 1665 Base: 2 2 5 2 2 2 2 c ---[ 173]---> Sorter-cost: 196 Base: 2 2 2 2 2 2 c ---[ 172]---> Sorter-cost: 473 Base: 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 421 Base: 2 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 764 Base: 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 884 Base: 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 1063 Base: 2 2 2 2 2 c ---[ 167]---> BDD-cost: 3 c ---[ 166]---> BDD-cost: 3 c ---[ 165]---> BDD-cost: 3 c ---[ 164]---> BDD-cost: 3 c ---[ 163]---> BDD-cost: 3 c ---[ 162]---> BDD-cost: 3 c ---[ 161]---> BDD-cost: 3 c ---[ 160]---> BDD-cost: 3 c ---[ 159]---> BDD-cost: 3 c ---[ 158]---> BDD-cost: 7 c ---[ 157]---> BDD-cost: 7 c ---[ 156]---> BDD-cost: 3 c ---[ 155]---> BDD-cost: 3 c ---[ 154]---> BDD-cost: 3 c ---[ 153]---> BDD-cost: 3 c ---[ 152]---> BDD-cost: 7 c ---[ 151]---> BDD-cost: 7 c ---[ 150]---> BDD-cost: 3 c ---[ 149]---> BDD-cost: 3 c ---[ 148]---> BDD-cost: 3 c ---[ 147]---> BDD-cost: 3 c ---[ 146]---> BDD-cost: 7 c ---[ 145]---> BDD-cost: 7 c ---[ 144]---> BDD-cost: 3 c ---[ 142]---> BDD-cost: 7 c ---[ 141]---> BDD-cost: 3 c ---[ 140]---> BDD-cost: 3 c ---[ 139]---> BDD-cost: 3 c ---[ 138]---> BDD-cost: 7 c ---[ 136]---> BDD-cost: 3 c ---[ 135]---> BDD-cost: 3 c ---[ 134]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 3 c ---[ 132]---> BDD-cost: 3 c ---[ 130]---> BDD-cost: 3 c ---[ 129]---> BDD-cost: 3 c ---[ 128]---> BDD-cost: 3 c ---[ 127]---> BDD-cost: 3 c ---[ 126]---> BDD-cost: 3 c ---[ 124]---> BDD-cost: 7 c ---[ 123]---> BDD-cost: 3 c ---[ 122]---> BDD-cost: 3 c ---[ 121]---> BDD-cost: 3 c ---[ 120]---> BDD-cost: 7 c ---[ 116]---> BDD-cost: 7 c ---[ 115]---> BDD-cost: 3 c ---[ 114]---> BDD-cost: 6 c ---[ 110]---> BDD-cost: 7 c ---[ 109]---> BDD-cost: 3 c ---[ 108]---> BDD-cost: 6 c ---[ 104]---> BDD-cost: 3 c ---[ 103]---> BDD-cost: 3 c ---[ 102]---> BDD-cost: 5 c ---[ 98]---> BDD-cost: 7 c ---[ 97]---> BDD-cost: 3 c ---[ 96]---> BDD-cost: 6 c ---[ 91]---> BDD-cost: 3 c ---[ 90]---> BDD-cost: 3 c ---[ 85]---> BDD-cost: 7 c ---[ 84]---> BDD-cost: 3 c ---[ 79]---> BDD-cost: 3 c ---[ 78]---> BDD-cost: 3 c ---[ 73]---> BDD-cost: 3 c ---[ 72]---> BDD-cost: 3 c ---[ 68]---> BDD-cost: 3 c ---[ 67]---> BDD-cost: 3 c ---[ 66]---> BDD-cost: 3 c ---[ 62]---> BDD-cost: 3 c ---[ 61]---> BDD-cost: 3 c ---[ 60]---> BDD-cost: 3 c ---[ 56]---> BDD-cost: 3 c ---[ 55]---> BDD-cost: 3 c ---[ 54]---> BDD-cost: 3 c ---[ 50]---> BDD-cost: 3 c ---[ 49]---> BDD-cost: 3 c ---[ 48]---> BDD-cost: 3 c ---[ 47]---> BDD-cost: 3 c ---[ 46]---> BDD-cost: 3 c ---[ 45]---> BDD-cost: 6 c ---[ 44]---> BDD-cost: 6 c ---[ 43]---> BDD-cost: 6 c ---[ 42]---> BDD-cost: 6 c ---[ 41]---> BDD-cost: 3 c ---[ 40]---> BDD-cost: 7 c ---[ 39]---> BDD-cost: 6 c ---[ 38]---> BDD-cost: 6 c ---[ 37]---> BDD-cost: 6 c ---[ 36]---> BDD-cost: 6 c ---[ 35]---> BDD-cost: 3 c ---[ 34]---> BDD-cost: 7 c ---[ 33]---> BDD-cost: 5 c ---[ 32]---> BDD-cost: 5 c ---[ 31]---> BDD-cost: 5 c ---[ 30]---> BDD-cost: 5 c ---[ 29]---> BDD-cost: 3 c ---[ 28]---> BDD-cost: 7 c ---[ 27]---> BDD-cost: 5 c ---[ 26]---> BDD-cost: 5 c ---[ 25]---> BDD-cost: 5 c ---[ 24]---> BDD-cost: 5 c ---[ 22]---> BDD-cost: 7 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 6 c ---[ 19]---> BDD-cost: 6 c ---[ 18]---> BDD-cost: 6 c ---[ 16]---> BDD-cost: 7 c ---[ 15]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 6 c ---[ 13]---> BDD-cost: 6 c ---[ 12]---> BDD-cost: 6 c ---[ 10]---> BDD-cost: 7 c ---[ 9]---> BDD-cost: 3 c ---[ 8]---> BDD-cost: 6 c ---[ 7]---> BDD-cost: 6 c ---[ 6]---> BDD-cost: 6 c ---[ 4]---> BDD-cost: 6 c ---[ 3]---> BDD-cost: 3 c ---[ 2]---> BDD-cost: 5 c ---[ 1]---> BDD-cost: 5 c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 157483 397264 | 52494 0 0 nan | 0.000 % | c | 100 | 157402 397079 | 57743 93 599 6.4 | 5.605 % | c | 250 | 157402 397079 | 63517 243 1788 7.4 | 5.605 % | c | 475 | 157263 396762 | 69869 457 3288 7.2 | 5.672 % | c | 813 | 157208 396638 | 76856 794 6792 8.6 | 5.698 % | c | 1319 | 156812 395741 | 84542 1267 10886 8.6 | 5.895 % | c | 2078 | 156456 394924 | 92996 2003 54480 27.2 | 6.075 % | c | 3217 | 156172 394286 | 102295 3121 68140 21.8 | 6.212 % | c | 4925 | 155735 393282 | 112525 4761 121732 25.6 | 6.437 % | c | 7488 | 154910 391386 | 123778 7280 209775 28.8 | 6.883 % | c | 11333 | 154139 389612 | 136155 11054 291237 26.3 | 7.263 % | c | 17099 | 153662 388518 | 149771 16795 475385 28.3 | 7.514 % | c | 25750 | 153495 388117 | 164748 25435 925575 36.4 | 7.603 % | c | 38724 | 152688 386270 | 181223 38366 1340182 34.9 | 8.010 % | c | 58185 | 151682 383823 | 199345 57753 2030081 35.2 | 8.470 % | c | 87377 | 151486 383381 | 219280 86899 3425488 39.4 | 8.574 % | c | 131166 | 150944 382147 | 241208 130636 5406999 41.4 | 8.860 % | c | 196850 | 149801 379321 | 265329 196246 7845951 40.0 | 9.425 % | c | 295377 | 149561 378749 | 291862 48914 1362935 27.9 | 9.555 % | c | 443166 | 148602 376555 | 321048 196630 7273432 37.0 | 10.086 % |
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/29150/stat): 29150 (minisat+_script) R 29149 29150 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855735044 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/29150/statm): 174 3 169 147 0 27 0 [pid=29150] 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=29151 New process pid=29152 New process pid=29153 execve syscall for /bin/sed executable One traced child (pid=29152) 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=29153) exited with status: 0 One traced child (pid=29151) exited with status: 0 New process pid=29154 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-vpm2.opb [startup+10.0037 s] Raw data (loadavg): 0.90 0.95 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 4877 0 0 0 959 18 0 0 25 0 1 0 1855735049 20553728 4672 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 5018 4672 145 145 0 4873 0 [pid=29154] vsize: 20072 Current children cumulated CPU time (s) 9.78 Current children cumulated vsize (Kb) 22196 [startup+20.0054 s] Raw data (loadavg): 0.92 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 5154 0 0 0 1954 19 0 0 25 0 1 0 1855735049 21667840 4949 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 5290 4949 145 145 0 5145 0 [pid=29154] vsize: 21160 Current children cumulated CPU time (s) 19.74 Current children cumulated vsize (Kb) 23284 [startup+30.0062 s] Raw data (loadavg): 0.93 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 5419 0 0 0 2948 22 0 0 25 0 1 0 1855735049 22794240 5214 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 5565 5214 145 145 0 5420 0 [pid=29154] vsize: 22260 Current children cumulated CPU time (s) 29.71 Current children cumulated vsize (Kb) 24384 [startup+40.0069 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 5886 0 0 0 3941 25 0 0 25 0 1 0 1855735049 24678400 5681 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 6025 5681 145 145 0 5880 0 [pid=29154] vsize: 24100 Current children cumulated CPU time (s) 39.67 Current children cumulated vsize (Kb) 26224 [startup+50.0086 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 6126 0 0 0 4935 28 0 0 25 0 1 0 1855735049 25624576 5921 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 6256 5921 145 145 0 6111 0 [pid=29154] vsize: 25024 Current children cumulated CPU time (s) 49.64 Current children cumulated vsize (Kb) 27148 [startup+60.0083 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 6354 0 0 0 5931 29 0 0 25 0 1 0 1855735049 26673152 6149 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 6512 6149 145 145 0 6367 0 [pid=29154] vsize: 26048 Current children cumulated CPU time (s) 59.61 Current children cumulated vsize (Kb) 28172 [startup+70.009 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 6551 0 0 0 6928 31 0 0 25 0 1 0 1855735049 27451392 6346 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 6702 6346 145 145 0 6557 0 [pid=29154] vsize: 26808 Current children cumulated CPU time (s) 69.6 Current children cumulated vsize (Kb) 28932 [startup+80.0097 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 6867 0 0 0 7921 33 0 0 25 0 1 0 1855735049 28712960 6662 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 7010 6662 145 145 0 6865 0 [pid=29154] vsize: 28040 Current children cumulated CPU time (s) 79.55 Current children cumulated vsize (Kb) 30164 [startup+90.0105 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 7353 0 0 0 8913 37 0 0 25 0 1 0 1855735049 30670848 7148 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 7488 7148 145 145 0 7343 0 [pid=29154] vsize: 29952 Current children cumulated CPU time (s) 89.51 Current children cumulated vsize (Kb) 32076 [startup+100.011 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 7725 0 0 0 9907 40 0 0 25 0 1 0 1855735049 32169984 7520 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 7854 7520 145 145 0 7709 0 [pid=29154] vsize: 31416 Current children cumulated CPU time (s) 99.48 Current children cumulated vsize (Kb) 33540 [startup+110.012 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8019 0 0 0 10901 42 0 0 25 0 1 0 1855735049 33619968 7814 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 8208 7814 145 145 0 8063 0 [pid=29154] vsize: 32832 Current children cumulated CPU time (s) 109.44 Current children cumulated vsize (Kb) 34956 [startup+120.013 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8246 0 0 0 11896 44 0 0 25 0 1 0 1855735049 34541568 8041 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 8433 8041 145 145 0 8288 0 [pid=29154] vsize: 33732 Current children cumulated CPU time (s) 119.41 Current children cumulated vsize (Kb) 35856 [startup+130.013 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8470 0 0 0 12893 46 0 0 25 0 1 0 1855735049 35454976 8265 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 8656 8265 145 145 0 8511 0 [pid=29154] vsize: 34624 Current children cumulated CPU time (s) 129.4 Current children cumulated vsize (Kb) 36748 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8654 0 0 0 13890 47 0 0 25 0 1 0 1855735049 36188160 8449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 8835 8449 145 145 0 8690 0 [pid=29154] vsize: 35340 Current children cumulated CPU time (s) 139.38 Current children cumulated vsize (Kb) 37464 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8830 0 0 0 14888 48 0 0 25 0 1 0 1855735049 36900864 8625 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 9009 8625 145 145 0 8864 0 [pid=29154] vsize: 36036 Current children cumulated CPU time (s) 149.37 Current children cumulated vsize (Kb) 38160 [startup+160.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8992 0 0 0 15884 51 0 0 25 0 1 0 1855735049 37556224 8787 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 9169 8787 145 145 0 9024 0 [pid=29154] vsize: 36676 Current children cumulated CPU time (s) 159.36 Current children cumulated vsize (Kb) 38800 [startup+170.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9168 0 0 0 16881 53 0 0 25 0 1 0 1855735049 38277120 8963 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 9345 8963 145 145 0 9200 0 [pid=29154] vsize: 37380 Current children cumulated CPU time (s) 169.35 Current children cumulated vsize (Kb) 39504 [startup+180.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9314 0 0 0 17878 54 0 0 25 0 1 0 1855735049 38866944 9109 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 9489 9109 145 145 0 9344 0 [pid=29154] vsize: 37956 Current children cumulated CPU time (s) 179.33 Current children cumulated vsize (Kb) 40080 [startup+190.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9463 0 0 0 18876 55 0 0 25 0 1 0 1855735049 39477248 9258 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 9638 9258 145 145 0 9493 0 [pid=29154] vsize: 38552 Current children cumulated CPU time (s) 189.32 Current children cumulated vsize (Kb) 40676 [startup+200.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9624 0 0 0 19873 56 0 0 25 0 1 0 1855735049 40124416 9419 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 9796 9419 145 145 0 9651 0 [pid=29154] vsize: 39184 Current children cumulated CPU time (s) 199.3 Current children cumulated vsize (Kb) 41308 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9841 0 0 0 20869 58 0 0 25 0 1 0 1855735049 40988672 9636 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 10007 9636 145 145 0 9862 0 [pid=29154] vsize: 40028 Current children cumulated CPU time (s) 209.28 Current children cumulated vsize (Kb) 42152 [startup+220.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 10010 0 0 0 21865 60 0 0 25 0 1 0 1855735049 41668608 9805 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 10173 9805 145 145 0 10028 0 [pid=29154] vsize: 40692 Current children cumulated CPU time (s) 219.26 Current children cumulated vsize (Kb) 42816 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 10275 0 0 0 22859 63 0 0 25 0 1 0 1855735049 42737664 10070 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 10434 10070 145 145 0 10289 0 [pid=29154] vsize: 41736 Current children cumulated CPU time (s) 229.23 Current children cumulated vsize (Kb) 43860 [startup+240.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 10517 0 0 0 23854 65 0 0 25 0 1 0 1855735049 43716608 10312 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 10673 10312 145 145 0 10528 0 [pid=29154] vsize: 42692 Current children cumulated CPU time (s) 239.2 Current children cumulated vsize (Kb) 44816 [startup+250.027 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) T 29150 29150 2660 0 -1 0 10775 0 0 0 24848 67 0 0 25 0 1 0 1855735049 44752896 10570 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/29154/statm): 10926 10570 145 145 0 10781 0 [pid=29154] vsize: 43704 Current children cumulated CPU time (s) 249.16 Current children cumulated vsize (Kb) 45828 [startup+260.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11088 0 0 0 25842 70 0 0 25 0 1 0 1855735049 46022656 10883 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 11236 10883 145 145 0 11091 0 [pid=29154] vsize: 44944 Current children cumulated CPU time (s) 259.13 Current children cumulated vsize (Kb) 47068 [startup+270.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11281 0 0 0 26840 71 0 0 25 0 1 0 1855735049 46837760 11076 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 11435 11076 145 145 0 11290 0 [pid=29154] vsize: 45740 Current children cumulated CPU time (s) 269.12 Current children cumulated vsize (Kb) 47864 [startup+280.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11423 0 0 0 27837 72 0 0 25 0 1 0 1855735049 47398912 11218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 11572 11218 145 145 0 11427 0 [pid=29154] vsize: 46288 Current children cumulated CPU time (s) 279.1 Current children cumulated vsize (Kb) 48412 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11622 0 0 0 28832 75 0 0 25 0 1 0 1855735049 48709632 11417 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 11892 11417 145 145 0 11747 0 [pid=29154] vsize: 47568 Current children cumulated CPU time (s) 289.08 Current children cumulated vsize (Kb) 49692 [startup+300.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11787 0 0 0 29830 76 0 0 25 0 1 0 1855735049 49385472 11582 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 12057 11582 145 145 0 11912 0 [pid=29154] vsize: 48228 Current children cumulated CPU time (s) 299.07 Current children cumulated vsize (Kb) 50352 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11960 0 0 0 30827 78 0 0 25 0 1 0 1855735049 50094080 11755 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 12230 11755 145 145 0 12085 0 [pid=29154] vsize: 48920 Current children cumulated CPU time (s) 309.06 Current children cumulated vsize (Kb) 51044 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 12199 0 0 0 31822 80 0 0 25 0 1 0 1855735049 51073024 11994 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 12469 11994 145 145 0 12324 0 [pid=29154] vsize: 49876 Current children cumulated CPU time (s) 319.03 Current children cumulated vsize (Kb) 52000 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) T 29150 29150 2660 0 -1 0 12444 0 0 0 32819 82 0 0 25 0 1 0 1855735049 52072448 12239 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/29154/statm): 12713 12239 145 145 0 12568 0 [pid=29154] vsize: 50852 Current children cumulated CPU time (s) 329.02 Current children cumulated vsize (Kb) 52976 [startup+340.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 12584 0 0 0 33817 83 0 0 25 0 1 0 1855735049 52625408 12379 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 12848 12379 145 145 0 12703 0 [pid=29154] vsize: 51392 Current children cumulated CPU time (s) 339.01 Current children cumulated vsize (Kb) 53516 [startup+350.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 12786 0 0 0 34814 84 0 0 25 0 1 0 1855735049 53415936 12581 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 13041 12581 145 145 0 12896 0 [pid=29154] vsize: 52164 Current children cumulated CPU time (s) 348.99 Current children cumulated vsize (Kb) 54288 [startup+360.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 12971 0 0 0 35810 86 0 0 25 0 1 0 1855735049 54157312 12766 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 13222 12766 145 145 0 13077 0 [pid=29154] vsize: 52888 Current children cumulated CPU time (s) 358.97 Current children cumulated vsize (Kb) 55012 [startup+370.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13132 0 0 0 36809 87 0 0 25 0 1 0 1855735049 54812672 12927 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 13382 12927 145 145 0 13237 0 [pid=29154] vsize: 53528 Current children cumulated CPU time (s) 368.97 Current children cumulated vsize (Kb) 55652 [startup+380.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13281 0 0 0 37806 88 0 0 25 0 1 0 1855735049 55398400 13076 4294967295 134512640 135094434 3221224432 3221223104 134556297 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 13525 13076 145 145 0 13380 0 [pid=29154] vsize: 54100 Current children cumulated CPU time (s) 378.95 Current children cumulated vsize (Kb) 56224 [startup+390.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13418 0 0 0 38804 89 0 0 25 0 1 0 1855735049 55971840 13213 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 13665 13213 145 145 0 13520 0 [pid=29154] vsize: 54660 Current children cumulated CPU time (s) 388.94 Current children cumulated vsize (Kb) 56784 [startup+400.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13586 0 0 0 39802 90 0 0 25 0 1 0 1855735049 56680448 13381 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 13838 13381 145 145 0 13693 0 [pid=29154] vsize: 55352 Current children cumulated CPU time (s) 398.93 Current children cumulated vsize (Kb) 57476 [startup+410.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13777 0 0 0 40800 91 0 0 25 0 1 0 1855735049 57446400 13572 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 14025 13572 145 145 0 13880 0 [pid=29154] vsize: 56100 Current children cumulated CPU time (s) 408.92 Current children cumulated vsize (Kb) 58224 [startup+420.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13987 0 0 0 41795 94 0 0 25 0 1 0 1855735049 58294272 13782 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 14232 13782 145 145 0 14087 0 [pid=29154] vsize: 56928 Current children cumulated CPU time (s) 418.9 Current children cumulated vsize (Kb) 59052 [startup+430.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 14256 0 0 0 42788 97 0 0 25 0 1 0 1855735049 59379712 14051 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 14497 14051 145 145 0 14352 0 [pid=29154] vsize: 57988 Current children cumulated CPU time (s) 428.86 Current children cumulated vsize (Kb) 60112 [startup+440.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 14520 0 0 0 43783 99 0 0 25 0 1 0 1855735049 60452864 14315 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 14759 14315 145 145 0 14614 0 [pid=29154] vsize: 59036 Current children cumulated CPU time (s) 438.83 Current children cumulated vsize (Kb) 61160 [startup+450.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 14700 0 0 0 44780 100 0 0 25 0 1 0 1855735049 61181952 14495 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 14937 14495 145 145 0 14792 0 [pid=29154] vsize: 59748 Current children cumulated CPU time (s) 448.81 Current children cumulated vsize (Kb) 61872 [startup+460.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 14857 0 0 0 45777 102 0 0 25 0 1 0 1855735049 61820928 14652 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29154/statm): 15093 14652 145 145 0 14948 0 [pid=29154] vsize: 60372 Current children cumulated CPU time (s) 458.8 Current children cumulated vsize (Kb) 62496 [startup+470.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15025 0 0 0 46774 104 0 0 25 0 1 0 1855735049 62500864 14820 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 15259 14820 145 145 0 15114 0 [pid=29154] vsize: 61036 Current children cumulated CPU time (s) 468.79 Current children cumulated vsize (Kb) 63160 [startup+480.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15232 0 0 0 47771 105 0 0 25 0 1 0 1855735049 63336448 15027 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 15463 15027 145 145 0 15318 0 [pid=29154] vsize: 61852 Current children cumulated CPU time (s) 478.77 Current children cumulated vsize (Kb) 63976 [startup+490.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15445 0 0 0 48766 107 0 0 25 0 1 0 1855735049 64200704 15240 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 15674 15240 145 145 0 15529 0 [pid=29154] vsize: 62696 Current children cumulated CPU time (s) 488.74 Current children cumulated vsize (Kb) 64820 [startup+500.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15570 0 0 0 49765 108 0 0 25 0 1 0 1855735049 64724992 15365 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 15802 15365 145 145 0 15657 0 [pid=29154] vsize: 63208 Current children cumulated CPU time (s) 498.74 Current children cumulated vsize (Kb) 65332 [startup+510.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15703 0 0 0 50763 109 0 0 25 0 1 0 1855735049 65241088 15498 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 15928 15498 145 145 0 15783 0 [pid=29154] vsize: 63712 Current children cumulated CPU time (s) 508.73 Current children cumulated vsize (Kb) 65836 [startup+520.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15843 0 0 0 51761 110 0 0 25 0 1 0 1855735049 65810432 15638 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 16067 15638 145 145 0 15922 0 [pid=29154] vsize: 64268 Current children cumulated CPU time (s) 518.72 Current children cumulated vsize (Kb) 66392 [startup+530.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15980 0 0 0 52759 110 0 0 25 0 1 0 1855735049 66359296 15775 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 16201 15775 145 145 0 16056 0 [pid=29154] vsize: 64804 Current children cumulated CPU time (s) 528.7 Current children cumulated vsize (Kb) 66928 [startup+540.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16109 0 0 0 53756 113 0 0 25 0 1 0 1855735049 66883584 15904 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 16329 15904 145 145 0 16184 0 [pid=29154] vsize: 65316 Current children cumulated CPU time (s) 538.7 Current children cumulated vsize (Kb) 67440 [startup+550.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16252 0 0 0 54753 115 0 0 25 0 1 0 1855735049 67485696 16047 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 16476 16047 145 145 0 16331 0 [pid=29154] vsize: 65904 Current children cumulated CPU time (s) 548.69 Current children cumulated vsize (Kb) 68028 [startup+560.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16408 0 0 0 55752 116 0 0 25 0 1 0 1855735049 68112384 16203 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 16629 16203 145 145 0 16484 0 [pid=29154] vsize: 66516 Current children cumulated CPU time (s) 558.69 Current children cumulated vsize (Kb) 68640 [startup+570.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16535 0 0 0 56749 117 0 0 25 0 1 0 1855735049 68620288 16330 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 16753 16330 145 145 0 16608 0 [pid=29154] vsize: 67012 Current children cumulated CPU time (s) 568.67 Current children cumulated vsize (Kb) 69136 [startup+580.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16672 0 0 0 57747 118 0 0 25 0 1 0 1855735049 69152768 16467 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 16883 16467 145 145 0 16738 0 [pid=29154] vsize: 67532 Current children cumulated CPU time (s) 578.66 Current children cumulated vsize (Kb) 69656 [startup+590.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16815 0 0 0 58745 119 0 0 25 0 1 0 1855735049 69763072 16610 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 17032 16610 145 145 0 16887 0 [pid=29154] vsize: 68128 Current children cumulated CPU time (s) 588.65 Current children cumulated vsize (Kb) 70252 [startup+600.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16963 0 0 0 59743 121 0 0 25 0 1 0 1855735049 70352896 16758 4294967295 134512640 135094434 3221224432 3221223104 134556401 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 17176 16758 145 145 0 17031 0 [pid=29154] vsize: 68704 Current children cumulated CPU time (s) 598.65 Current children cumulated vsize (Kb) 70828 [startup+610.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17104 0 0 0 60740 122 0 0 25 0 1 0 1855735049 70918144 16899 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 17314 16899 145 145 0 17169 0 [pid=29154] vsize: 69256 Current children cumulated CPU time (s) 608.63 Current children cumulated vsize (Kb) 71380 [startup+620.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17218 0 0 0 61737 123 0 0 25 0 1 0 1855735049 71376896 17013 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 17426 17013 145 145 0 17281 0 [pid=29154] vsize: 69704 Current children cumulated CPU time (s) 618.61 Current children cumulated vsize (Kb) 71828 [startup+630.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17330 0 0 0 62735 124 0 0 25 0 1 0 1855735049 71827456 17125 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 17536 17125 145 145 0 17391 0 [pid=29154] vsize: 70144 Current children cumulated CPU time (s) 628.6 Current children cumulated vsize (Kb) 72268 [startup+640.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17447 0 0 0 63734 125 0 0 25 0 1 0 1855735049 72310784 17242 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 17654 17242 145 145 0 17509 0 [pid=29154] vsize: 70616 Current children cumulated CPU time (s) 638.6 Current children cumulated vsize (Kb) 72740 [startup+650.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17561 0 0 0 64732 126 0 0 25 0 1 0 1855735049 72761344 17356 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 17764 17356 145 145 0 17619 0 [pid=29154] vsize: 71056 Current children cumulated CPU time (s) 648.59 Current children cumulated vsize (Kb) 73180 [startup+660.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17675 0 0 0 65730 126 0 0 25 0 1 0 1855735049 73220096 17470 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 17876 17470 145 145 0 17731 0 [pid=29154] vsize: 71504 Current children cumulated CPU time (s) 658.57 Current children cumulated vsize (Kb) 73628 [startup+670.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17785 0 0 0 66728 127 0 0 25 0 1 0 1855735049 74731520 17580 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18245 17580 145 145 0 18100 0 [pid=29154] vsize: 72980 Current children cumulated CPU time (s) 668.56 Current children cumulated vsize (Kb) 75104 [startup+680.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17880 0 0 0 67726 128 0 0 25 0 1 0 1855735049 75104256 17675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18336 17675 145 145 0 18191 0 [pid=29154] vsize: 73344 Current children cumulated CPU time (s) 678.55 Current children cumulated vsize (Kb) 75468 [startup+690.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17987 0 0 0 68725 128 0 0 25 0 1 0 1855735049 75542528 17782 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18443 17782 145 145 0 18298 0 [pid=29154] vsize: 73772 Current children cumulated CPU time (s) 688.54 Current children cumulated vsize (Kb) 75896 [startup+700.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18106 0 0 0 69723 129 0 0 25 0 1 0 1855735049 76021760 17901 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18560 17901 145 145 0 18415 0 [pid=29154] vsize: 74240 Current children cumulated CPU time (s) 698.53 Current children cumulated vsize (Kb) 76364 [startup+710.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18207 0 0 0 70721 129 0 0 25 0 1 0 1855735049 76419072 18002 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18657 18002 145 145 0 18512 0 [pid=29154] vsize: 74628 Current children cumulated CPU time (s) 708.51 Current children cumulated vsize (Kb) 76752 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 71718 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 718.5 Current children cumulated vsize (Kb) 77256 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 72718 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 728.5 Current children cumulated vsize (Kb) 77256 [startup+740.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 73719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 738.51 Current children cumulated vsize (Kb) 77256 [startup+750.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 74719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 748.51 Current children cumulated vsize (Kb) 77256 [startup+760.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 75719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223104 134556184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 758.51 Current children cumulated vsize (Kb) 77256 [startup+770.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 76719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 768.51 Current children cumulated vsize (Kb) 77256 [startup+780.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 77719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 778.51 Current children cumulated vsize (Kb) 77256 [startup+790.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 78719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 788.51 Current children cumulated vsize (Kb) 77256 [startup+800.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 79719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 798.51 Current children cumulated vsize (Kb) 77256 [startup+810.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 80720 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 808.52 Current children cumulated vsize (Kb) 77256 [startup+820.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 81719 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 818.52 Current children cumulated vsize (Kb) 77256 [startup+830.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 82720 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 828.53 Current children cumulated vsize (Kb) 77256 [startup+840.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 83720 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 838.53 Current children cumulated vsize (Kb) 77256 [startup+850.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 84720 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 848.53 Current children cumulated vsize (Kb) 77256 [startup+860.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 85720 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 858.53 Current children cumulated vsize (Kb) 77256 [startup+870.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 86721 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 868.54 Current children cumulated vsize (Kb) 77256 [startup+880.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 87720 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 878.53 Current children cumulated vsize (Kb) 77256 [startup+890.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 88721 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 888.54 Current children cumulated vsize (Kb) 77256 [startup+900.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 89721 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 898.54 Current children cumulated vsize (Kb) 77256 [startup+910.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 90721 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 908.54 Current children cumulated vsize (Kb) 77256 [startup+920.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 91721 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 918.54 Current children cumulated vsize (Kb) 77256 [startup+930.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 92722 132 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 928.55 Current children cumulated vsize (Kb) 77256 [startup+940.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 93722 132 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 938.55 Current children cumulated vsize (Kb) 77256 [startup+950.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 94722 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 948.56 Current children cumulated vsize (Kb) 77256 [startup+960.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 95722 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 958.56 Current children cumulated vsize (Kb) 77256 [startup+970.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 96722 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 968.56 Current children cumulated vsize (Kb) 77256 [startup+980.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 97722 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 978.56 Current children cumulated vsize (Kb) 77256 [startup+990.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 98723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 988.57 Current children cumulated vsize (Kb) 77256 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 99723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 998.57 Current children cumulated vsize (Kb) 77256 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 100723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1008.57 Current children cumulated vsize (Kb) 77256 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 101723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1018.57 Current children cumulated vsize (Kb) 77256 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 102723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1028.57 Current children cumulated vsize (Kb) 77256 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 103724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1038.58 Current children cumulated vsize (Kb) 77256 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 104724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1048.58 Current children cumulated vsize (Kb) 77256 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 105724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1058.58 Current children cumulated vsize (Kb) 77256 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 106724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1068.58 Current children cumulated vsize (Kb) 77256 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 107724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1078.58 Current children cumulated vsize (Kb) 77256 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18341 0 0 0 108725 133 0 0 25 0 1 0 1855735049 76935168 18136 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18136 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1088.59 Current children cumulated vsize (Kb) 77256 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18341 0 0 0 109725 133 0 0 25 0 1 0 1855735049 76935168 18136 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18136 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1098.59 Current children cumulated vsize (Kb) 77256 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18343 0 0 0 110725 133 0 0 25 0 1 0 1855735049 76935168 18138 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18783 18138 145 145 0 18638 0 [pid=29154] vsize: 75132 Current children cumulated CPU time (s) 1108.59 Current children cumulated vsize (Kb) 77256 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 111725 133 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223056 134557577 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1118.59 Current children cumulated vsize (Kb) 77316 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 112725 133 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1128.59 Current children cumulated vsize (Kb) 77316 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 113724 135 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1138.6 Current children cumulated vsize (Kb) 77316 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 114723 135 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223104 134556496 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1148.59 Current children cumulated vsize (Kb) 77316 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 115723 136 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1158.6 Current children cumulated vsize (Kb) 77316 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 116723 136 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1168.6 Current children cumulated vsize (Kb) 77316 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 117723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223104 134556020 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1178.61 Current children cumulated vsize (Kb) 77316 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 118723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1188.61 Current children cumulated vsize (Kb) 77316 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 119723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1198.61 Current children cumulated vsize (Kb) 77316 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 120723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1208.61 Current children cumulated vsize (Kb) 77316 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 29154 Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29150/statm): 531 226 485 147 0 384 0 [pid=29150] vsize: 2124 Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 120723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0 [pid=29154] vsize: 75192 Current children cumulated CPU time (s) 1208.61 Current children cumulated vsize (Kb) 77316 Sending SIGTERM to -29150 Sleeping 2 seconds One traced child (pid=29150) ended because it received signal 15 (SIGTERM) One traced child (pid=29154) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.14 CPU time (s): 1208.65 CPU user time (s): 1207.24 CPU system time (s): 1.41079 CPU usage (%): 99.8767 Max. virtual memory (cumulated for all children) (Kb): 77316
ERROR: no interpretation found !