Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-israel.opb |
MD5SUM | 7ba5c7ed3d893d37e85d9935730a0f21 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -86917125500 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2670 |
Biggest coefficient in the objective function | 807185416192000 |
Number of bits for the biggest coefficient in the objective function | 50 |
Sum of the numbers in the objective function | 9901243932822396 |
Number of bits of the sum of numbers in the objective function | 54 |
Biggest number in a constraint | 807185416192000 |
Number of bits of the biggest number in a constraint | 50 |
Biggest sum of numbers in a constraint | 9901243932822396 |
Number of bits of the biggest sum of numbers | 54 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 731.752 |
Number of variables | 4260 |
Total number of constraints | 174 |
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 | 174 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 3540 |
LAUNCH ON wulflinc19 THE 2005-09-18 20:20:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2783 boxname=wulflinc19 idbench=439 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 7ba5c7ed3d893d37e85d9935730a0f21 /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-israel.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-israel.opb IDLAUNCH: 2783 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 920872 kB Buffers: 34592 kB Cached: 51888 kB SwapCached: 832 kB Active: 61864 kB Inactive: 27248 kB HighTotal: 131008 kB HighFree: 78372 kB LowTotal: 903652 kB LowFree: 842500 kB SwapTotal: 2097892 kB SwapFree: 2096460 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 19100 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:41:04 (client local time) WITH STATUS 0 IN 1209.83 SECONDS stats: 2783 7 1209.83 0
c Parsing PB file... c PARSE ERROR! [line 146] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 174 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ssssssss c ---[ 181]---> Adder-cost: 1424 maxlim: 155461596 bits: 28/28 c ---[ 179]---> Sorter-cost: 3962 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[ 178]---> Sorter-cost: 4599 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 177]---> Sorter-cost: 4395 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 176]---> Sorter-cost: 4395 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 175]---> Sorter-cost: 4395 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 174]---> Sorter-cost: 4395 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 c ---[ 173]---> Sorter-cost: 4455 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2 c ---[ 172]---> Sorter-cost: 4295 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 4295 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 3 5 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 4942 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 3789 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[ 167]---> Sorter-cost: 2167 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 c ---[ 166]---> Sorter-cost: 1672 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 165]---> Sorter-cost: 1735 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 2083 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 163]---> Sorter-cost: 2351 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 3110 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 c ---[ 161]---> Sorter-cost: 2860 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 160]---> Sorter-cost: 2983 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 159]---> Sorter-cost: 3410 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[ 158]---> Sorter-cost: 696 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[ 157]---> Sorter-cost: 3209 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 c ---[ 156]---> Sorter-cost: 2871 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 c ---[ 155]---> Sorter-cost: 2914 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 154]---> Sorter-cost: 2827 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 153]---> Sorter-cost: 2826 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 152]---> Sorter-cost: 2826 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 151]---> Sorter-cost: 2825 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 150]---> Sorter-cost: 2825 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 149]---> Sorter-cost: 2825 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 148]---> Sorter-cost: 2826 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 147]---> Adder-cost: 616 maxlim: 600882799 bits: 30/30 c ---[ 146]---> Sorter-cost: 2822 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 145]---> Sorter-cost: 2826 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 144]---> Sorter-cost: 2825 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 c ---[ 143]---> Adder-cost: 608 maxlim: 681572099 bits: 30/30 c ---[ 142]---> Adder-cost: 567 maxlim: 366999295 bits: 29/29 c ---[ 141]---> Adder-cost: 576 maxlim: 366999291 bits: 29/29 c ---[ 140]---> Adder-cost: 564 maxlim: 366999287 bits: 29/29 c ---[ 139]---> Adder-cost: 564 maxlim: 366999283 bits: 29/29 c ---[ 138]---> Adder-cost: 564 maxlim: 366999279 bits: 29/29 c ---[ 137]---> Adder-cost: 564 maxlim: 366999275 bits: 29/29 c ---[ 136]---> Sorter-cost: 1225 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 135]---> Adder-cost: 564 maxlim: 366999270 bits: 29/29 c ---
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/13256/stat): 13256 (minisat+_script) R 13255 13256 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844075397 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/13256/statm): 174 3 169 147 0 27 0 [pid=13256] 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=13257 New process pid=13258 New process pid=13259 execve syscall for /bin/sed executable One traced child (pid=13258) 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=13259) exited with status: 0 One traced child (pid=13257) exited with status: 0 New process pid=13260 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-israel.opb One traced child (pid=13260) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=13261 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-israel.opb [startup+10.0035 s] Raw data (loadavg): 0.93 0.95 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1577 0 3 0 957 11 0 0 25 0 1 0 1844075403 6258688 1390 4294967295 134512640 135167914 3221224448 3221220400 134849061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 1528 1390 162 162 0 1366 0 [pid=13261] vsize: 6112 Current children cumulated CPU time (s) 9.7 Current children cumulated vsize (Kb) 8240 [startup+20.0043 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1577 0 3 0 1957 11 0 0 25 0 1 0 1844075403 6258688 1390 4294967295 134512640 135167914 3221224448 3221220016 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 1528 1390 162 162 0 1366 0 [pid=13261] vsize: 6112 Current children cumulated CPU time (s) 19.7 Current children cumulated vsize (Kb) 8240 [startup+30.0051 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1589 0 3 0 2956 11 0 0 25 0 1 0 1844075403 6455296 1402 4294967295 134512640 135167914 3221224448 3221220204 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 1576 1402 162 162 0 1414 0 [pid=13261] vsize: 6304 Current children cumulated CPU time (s) 29.69 Current children cumulated vsize (Kb) 8432 [startup+40.0069 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1703 0 3 0 3955 12 0 0 25 0 1 0 1844075403 6643712 1474 4294967295 134512640 135167914 3221224448 3221219360 134629285 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 1622 1474 162 162 0 1460 0 [pid=13261] vsize: 6488 Current children cumulated CPU time (s) 39.69 Current children cumulated vsize (Kb) 8616 [startup+50.0077 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1738 0 3 0 4955 12 0 0 25 0 1 0 1844075403 7127040 1509 4294967295 134512640 135167914 3221224448 3221221088 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 1740 1509 162 162 0 1578 0 [pid=13261] vsize: 6960 Current children cumulated CPU time (s) 49.69 Current children cumulated vsize (Kb) 9088 [startup+60.0076 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 1807 0 3 0 5955 12 0 0 25 0 1 0 1844075403 7307264 1578 4294967295 134512640 135167914 3221224448 3221219792 134845890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 1784 1578 162 162 0 1622 0 [pid=13261] vsize: 7136 Current children cumulated CPU time (s) 59.69 Current children cumulated vsize (Kb) 9264 [startup+70.0094 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2036 0 3 0 6953 13 0 0 25 0 1 0 1844075403 7806976 1724 4294967295 134512640 135167914 3221224448 3221220576 134843001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 1906 1724 162 162 0 1744 0 [pid=13261] vsize: 7624 Current children cumulated CPU time (s) 69.68 Current children cumulated vsize (Kb) 9752 [startup+80.0102 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2142 0 3 0 7952 14 0 0 25 0 1 0 1844075403 8081408 1830 4294967295 134512640 135167914 3221224448 3221221792 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 1973 1830 162 162 0 1811 0 [pid=13261] vsize: 7892 Current children cumulated CPU time (s) 79.68 Current children cumulated vsize (Kb) 10020 [startup+90.011 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2295 0 3 0 8951 14 0 0 25 0 1 0 1844075403 9265152 1983 4294967295 134512640 135167914 3221224448 3221221948 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 2262 1983 162 162 0 2100 0 [pid=13261] vsize: 9048 Current children cumulated CPU time (s) 89.67 Current children cumulated vsize (Kb) 11176 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2738 0 3 0 9950 15 0 0 25 0 1 0 1844075403 10235904 2261 4294967295 134512640 135167914 3221224448 3221221824 134630940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 2499 2261 162 162 0 2337 0 [pid=13261] vsize: 9996 Current children cumulated CPU time (s) 99.67 Current children cumulated vsize (Kb) 12124 [startup+110.013 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2798 0 3 0 10949 16 0 0 25 0 1 0 1844075403 10407936 2321 4294967295 134512640 135167914 3221224448 3221220940 134693728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 2541 2321 162 162 0 2379 0 [pid=13261] vsize: 10164 Current children cumulated CPU time (s) 109.67 Current children cumulated vsize (Kb) 12292 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2866 0 3 0 11949 16 0 0 25 0 1 0 1844075403 10571776 2389 4294967295 134512640 135167914 3221224448 3221221792 134843015 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 2581 2389 162 162 0 2419 0 [pid=13261] vsize: 10324 Current children cumulated CPU time (s) 119.67 Current children cumulated vsize (Kb) 12452 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2934 0 3 0 12948 16 0 0 25 0 1 0 1844075403 10752000 2457 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 2625 2457 162 162 0 2463 0 [pid=13261] vsize: 10500 Current children cumulated CPU time (s) 129.66 Current children cumulated vsize (Kb) 12628 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2950 0 3 0 13948 17 0 0 25 0 1 0 1844075403 10792960 2473 4294967295 134512640 135167914 3221224448 3221221740 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 2635 2473 162 162 0 2473 0 [pid=13261] vsize: 10540 Current children cumulated CPU time (s) 139.67 Current children cumulated vsize (Kb) 12668 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2982 0 3 0 14948 17 0 0 25 0 1 0 1844075403 10874880 2505 4294967295 134512640 135167914 3221224448 3221219632 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13261/statm): 2655 2505 162 162 0 2493 0 [pid=13261] vsize: 10620 Current children cumulated CPU time (s) 149.67 Current children cumulated vsize (Kb) 12748 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 2997 0 3 0 15946 19 0 0 25 0 1 0 1844075403 10915840 2520 4294967295 134512640 135167914 3221224448 3221220912 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 2665 2520 162 162 0 2503 0 [pid=13261] vsize: 10660 Current children cumulated CPU time (s) 159.67 Current children cumulated vsize (Kb) 12788 [startup+170.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3011 0 3 0 16946 19 0 0 25 0 1 0 1844075403 10948608 2534 4294967295 134512640 135167914 3221224448 3221220832 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 2673 2534 162 162 0 2511 0 [pid=13261] vsize: 10692 Current children cumulated CPU time (s) 169.67 Current children cumulated vsize (Kb) 12820 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3027 0 3 0 17946 19 0 0 25 0 1 0 1844075403 12558336 2550 4294967295 134512640 135167914 3221224448 3221220672 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3066 2550 162 162 0 2904 0 [pid=13261] vsize: 12264 Current children cumulated CPU time (s) 179.67 Current children cumulated vsize (Kb) 14392 [startup+190.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3130 0 3 0 18945 19 0 0 25 0 1 0 1844075403 12832768 2653 4294967295 134512640 135167914 3221224448 3221221840 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3133 2653 162 162 0 2971 0 [pid=13261] vsize: 12532 Current children cumulated CPU time (s) 189.66 Current children cumulated vsize (Kb) 14660 [startup+200.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3193 0 3 0 19945 19 0 0 25 0 1 0 1844075403 13029376 2716 4294967295 134512640 135167914 3221224448 3221220724 134845880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3181 2716 162 162 0 3019 0 [pid=13261] vsize: 12724 Current children cumulated CPU time (s) 199.66 Current children cumulated vsize (Kb) 14852 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3193 0 3 0 20945 19 0 0 25 0 1 0 1844075403 13029376 2716 4294967295 134512640 135167914 3221224448 3221220180 134845938 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3181 2716 162 162 0 3019 0 [pid=13261] vsize: 12724 Current children cumulated CPU time (s) 209.66 Current children cumulated vsize (Kb) 14852 [startup+220.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3193 0 3 0 21945 20 0 0 25 0 1 0 1844075403 13029376 2716 4294967295 134512640 135167914 3221224448 3221221904 134845906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3181 2716 162 162 0 3019 0 [pid=13261] vsize: 12724 Current children cumulated CPU time (s) 219.67 Current children cumulated vsize (Kb) 14852 [startup+230.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3207 0 3 0 22946 20 0 0 25 0 1 0 1844075403 13029376 2730 4294967295 134512640 135167914 3221224448 3221188076 134618900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3181 2730 162 162 0 3019 0 [pid=13261] vsize: 12724 Current children cumulated CPU time (s) 229.68 Current children cumulated vsize (Kb) 14852 [startup+240.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3215 0 3 0 23946 20 0 0 25 0 1 0 1844075403 13062144 2738 4294967295 134512640 135167914 3221224448 3221218912 134696738 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3189 2738 162 162 0 3027 0 [pid=13261] vsize: 12756 Current children cumulated CPU time (s) 239.68 Current children cumulated vsize (Kb) 14884 [startup+250.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3215 0 3 0 24946 20 0 0 25 0 1 0 1844075403 13062144 2738 4294967295 134512640 135167914 3221224448 3221220220 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3189 2738 162 162 0 3027 0 [pid=13261] vsize: 12756 Current children cumulated CPU time (s) 249.68 Current children cumulated vsize (Kb) 14884 [startup+260.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3215 0 3 0 25946 20 0 0 25 0 1 0 1844075403 13062144 2738 4294967295 134512640 135167914 3221224448 3221220176 134718188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3189 2738 162 162 0 3027 0 [pid=13261] vsize: 12756 Current children cumulated CPU time (s) 259.68 Current children cumulated vsize (Kb) 14884 [startup+270.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3215 0 3 0 26946 20 0 0 25 0 1 0 1844075403 13062144 2738 4294967295 134512640 135167914 3221224448 3221222192 134844676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3189 2738 162 162 0 3027 0 [pid=13261] vsize: 12756 Current children cumulated CPU time (s) 269.68 Current children cumulated vsize (Kb) 14884 [startup+280.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 27946 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221220152 134693621 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0 [pid=13261] vsize: 12820 Current children cumulated CPU time (s) 279.68 Current children cumulated vsize (Kb) 14948 [startup+290.027 s] Raw data (loadavg): 1.07 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 28946 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221221004 134718182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0 [pid=13261] vsize: 12820 Current children cumulated CPU time (s) 289.68 Current children cumulated vsize (Kb) 14948 [startup+300.028 s] Raw data (loadavg): 1.06 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 29947 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221221052 134722225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0 [pid=13261] vsize: 12820 Current children cumulated CPU time (s) 299.69 Current children cumulated vsize (Kb) 14948 [startup+310.028 s] Raw data (loadavg): 1.05 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 30946 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221222160 134849110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0 [pid=13261] vsize: 12820 Current children cumulated CPU time (s) 309.68 Current children cumulated vsize (Kb) 14948 [startup+320.029 s] Raw data (loadavg): 1.04 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3240 0 3 0 31947 20 0 0 25 0 1 0 1844075403 13127680 2763 4294967295 134512640 135167914 3221224448 3221221888 134845906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3205 2763 162 162 0 3043 0 [pid=13261] vsize: 12820 Current children cumulated CPU time (s) 319.69 Current children cumulated vsize (Kb) 14948 [startup+330.029 s] Raw data (loadavg): 1.04 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 32947 20 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221220928 134849068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 329.69 Current children cumulated vsize (Kb) 15004 [startup+340.03 s] Raw data (loadavg): 1.03 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 33947 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221219616 134843420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 339.7 Current children cumulated vsize (Kb) 15004 [startup+350.031 s] Raw data (loadavg): 1.03 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 34947 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221416 134845877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 349.7 Current children cumulated vsize (Kb) 15004 [startup+360.032 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 35948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221024 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 359.71 Current children cumulated vsize (Kb) 15004 [startup+370.033 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 36948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221152 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 369.71 Current children cumulated vsize (Kb) 15004 [startup+380.032 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 37948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221219644 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 379.71 Current children cumulated vsize (Kb) 15004 [startup+390.033 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 38948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221220304 134845906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 389.71 Current children cumulated vsize (Kb) 15004 [startup+400.034 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 39948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221024 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 399.71 Current children cumulated vsize (Kb) 15004 [startup+410.034 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 40948 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221616 134849122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 409.71 Current children cumulated vsize (Kb) 15004 [startup+420.035 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3262 0 3 0 41949 21 0 0 25 0 1 0 1844075403 13185024 2785 4294967295 134512640 135167914 3221224448 3221221424 134722532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3219 2785 162 162 0 3057 0 [pid=13261] vsize: 12876 Current children cumulated CPU time (s) 419.72 Current children cumulated vsize (Kb) 15004 [startup+430.035 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3276 0 3 0 42949 21 0 0 25 0 1 0 1844075403 13238272 2799 4294967295 134512640 135167914 3221224448 3221220764 134694480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3232 2799 162 162 0 3070 0 [pid=13261] vsize: 12928 Current children cumulated CPU time (s) 429.72 Current children cumulated vsize (Kb) 15056 [startup+440.036 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3276 0 3 0 43949 21 0 0 25 0 1 0 1844075403 13238272 2799 4294967295 134512640 135167914 3221224448 3221221440 134843064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3232 2799 162 162 0 3070 0 [pid=13261] vsize: 12928 Current children cumulated CPU time (s) 439.72 Current children cumulated vsize (Kb) 15056 [startup+450.037 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3280 0 3 0 44949 21 0 0 25 0 1 0 1844075403 13238272 2803 4294967295 134512640 135167914 3221224448 3221220704 134849110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3232 2803 162 162 0 3070 0 [pid=13261] vsize: 12928 Current children cumulated CPU time (s) 449.72 Current children cumulated vsize (Kb) 15056 [startup+460.037 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3280 0 3 0 45950 21 0 0 25 0 1 0 1844075403 13238272 2803 4294967295 134512640 135167914 3221224448 3221220528 134722521 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3232 2803 162 162 0 3070 0 [pid=13261] vsize: 12928 Current children cumulated CPU time (s) 459.73 Current children cumulated vsize (Kb) 15056 [startup+470.038 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3304 0 3 0 46950 21 0 0 25 0 1 0 1844075403 13295616 2827 4294967295 134512640 135167914 3221224448 3221220116 134844636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3246 2827 162 162 0 3084 0 [pid=13261] vsize: 12984 Current children cumulated CPU time (s) 469.73 Current children cumulated vsize (Kb) 15112 [startup+480.038 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3304 0 3 0 47950 21 0 0 25 0 1 0 1844075403 13295616 2827 4294967295 134512640 135167914 3221224448 3221220848 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3246 2827 162 162 0 3084 0 [pid=13261] vsize: 12984 Current children cumulated CPU time (s) 479.73 Current children cumulated vsize (Kb) 15112 [startup+490.039 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3304 0 3 0 48950 21 0 0 25 0 1 0 1844075403 13295616 2827 4294967295 134512640 135167914 3221224448 3221221456 134849061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3246 2827 162 162 0 3084 0 [pid=13261] vsize: 12984 Current children cumulated CPU time (s) 489.73 Current children cumulated vsize (Kb) 15112 [startup+500.04 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 49950 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221220656 134844672 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0 [pid=13261] vsize: 13032 Current children cumulated CPU time (s) 499.73 Current children cumulated vsize (Kb) 15160 [startup+510.04 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 50950 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221220912 134694517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0 [pid=13261] vsize: 13032 Current children cumulated CPU time (s) 509.73 Current children cumulated vsize (Kb) 15160 [startup+520.041 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 51951 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221219488 134849148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0 [pid=13261] vsize: 13032 Current children cumulated CPU time (s) 519.74 Current children cumulated vsize (Kb) 15160 [startup+530.041 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 52951 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221221744 134843139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0 [pid=13261] vsize: 13032 Current children cumulated CPU time (s) 529.74 Current children cumulated vsize (Kb) 15160 [startup+540.042 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3323 0 3 0 53951 21 0 0 25 0 1 0 1844075403 13344768 2846 4294967295 134512640 135167914 3221224448 3221221964 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3258 2846 162 162 0 3096 0 [pid=13261] vsize: 13032 Current children cumulated CPU time (s) 539.74 Current children cumulated vsize (Kb) 15160 [startup+550.043 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 3370 0 3 0 54951 22 0 0 25 0 1 0 1844075403 13537280 2893 4294967295 134512640 135167914 3221224448 3221221792 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3305 2893 162 162 0 3143 0 [pid=13261] vsize: 13220 Current children cumulated CPU time (s) 549.75 Current children cumulated vsize (Kb) 15348 [startup+560.043 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 4096 0 3 0 55949 23 0 0 25 0 1 0 1844075403 15024128 3289 4294967295 134512640 135167914 3221224448 3221222112 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3668 3289 162 162 0 3506 0 [pid=13261] vsize: 14672 Current children cumulated CPU time (s) 559.74 Current children cumulated vsize (Kb) 16800 [startup+570.044 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 4101 0 3 0 56949 23 0 0 25 0 1 0 1844075403 15024128 3294 4294967295 134512640 135167914 3221224448 3221221728 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 3668 3294 162 162 0 3506 0 [pid=13261] vsize: 14672 Current children cumulated CPU time (s) 569.74 Current children cumulated vsize (Kb) 16800 [startup+580.045 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 57934 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217744 134843012 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 579.68 Current children cumulated vsize (Kb) 21728 [startup+590.045 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 58934 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217216 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 589.68 Current children cumulated vsize (Kb) 21728 [startup+600.046 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 59934 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217680 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 599.68 Current children cumulated vsize (Kb) 21728 [startup+610.047 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 60935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218016 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 609.69 Current children cumulated vsize (Kb) 21728 [startup+620.048 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 61935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217856 134696298 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 619.69 Current children cumulated vsize (Kb) 21728 [startup+630.048 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 62935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218032 134844708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 629.69 Current children cumulated vsize (Kb) 21728 [startup+640.049 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 63935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217912 134845877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 639.69 Current children cumulated vsize (Kb) 21728 [startup+650.05 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 64935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218468 134849086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 649.69 Current children cumulated vsize (Kb) 21728 [startup+660.05 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 65935 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217944 134693553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 659.69 Current children cumulated vsize (Kb) 21728 [startup+670.051 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 66936 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218596 134845938 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 669.7 Current children cumulated vsize (Kb) 21728 [startup+680.052 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 67936 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217720 134845939 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 679.7 Current children cumulated vsize (Kb) 21728 [startup+690.053 s] Raw data (loadavg): 1.08 1.00 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 68936 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218076 134844675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 689.7 Current children cumulated vsize (Kb) 21728 [startup+700.053 s] Raw data (loadavg): 1.07 1.00 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 69936 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218060 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 699.7 Current children cumulated vsize (Kb) 21728 [startup+710.054 s] Raw data (loadavg): 1.06 1.00 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 70937 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218224 134696598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 709.71 Current children cumulated vsize (Kb) 21728 [startup+720.055 s] Raw data (loadavg): 1.05 1.00 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 71937 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218824 134696561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 719.71 Current children cumulated vsize (Kb) 21728 [startup+730.056 s] Raw data (loadavg): 1.04 1.00 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 72937 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218032 134844689 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 729.71 Current children cumulated vsize (Kb) 21728 [startup+740.057 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 73937 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218020 134844636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 739.71 Current children cumulated vsize (Kb) 21728 [startup+750.057 s] Raw data (loadavg): 1.11 1.02 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 74938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218040 134693686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 749.72 Current children cumulated vsize (Kb) 21728 [startup+760.058 s] Raw data (loadavg): 1.09 1.02 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 75938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217280 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 759.72 Current children cumulated vsize (Kb) 21728 [startup+770.059 s] Raw data (loadavg): 1.08 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 76938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218128 134630738 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 769.72 Current children cumulated vsize (Kb) 21728 [startup+780.06 s] Raw data (loadavg): 1.06 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 77938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218400 134723225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 779.72 Current children cumulated vsize (Kb) 21728 [startup+790.061 s] Raw data (loadavg): 1.05 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 78938 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218928 134696587 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 789.72 Current children cumulated vsize (Kb) 21728 [startup+800.061 s] Raw data (loadavg): 1.04 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 79939 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218192 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 799.73 Current children cumulated vsize (Kb) 21728 [startup+810.061 s] Raw data (loadavg): 1.04 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 80939 32 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217708 134723206 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 809.73 Current children cumulated vsize (Kb) 21728 [startup+820.063 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 81939 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217936 134849068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 819.74 Current children cumulated vsize (Kb) 21728 [startup+830.063 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 82939 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217568 134849179 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 829.74 Current children cumulated vsize (Kb) 21728 [startup+840.064 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 83939 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218260 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 839.74 Current children cumulated vsize (Kb) 21728 [startup+850.064 s] Raw data (loadavg): 1.02 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 84939 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221219200 134844703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 849.74 Current children cumulated vsize (Kb) 21728 [startup+860.064 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 85940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218292 134843000 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 859.75 Current children cumulated vsize (Kb) 21728 [startup+870.065 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 86940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217376 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 869.75 Current children cumulated vsize (Kb) 21728 [startup+880.066 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 87940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218320 134844676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 879.75 Current children cumulated vsize (Kb) 21728 [startup+890.067 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 88940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218640 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 889.75 Current children cumulated vsize (Kb) 21728 [startup+900.067 s] Raw data (loadavg): 1.01 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 89940 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221219200 134629448 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 899.75 Current children cumulated vsize (Kb) 21728 [startup+910.068 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 90941 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217884 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 909.76 Current children cumulated vsize (Kb) 21728 [startup+920.069 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 91941 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217888 134845937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 919.76 Current children cumulated vsize (Kb) 21728 [startup+930.069 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 92941 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218652 134694480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 929.76 Current children cumulated vsize (Kb) 21728 [startup+940.07 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 93941 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218112 134522189 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 939.76 Current children cumulated vsize (Kb) 21728 [startup+950.071 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 94942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218400 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 949.77 Current children cumulated vsize (Kb) 21728 [startup+960.071 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 95942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218496 134845906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 959.77 Current children cumulated vsize (Kb) 21728 [startup+970.072 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 96942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218652 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 969.77 Current children cumulated vsize (Kb) 21728 [startup+980.072 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 97942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218736 134845930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 979.77 Current children cumulated vsize (Kb) 21728 [startup+990.073 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 98942 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217920 134843130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 989.77 Current children cumulated vsize (Kb) 21728 [startup+1000.07 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 99943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218448 134843130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 999.78 Current children cumulated vsize (Kb) 21728 [startup+1010.07 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 100943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218288 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1009.78 Current children cumulated vsize (Kb) 21728 [startup+1020.07 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 101943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218920 134693629 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1019.78 Current children cumulated vsize (Kb) 21728 [startup+1030.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 102943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218800 134843064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1029.78 Current children cumulated vsize (Kb) 21728 [startup+1040.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 103943 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221219308 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1039.78 Current children cumulated vsize (Kb) 21728 [startup+1050.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 104944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218972 134722225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1049.79 Current children cumulated vsize (Kb) 21728 [startup+1060.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 105944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218080 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1059.79 Current children cumulated vsize (Kb) 21728 [startup+1070.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 106944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217568 134849113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1069.79 Current children cumulated vsize (Kb) 21728 [startup+1080.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 107944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218448 134694504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1079.79 Current children cumulated vsize (Kb) 21728 [startup+1090.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 108944 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218464 134849071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1089.79 Current children cumulated vsize (Kb) 21728 [startup+1100.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 109945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217392 134843130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1099.8 Current children cumulated vsize (Kb) 21728 [startup+1110.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 110945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218284 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1109.8 Current children cumulated vsize (Kb) 21728 [startup+1120.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 111945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218468 134522233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1119.8 Current children cumulated vsize (Kb) 21728 [startup+1130.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 112945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218796 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1129.8 Current children cumulated vsize (Kb) 21728 [startup+1140.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 113945 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218048 134843030 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1139.8 Current children cumulated vsize (Kb) 21728 [startup+1150.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 114946 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218448 134843064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1149.81 Current children cumulated vsize (Kb) 21728 [startup+1160.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 115946 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218240 134695313 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1159.81 Current children cumulated vsize (Kb) 21728 [startup+1170.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 116946 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218252 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1169.81 Current children cumulated vsize (Kb) 21728 [startup+1180.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 117946 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218736 134696395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1179.81 Current children cumulated vsize (Kb) 21728 [startup+1190.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 118947 33 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221218032 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1189.82 Current children cumulated vsize (Kb) 21728 [startup+1200.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 119947 34 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217856 134843404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1199.83 Current children cumulated vsize (Kb) 21728 [startup+1210.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 120947 34 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217920 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1209.83 Current children cumulated vsize (Kb) 21728 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 13261 Raw data (/proc/13256/stat): 13256 (minisat+_script) S 13255 13256 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1844075397 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13256/statm): 532 234 485 147 0 385 0 [pid=13256] vsize: 2128 Raw data (/proc/13261/stat): 13261 (minisat+_bignum) R 13256 13256 5929 0 -1 0 6012 0 3 0 120947 34 0 0 25 0 1 0 1844075403 20070400 4585 4294967295 134512640 135167914 3221224448 3221217920 134849110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13261/statm): 4900 4585 162 162 0 4738 0 [pid=13261] vsize: 19600 Current children cumulated CPU time (s) 1209.83 Current children cumulated vsize (Kb) 21728 Sending SIGTERM to -13256 Sleeping 2 seconds One traced child (pid=13256) ended because it received signal 15 (SIGTERM) One traced child (pid=13261) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.1 CPU time (s): 1209.83 CPU user time (s): 1209.48 CPU system time (s): 0.350946 CPU usage (%): 99.9771 Max. virtual memory (cumulated for all children) (Kb): 21728
ERROR: no interpretation found !