Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-recipe.opb |
MD5SUM | 3ed8b1557bef6552695b255ca35679eb |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -107049521 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1055 |
Biggest coefficient in the objective function | 65536000 |
Number of bits for the biggest coefficient in the objective function | 26 |
Sum of the numbers in the objective function | 584330055 |
Number of bits of the sum of numbers in the objective function | 30 |
Biggest number in a constraint | 5681631310381056 |
Number of bits of the biggest number in a constraint | 53 |
Biggest sum of numbers in a constraint | 98271137637301167 |
Number of bits of the biggest sum of numbers | 57 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1260.57 |
Number of variables | 3671 |
Total number of constraints | 159 |
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 | 159 |
Minimum length of a constraint | 10 |
Maximum length of a constraint | 420 |
LAUNCH ON wulflinc7 THE 2005-09-18 20:30:00 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2796 boxname=wulflinc7 idbench=452 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3ed8b1557bef6552695b255ca35679eb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-recipe.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-recipe.opb IDLAUNCH: 2796 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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 : 2 cpu MHz : 451.050 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: 908236 kB Buffers: 35824 kB Cached: 66116 kB SwapCached: 740 kB Active: 70032 kB Inactive: 34512 kB HighTotal: 131008 kB HighFree: 62804 kB LowTotal: 903652 kB LowFree: 845432 kB SwapTotal: 2097136 kB SwapFree: 2095892 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5716 kB Slab: 16304 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 20:50:00 (client local time) WITH STATUS 0 IN 1199.96 SECONDS stats: 2796 7 1199.96 0
c Parsing PB file... c PARSE ERROR! [line 332] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 201 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ################################################### c -- Clauses(.)/Splits(s): sssssssss c ---[ 209]---> BDD-cost: 16 c ---[ 208]---> BDD-cost: 15 c ---[ 207]---> BDD-cost: 16 c ---[ 205]---> BDD-cost: 14 c ---[ 202]---> BDD-cost: 16 c ---[ 200]---> BDD-cost: 15 c ---[ 199]---> BDD-cost: 15 c ---[ 191]---> BDD-cost: 15 c ---[ 190]---> BDD-cost: 14 c ---[ 189]---> BDD-cost: 16 c ---[ 187]---> BDD-cost: 13 c ---[ 186]---> BDD-cost: 11 c ---[ 182]---> BDD-cost: 15 c ---[ 173]---> BDD-cost: 15 c ---[ 171]---> BDD-cost: 14 c ---[ 170]---> BDD-cost: 13 c ---[ 169]---> BDD-cost: 12 c ---[ 168]---> BDD-cost: 11 c ---[ 153]---> BDD-cost: 14 c ---[ 152]---> BDD-cost: 13 c ---[ 150]---> BDD-cost: 11 c ---[ 147]---> BDD-cost: 14 c ---[ 146]---> BDD-cost: 14 c ---[ 145]---> BDD-cost: 14 c ---[ 144]---> BDD-cost: 14 c ---[ 143]---> BDD-cost: 14 c ---[ 142]---> BDD-cost: 14 c ---[ 141]---> BDD-cost: 14 c ---[ 139]---> Adder-cost: 752 maxlim: 6710886300 bits: 34/33 c ---[ 137]---> Adder-cost: 670 maxlim: 671088630 bits: 30/30 c ---[ 135]---> Adder-cost: 819 maxlim: 13421772600 bits: 35/34 c ---[ 133]---> Adder-cost: 668 maxlim: 671088630 bits: 30/30 c ---[ 131]---> Sorter-cost: 2270 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 129]---> Adder-cost: 676 maxlim: 671088630 bits: 30/30 c ---[ 127]---> BDD-cost: 85 c ---[ 125]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 123]---> Sorter-cost: 385 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 121]---> Sorter-cost: 622 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> Sorter-cost: 566 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 117]---> BDD-cost: 128 c ---[ 115]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 362 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 111]---> Sorter-cost: 592 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 109]---> Sorter-cost: 530 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> BDD-cost: 131 c ---[ 105]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 385 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 101]---> Sorter-cost: 606 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> Sorter-cost: 552 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 97]---> BDD-cost: 128 c ---[ 95]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 93]---> BDD-cost: 133 c ---[ 91]---> Sorter-cost: 558 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 89]---> Sorter-cost: 530 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 87]---> BDD-cost: 131 c ---[ 85]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 83]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 81]---> BDD-cost: 128 c ---[ 79]---> Sorter-cost: 549 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 77]---> Sorter-cost: 523 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 75]---> BDD-cost: 126 c ---[ 73]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 71]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 69]---> BDD-cost: 119 c ---[ 67]---> Sorter-cost: 509 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 65]---> Sorter-cost: 485 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> BDD-cost: 122 c ---[ 61]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 1032 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 385 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 622 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 566 Base: 2 2 2 2
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/27746/stat): 27746 (minisat+_script) R 27745 27746 15400 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785942237 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/27746/statm): 174 3 169 147 0 27 0 [pid=27746] 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=27747 New process pid=27748 New process pid=27749 execve syscall for /bin/sed executable One traced child (pid=27748) 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=27749) exited with status: 0 One traced child (pid=27747) exited with status: 0 New process pid=27750 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-recipe.opb One traced child (pid=27750) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=27751 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-recipe.opb [startup+10.0032 s] Raw data (loadavg): 0.89 0.95 0.90 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 680 0 0 0 968 3 0 0 25 0 1 0 1785942260 3117056 666 4294967295 134512640 135167914 3221224448 3221221024 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 761 666 162 162 0 599 0 [pid=27751] vsize: 3044 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 5172 [startup+20.0038 s] Raw data (loadavg): 0.91 0.95 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 680 0 0 0 1968 3 0 0 25 0 1 0 1785942260 3117056 666 4294967295 134512640 135167914 3221224448 3221221388 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 761 666 162 162 0 599 0 [pid=27751] vsize: 3044 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 5172 [startup+30.0054 s] Raw data (loadavg): 0.92 0.95 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 939 0 0 0 2967 4 0 0 25 0 1 0 1785942260 4120576 880 4294967295 134512640 135167914 3221224448 3221221052 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1006 880 162 162 0 844 0 [pid=27751] vsize: 4024 Current children cumulated CPU time (s) 29.87 Current children cumulated vsize (Kb) 6152 [startup+40.0061 s] Raw data (loadavg): 0.93 0.95 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 964 0 0 0 3966 5 0 0 25 0 1 0 1785942260 4091904 873 4294967295 134512640 135167914 3221224448 3221220368 134845937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 999 873 162 162 0 837 0 [pid=27751] vsize: 3996 Current children cumulated CPU time (s) 39.87 Current children cumulated vsize (Kb) 6124 [startup+50.0077 s] Raw data (loadavg): 0.94 0.95 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1255 0 0 0 4964 6 0 0 25 0 1 0 1785942260 5308416 1122 4294967295 134512640 135167914 3221224448 3221219432 134718503 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1296 1122 162 162 0 1134 0 [pid=27751] vsize: 5184 Current children cumulated CPU time (s) 49.86 Current children cumulated vsize (Kb) 7312 [startup+60.0083 s] Raw data (loadavg): 0.95 0.95 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1255 0 0 0 5964 6 0 0 25 0 1 0 1785942260 5308416 1122 4294967295 134512640 135167914 3221224448 3221219616 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1296 1122 162 162 0 1134 0 [pid=27751] vsize: 5184 Current children cumulated CPU time (s) 59.86 Current children cumulated vsize (Kb) 7312 [startup+70.009 s] Raw data (loadavg): 0.96 0.95 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1255 0 0 0 6965 6 0 0 25 0 1 0 1785942260 5308416 1122 4294967295 134512640 135167914 3221224448 3221219504 134694489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1296 1122 162 162 0 1134 0 [pid=27751] vsize: 5184 Current children cumulated CPU time (s) 69.87 Current children cumulated vsize (Kb) 7312 [startup+80.0096 s] Raw data (loadavg): 0.96 0.95 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1255 0 0 0 7965 6 0 0 25 0 1 0 1785942260 5308416 1122 4294967295 134512640 135167914 3221224448 3221221200 134843107 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1296 1122 162 162 0 1134 0 [pid=27751] vsize: 5184 Current children cumulated CPU time (s) 79.87 Current children cumulated vsize (Kb) 7312 [startup+90.0102 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1255 0 0 0 8965 6 0 0 25 0 1 0 1785942260 5308416 1122 4294967295 134512640 135167914 3221224448 3221220864 134696581 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1296 1122 162 162 0 1134 0 [pid=27751] vsize: 5184 Current children cumulated CPU time (s) 89.87 Current children cumulated vsize (Kb) 7312 [startup+100.011 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1255 0 0 0 9965 6 0 0 25 0 1 0 1785942260 5308416 1122 4294967295 134512640 135167914 3221224448 3221221452 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1296 1122 162 162 0 1134 0 [pid=27751] vsize: 5184 Current children cumulated CPU time (s) 99.87 Current children cumulated vsize (Kb) 7312 [startup+110.011 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1255 0 0 0 10966 6 0 0 25 0 1 0 1785942260 5308416 1122 4294967295 134512640 135167914 3221224448 3221221296 134629270 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1296 1122 162 162 0 1134 0 [pid=27751] vsize: 5184 Current children cumulated CPU time (s) 109.88 Current children cumulated vsize (Kb) 7312 [startup+120.012 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1255 0 0 0 11966 6 0 0 25 0 1 0 1785942260 5308416 1122 4294967295 134512640 135167914 3221224448 3221222672 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1296 1122 162 162 0 1134 0 [pid=27751] vsize: 5184 Current children cumulated CPU time (s) 119.88 Current children cumulated vsize (Kb) 7312 [startup+130.013 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1616 0 0 0 12964 7 0 0 25 0 1 0 1785942260 5976064 1358 4294967295 134512640 135167914 3221224448 3221219324 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1459 1358 162 162 0 1297 0 [pid=27751] vsize: 5836 Current children cumulated CPU time (s) 129.87 Current children cumulated vsize (Kb) 7964 [startup+140.012 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1616 0 0 0 13964 7 0 0 25 0 1 0 1785942260 5976064 1358 4294967295 134512640 135167914 3221224448 3221220304 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1459 1358 162 162 0 1297 0 [pid=27751] vsize: 5836 Current children cumulated CPU time (s) 139.87 Current children cumulated vsize (Kb) 7964 [startup+150.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1616 0 0 0 14965 7 0 0 25 0 1 0 1785942260 5976064 1358 4294967295 134512640 135167914 3221224448 3221220520 134843032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1459 1358 162 162 0 1297 0 [pid=27751] vsize: 5836 Current children cumulated CPU time (s) 149.88 Current children cumulated vsize (Kb) 7964 [startup+160.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1616 0 0 0 15965 7 0 0 25 0 1 0 1785942260 5976064 1358 4294967295 134512640 135167914 3221224448 3221220960 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1459 1358 162 162 0 1297 0 [pid=27751] vsize: 5836 Current children cumulated CPU time (s) 159.88 Current children cumulated vsize (Kb) 7964 [startup+170.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1616 0 0 0 16965 7 0 0 25 0 1 0 1785942260 5976064 1358 4294967295 134512640 135167914 3221224448 3221221408 134720495 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1459 1358 162 162 0 1297 0 [pid=27751] vsize: 5836 Current children cumulated CPU time (s) 169.88 Current children cumulated vsize (Kb) 7964 [startup+180.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1616 0 0 0 17965 7 0 0 25 0 1 0 1785942260 5976064 1358 4294967295 134512640 135167914 3221224448 3221221728 134843402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1459 1358 162 162 0 1297 0 [pid=27751] vsize: 5836 Current children cumulated CPU time (s) 179.88 Current children cumulated vsize (Kb) 7964 [startup+190.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1616 0 0 0 18965 7 0 0 25 0 1 0 1785942260 5976064 1358 4294967295 134512640 135167914 3221224448 3221221792 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1459 1358 162 162 0 1297 0 [pid=27751] vsize: 5836 Current children cumulated CPU time (s) 189.88 Current children cumulated vsize (Kb) 7964 [startup+200.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1683 0 0 0 19965 7 0 0 25 0 1 0 1785942260 6041600 1383 4294967295 134512640 135167914 3221224448 3221218956 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1475 1383 162 162 0 1313 0 [pid=27751] vsize: 5900 Current children cumulated CPU time (s) 199.88 Current children cumulated vsize (Kb) 8028 [startup+210.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1683 0 0 0 20965 7 0 0 25 0 1 0 1785942260 6041600 1383 4294967295 134512640 135167914 3221224448 3221219432 134718503 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1475 1383 162 162 0 1313 0 [pid=27751] vsize: 5900 Current children cumulated CPU time (s) 209.88 Current children cumulated vsize (Kb) 8028 [startup+220.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1683 0 0 0 21965 7 0 0 25 0 1 0 1785942260 6041600 1383 4294967295 134512640 135167914 3221224448 3221220240 134629224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1475 1383 162 162 0 1313 0 [pid=27751] vsize: 5900 Current children cumulated CPU time (s) 219.88 Current children cumulated vsize (Kb) 8028 [startup+230.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1683 0 0 0 22966 7 0 0 25 0 1 0 1785942260 6041600 1383 4294967295 134512640 135167914 3221224448 3221219968 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1475 1383 162 162 0 1313 0 [pid=27751] vsize: 5900 Current children cumulated CPU time (s) 229.89 Current children cumulated vsize (Kb) 8028 [startup+240.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1683 0 0 0 23966 7 0 0 25 0 1 0 1785942260 6041600 1383 4294967295 134512640 135167914 3221224448 3221220928 134849122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1475 1383 162 162 0 1313 0 [pid=27751] vsize: 5900 Current children cumulated CPU time (s) 239.89 Current children cumulated vsize (Kb) 8028 [startup+250.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1683 0 0 0 24966 7 0 0 25 0 1 0 1785942260 6041600 1383 4294967295 134512640 135167914 3221224448 3221221284 134843000 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1475 1383 162 162 0 1313 0 [pid=27751] vsize: 5900 Current children cumulated CPU time (s) 249.89 Current children cumulated vsize (Kb) 8028 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1683 0 0 0 25967 7 0 0 25 0 1 0 1785942260 6041600 1383 4294967295 134512640 135167914 3221224448 3221220768 134629236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1475 1383 162 162 0 1313 0 [pid=27751] vsize: 5900 Current children cumulated CPU time (s) 259.9 Current children cumulated vsize (Kb) 8028 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1683 0 0 0 26967 7 0 0 25 0 1 0 1785942260 6041600 1383 4294967295 134512640 135167914 3221224448 3221222460 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1475 1383 162 162 0 1313 0 [pid=27751] vsize: 5900 Current children cumulated CPU time (s) 269.9 Current children cumulated vsize (Kb) 8028 [startup+280.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1704 0 0 0 27967 7 0 0 25 0 1 0 1785942260 6090752 1404 4294967295 134512640 135167914 3221224448 3221222064 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1487 1404 162 162 0 1325 0 [pid=27751] vsize: 5948 Current children cumulated CPU time (s) 279.9 Current children cumulated vsize (Kb) 8076 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1704 0 0 0 28967 7 0 0 25 0 1 0 1785942260 6090752 1404 4294967295 134512640 135167914 3221224448 3221221024 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1487 1404 162 162 0 1325 0 [pid=27751] vsize: 5948 Current children cumulated CPU time (s) 289.9 Current children cumulated vsize (Kb) 8076 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 29967 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221218208 134844720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 299.91 Current children cumulated vsize (Kb) 8088 [startup+310.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 30967 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221218800 134849148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 309.91 Current children cumulated vsize (Kb) 8088 [startup+320.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 31967 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219504 134694386 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 319.91 Current children cumulated vsize (Kb) 8088 [startup+330.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 32967 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219168 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 329.91 Current children cumulated vsize (Kb) 8088 [startup+340.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 33968 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221218608 134522816 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 339.92 Current children cumulated vsize (Kb) 8088 [startup+350.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 34968 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220096 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 349.92 Current children cumulated vsize (Kb) 8088 [startup+360.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 35968 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219840 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 359.92 Current children cumulated vsize (Kb) 8088 [startup+370.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 36968 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219624 134693609 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 369.92 Current children cumulated vsize (Kb) 8088 [startup+380.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 37969 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220724 134849147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 379.93 Current children cumulated vsize (Kb) 8088 [startup+390.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 38969 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221218752 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 389.93 Current children cumulated vsize (Kb) 8088 [startup+400.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 39969 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220760 134693783 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 399.93 Current children cumulated vsize (Kb) 8088 [startup+410.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 40969 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219904 134629328 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 409.93 Current children cumulated vsize (Kb) 8088 [startup+420.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 41970 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220320 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 419.94 Current children cumulated vsize (Kb) 8088 [startup+430.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 42970 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219152 134843107 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 429.94 Current children cumulated vsize (Kb) 8088 [startup+440.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 43970 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220336 134843406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 439.94 Current children cumulated vsize (Kb) 8088 [startup+450.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 44970 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220960 134629183 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 449.94 Current children cumulated vsize (Kb) 8088 [startup+460.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 45971 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219348 134849086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 459.95 Current children cumulated vsize (Kb) 8088 [startup+470.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 46971 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220064 134629345 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 469.95 Current children cumulated vsize (Kb) 8088 [startup+480.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 47971 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221221112 134693744 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 479.95 Current children cumulated vsize (Kb) 8088 [startup+490.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 48971 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219328 134694495 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 489.95 Current children cumulated vsize (Kb) 8088 [startup+500.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 49972 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219504 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 499.96 Current children cumulated vsize (Kb) 8088 [startup+510.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 50972 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220880 134844672 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 509.96 Current children cumulated vsize (Kb) 8088 [startup+520.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 51972 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220544 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 519.96 Current children cumulated vsize (Kb) 8088 [startup+530.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 52972 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220560 134843139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 529.96 Current children cumulated vsize (Kb) 8088 [startup+540.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 53972 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221221080 134695249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 539.96 Current children cumulated vsize (Kb) 8088 [startup+550.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 54973 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221221280 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 549.97 Current children cumulated vsize (Kb) 8088 [startup+560.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 55973 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221218576 134696219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 559.97 Current children cumulated vsize (Kb) 8088 [startup+570.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 56973 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219856 134843012 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 569.97 Current children cumulated vsize (Kb) 8088 [startup+580.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 57974 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220576 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 579.98 Current children cumulated vsize (Kb) 8088 [startup+590.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 58974 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220848 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 589.98 Current children cumulated vsize (Kb) 8088 [startup+600.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 59974 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221221728 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 599.98 Current children cumulated vsize (Kb) 8088 [startup+610.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 60974 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219568 134844720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 609.98 Current children cumulated vsize (Kb) 8088 [startup+620.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 61975 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220672 134696674 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 619.99 Current children cumulated vsize (Kb) 8088 [startup+630.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 62975 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221221364 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 629.99 Current children cumulated vsize (Kb) 8088 [startup+640.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 63975 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221221376 134844725 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 639.99 Current children cumulated vsize (Kb) 8088 [startup+650.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 64975 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221219664 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 649.99 Current children cumulated vsize (Kb) 8088 [startup+660.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 65976 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220172 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 660 Current children cumulated vsize (Kb) 8088 [startup+670.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 66976 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220908 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 670 Current children cumulated vsize (Kb) 8088 [startup+680.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 67976 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221220380 134845940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 680 Current children cumulated vsize (Kb) 8088 [startup+690.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 1821 0 0 0 68976 8 0 0 25 0 1 0 1785942260 6103040 1407 4294967295 134512640 135167914 3221224448 3221221552 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1490 1407 162 162 0 1328 0 [pid=27751] vsize: 5960 Current children cumulated CPU time (s) 690 Current children cumulated vsize (Kb) 8088 [startup+700.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 69975 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221218608 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 699.99 Current children cumulated vsize (Kb) 9496 [startup+710.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 70975 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219168 134849066 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 709.99 Current children cumulated vsize (Kb) 9496 [startup+720.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 71976 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219668 134849147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 720 Current children cumulated vsize (Kb) 9496 [startup+730.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 72976 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221218192 134718181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 730 Current children cumulated vsize (Kb) 9496 [startup+740.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 73976 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219168 134694338 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 740 Current children cumulated vsize (Kb) 9496 [startup+750.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 74977 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220012 134845940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 750.01 Current children cumulated vsize (Kb) 9496 [startup+760.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 75977 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219296 134720464 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 760.01 Current children cumulated vsize (Kb) 9496 [startup+770.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 76977 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219568 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 770.01 Current children cumulated vsize (Kb) 9496 [startup+780.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 77977 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220708 134845938 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 780.01 Current children cumulated vsize (Kb) 9496 [startup+790.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 78977 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219504 134522296 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 790.01 Current children cumulated vsize (Kb) 9496 [startup+800.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 79977 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221221088 134694539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 800.01 Current children cumulated vsize (Kb) 9496 [startup+810.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 80978 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219692 134722660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 810.02 Current children cumulated vsize (Kb) 9496 [startup+820.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 81978 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220396 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 820.02 Current children cumulated vsize (Kb) 9496 [startup+830.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 82978 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219504 134694539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 830.02 Current children cumulated vsize (Kb) 9496 [startup+840.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 83978 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220144 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 840.02 Current children cumulated vsize (Kb) 9496 [startup+850.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 84979 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220640 134844672 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 850.03 Current children cumulated vsize (Kb) 9496 [startup+860.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 85979 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219536 134629045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 860.03 Current children cumulated vsize (Kb) 9496 [startup+870.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 86979 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220364 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 870.03 Current children cumulated vsize (Kb) 9496 [startup+880.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 87979 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220848 134843130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 880.03 Current children cumulated vsize (Kb) 9496 [startup+890.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 88980 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219672 134845877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 890.04 Current children cumulated vsize (Kb) 9496 [startup+900.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 89980 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219808 134696248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 900.04 Current children cumulated vsize (Kb) 9496 [startup+910.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 90980 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 910.04 Current children cumulated vsize (Kb) 9496 [startup+920.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 91980 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220144 134844745 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 920.04 Current children cumulated vsize (Kb) 9496 [startup+930.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 92981 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220224 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 930.05 Current children cumulated vsize (Kb) 9496 [startup+940.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 93981 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221221228 134845882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 940.05 Current children cumulated vsize (Kb) 9496 [startup+950.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 94981 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221221468 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 950.05 Current children cumulated vsize (Kb) 9496 [startup+960.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 95981 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221218988 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 960.05 Current children cumulated vsize (Kb) 9496 [startup+970.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 96981 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219904 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 970.05 Current children cumulated vsize (Kb) 9496 [startup+980.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 97982 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220256 134630803 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 980.06 Current children cumulated vsize (Kb) 9496 [startup+990.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 98982 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220716 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 990.06 Current children cumulated vsize (Kb) 9496 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 99982 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221221616 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1000.06 Current children cumulated vsize (Kb) 9496 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 100982 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221218992 134849179 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1010.06 Current children cumulated vsize (Kb) 9496 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 101982 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220944 134629148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1020.06 Current children cumulated vsize (Kb) 9496 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 102983 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221221456 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1030.07 Current children cumulated vsize (Kb) 9496 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 103983 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221221568 134696248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1040.07 Current children cumulated vsize (Kb) 9496 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 104983 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221219328 134843404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1050.07 Current children cumulated vsize (Kb) 9496 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 105983 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220236 134693552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1060.07 Current children cumulated vsize (Kb) 9496 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 106984 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221220720 134522821 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1070.08 Current children cumulated vsize (Kb) 9496 [startup+1080.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 107984 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221222080 134843420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1080.08 Current children cumulated vsize (Kb) 9496 [startup+1090.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2075 0 0 0 108984 8 0 0 25 0 1 0 1785942260 7544832 1619 4294967295 134512640 135167914 3221224448 3221221580 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 1842 1619 162 162 0 1680 0 [pid=27751] vsize: 7368 Current children cumulated CPU time (s) 1090.08 Current children cumulated vsize (Kb) 9496 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 109983 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221219328 134522310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1100.08 Current children cumulated vsize (Kb) 10232 [startup+1110.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 110983 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221218192 134843118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1110.08 Current children cumulated vsize (Kb) 10232 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 111984 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221219628 134723265 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1120.09 Current children cumulated vsize (Kb) 10232 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 112984 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221218620 134695248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1130.09 Current children cumulated vsize (Kb) 10232 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 113984 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221218736 134696321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1140.09 Current children cumulated vsize (Kb) 10232 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 114984 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221220032 134843402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1150.09 Current children cumulated vsize (Kb) 10232 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 115985 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221219504 134694398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1160.1 Current children cumulated vsize (Kb) 10232 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 116985 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221219328 134694528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1170.1 Current children cumulated vsize (Kb) 10232 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 117985 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221220236 134693552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1180.1 Current children cumulated vsize (Kb) 10232 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 118985 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221220096 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1190.1 Current children cumulated vsize (Kb) 10232 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 119985 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221220384 134522315 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1200.1 Current children cumulated vsize (Kb) 10232 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27751 Raw data (/proc/27746/stat): 27746 (minisat+_script) S 27745 27746 15400 0 -1 0 314 659 0 0 0 1 12 3 17 0 1 0 1785942237 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27746/statm): 532 234 485 147 0 385 0 [pid=27746] vsize: 2128 Raw data (/proc/27751/stat): 27751 (minisat+_bignum) R 27746 27746 15400 0 -1 0 2477 0 0 0 119986 9 0 0 25 0 1 0 1785942260 8298496 1814 4294967295 134512640 135167914 3221224448 3221220364 134693585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27751/statm): 2026 1814 162 162 0 1864 0 [pid=27751] vsize: 8104 Current children cumulated CPU time (s) 1200.11 Current children cumulated vsize (Kb) 10232 Sending SIGTERM to -27746 Sleeping 2 seconds One traced child (pid=27746) ended because it received signal 15 (SIGTERM) One traced child (pid=27751) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1200.08 CPU time (s): 1199.96 CPU user time (s): 1199.86 CPU system time (s): 0.102984 CPU usage (%): 99.9901 Max. virtual memory (cumulated for all children) (Kb): 10232
ERROR: no interpretation found !