Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-vtp.base.opb |
MD5SUM | 62492fa5ef4f36caec6c1eec4eeb566a |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 181 |
Biggest coefficient in the objective function | 1073741824 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 7516192762 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 198568686125056 |
Number of bits of the biggest number in a constraint | 48 |
Biggest sum of numbers in a constraint | 12817928787879752 |
Number of bits of the biggest sum of numbers | 54 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 4524 |
Total number of constraints | 262 |
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 | 262 |
Minimum length of a constraint | 11 |
Maximum length of a constraint | 1080 |
LAUNCH ON wulflinc24 THE 2005-09-18 20:38:24 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2827 boxname=wulflinc24 idbench=483 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 62492fa5ef4f36caec6c1eec4eeb566a /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-vtp.base.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-vtp.base.opb IDLAUNCH: 2827 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 911216 kB Buffers: 35168 kB Cached: 60376 kB SwapCached: 744 kB Active: 67932 kB Inactive: 30204 kB HighTotal: 131008 kB HighFree: 67508 kB LowTotal: 903652 kB LowFree: 843708 kB SwapTotal: 2097892 kB SwapFree: 2096644 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5736 kB Slab: 19612 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:50:46 (client local time) WITH STATUS 0 IN 729.671 SECONDS stats: 2827 7 729.671 0
c Parsing PB file... c PARSE ERROR! [line 305] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 261 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################################ c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssss c ---[ 286]---> BDD-cost: 18 c ---[ 285]---> BDD-cost: 16 c ---[ 284]---> BDD-cost: 16 c ---[ 283]---> BDD-cost: 16 c ---[ 282]---> BDD-cost: 18 c ---[ 281]---> BDD-cost: 16 c ---[ 280]---> BDD-cost: 16 c ---[ 279]---> BDD-cost: 16 c ---[ 278]---> BDD-cost: 18 c ---[ 277]---> BDD-cost: 16 c ---[ 276]---> BDD-cost: 16 c ---[ 275]---> BDD-cost: 16 c ---[ 274]---> BDD-cost: 18 c ---[ 273]---> BDD-cost: 16 c ---[ 272]---> BDD-cost: 16 c ---[ 271]---> BDD-cost: 16 c ---[ 270]---> BDD-cost: 18 c ---[ 269]---> BDD-cost: 16 c ---[ 268]---> BDD-cost: 16 c ---[ 267]---> BDD-cost: 16 c ---[ 266]---> BDD-cost: 18 c ---[ 265]---> BDD-cost: 16 c ---[ 264]---> BDD-cost: 16 c ---[ 263]---> BDD-cost: 16 c ---[ 262]---> BDD-cost: 18 c ---[ 261]---> BDD-cost: 16 c ---[ 260]---> BDD-cost: 16 c ---[ 259]---> BDD-cost: 16 c ---[ 258]---> BDD-cost: 18 c ---[ 257]---> BDD-cost: 16 c ---[ 256]---> BDD-cost: 16 c ---[ 255]---> BDD-cost: 16 c ---[ 221]---> Sorter-cost: 699 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 219]---> Sorter-cost: 2344 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 217]---> Sorter-cost: 2370 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 215]---> Sorter-cost: 3598 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 213]---> Sorter-cost: 2363 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 211]---> Sorter-cost: 2378 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 c ---[ 209]---> Sorter-cost: 2440 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 ---[ 207]---> Sorter-cost: 1691 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 c ---[ 205]---> Sorter-cost: 1041 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 203]---> Adder-cost: 475 maxlim: 8105876 bits: 24/23 c ---[ 201]---> Sorter-cost: 3427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> Sorter-cost: 3442 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 197]---> Sorter-cost: 3457 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 c ---[ 195]---> Adder-cost: 502 maxlim: 75018132 bits: 28/27 c ---[ 193]---> Sorter-cost: 3571 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 c ---[ 191]---> Sorter-cost: 1997 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 ---[ 189]---> Sorter-cost: 1663 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 187]---> Sorter-cost: 3364 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 185]---> Sorter-cost: 3324 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 183]---> Sorter-cost: 3339 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 c ---[ 181]---> Adder-cost: 410 maxlim: 74725284 bits: 28/27 c ---[ 179]---> Sorter-cost: 3447 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 c ---[ 177]---> Adder-cost: 420 maxlim: 275744676 bits: 30/29 c ---[ 175]---> Sorter-cost: 1977 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 ---[ 173]---> Sorter-cost: 605 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 2111 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 169]---> Adder-cost: 388 maxlim: 9779094 bits: 25/24 c ---[ 167]---> Sorter-cost: 2171 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 165]---> Sorter-cost: 2186 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 c ---[ 163]---> Sorter-cost: 2207 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 ---[ 161]---> Sorter-cost: 2252 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 c ---[ 159]---> Sorter-cost: 1601 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 ---[ 147]---> c *
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/27508/stat): 27508 (minisat+_script) R 27507 27508 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844196815 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/27508/statm): 174 3 169 147 0 27 0 [pid=27508] 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=27509 New process pid=27510 New process pid=27511 execve syscall for /bin/sed executable One traced child (pid=27510) 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=27511) exited with status: 0 One traced child (pid=27509) exited with status: 0 New process pid=27512 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-vtp.base.opb One traced child (pid=27512) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=27513 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-vtp.base.opb [startup+10.004 s] Raw data (loadavg): 0.84 0.90 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 1568 0 0 0 972 5 0 0 25 0 1 0 1844196832 6123520 1357 4294967295 134512640 135167914 3221224448 3221221440 134843420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 1495 1357 162 162 0 1333 0 [pid=27513] vsize: 5980 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 8108 [startup+20.0048 s] Raw data (loadavg): 0.86 0.90 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 6295 0 0 0 1928 26 0 0 25 0 1 0 1844196832 23650304 5464 4294967295 134512640 135167914 3221224448 3221041212 134934490 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 5774 5464 162 162 0 5612 0 [pid=27513] vsize: 23096 Current children cumulated CPU time (s) 19.66 Current children cumulated vsize (Kb) 25224 [startup+30.0054 s] Raw data (loadavg): 0.88 0.91 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 11234 0 0 0 2885 47 0 0 25 0 1 0 1844196832 41181184 9744 4294967295 134512640 135167914 3221224448 3221039808 134847261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 10054 9744 162 162 0 9892 0 [pid=27513] vsize: 40216 Current children cumulated CPU time (s) 29.44 Current children cumulated vsize (Kb) 42344 [startup+40.0051 s] Raw data (loadavg): 0.90 0.91 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 17146 0 0 0 3839 71 0 0 25 0 1 0 1844196832 59998208 14338 4294967295 134512640 135167914 3221224448 3221051144 134693650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 14648 14338 162 162 0 14486 0 [pid=27513] vsize: 58592 Current children cumulated CPU time (s) 39.22 Current children cumulated vsize (Kb) 60720 [startup+50.0068 s] Raw data (loadavg): 0.91 0.91 0.91 1/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 20571 0 0 0 4798 88 0 0 25 0 1 0 1844196832 74027008 17763 4294967295 134512640 135167914 3221224448 3221045372 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 18073 17763 162 162 0 17911 0 [pid=27513] vsize: 72292 Current children cumulated CPU time (s) 48.98 Current children cumulated vsize (Kb) 74420 [startup+60.0075 s] Raw data (loadavg): 0.93 0.91 0.91 1/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 28514 0 0 0 5754 115 0 0 25 0 1 0 1844196832 95760384 23069 4294967295 134512640 135167914 3221224448 3221060844 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 23379 23069 162 162 0 23217 0 [pid=27513] vsize: 93516 Current children cumulated CPU time (s) 58.81 Current children cumulated vsize (Kb) 95644 [startup+70.0082 s] Raw data (loadavg): 0.94 0.92 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 31801 0 0 0 6716 130 0 0 25 0 1 0 1844196832 109223936 26356 4294967295 134512640 135167914 3221224448 3221039872 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 26666 26356 162 162 0 26504 0 [pid=27513] vsize: 106664 Current children cumulated CPU time (s) 68.58 Current children cumulated vsize (Kb) 108792 [startup+80.0089 s] Raw data (loadavg): 0.95 0.92 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 35064 0 0 0 7680 145 0 0 25 0 1 0 1844196832 122589184 29619 4294967295 134512640 135167914 3221224448 3221039872 134722532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 29929 29619 162 162 0 29767 0 [pid=27513] vsize: 119716 Current children cumulated CPU time (s) 78.37 Current children cumulated vsize (Kb) 121844 [startup+90.0086 s] Raw data (loadavg): 0.95 0.92 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 38178 0 0 0 8645 161 0 0 25 0 1 0 1844196832 135344128 32733 4294967295 134512640 135167914 3221224448 3221076872 134846971 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 33043 32733 162 162 0 32881 0 [pid=27513] vsize: 132172 Current children cumulated CPU time (s) 88.18 Current children cumulated vsize (Kb) 134300 [startup+100.009 s] Raw data (loadavg): 0.96 0.92 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 41217 0 0 0 9612 176 0 0 25 0 1 0 1844196832 147791872 35772 4294967295 134512640 135167914 3221224448 3221054592 134847211 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 36082 35772 162 162 0 35920 0 [pid=27513] vsize: 144328 Current children cumulated CPU time (s) 98 Current children cumulated vsize (Kb) 146456 [startup+110.01 s] Raw data (loadavg): 0.97 0.92 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 54527 0 0 0 10558 212 0 0 25 0 1 0 1844196832 202309632 49082 4294967295 134512640 135167914 3221224448 3221052752 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 49392 49082 162 162 0 49230 0 [pid=27513] vsize: 197568 Current children cumulated CPU time (s) 107.82 Current children cumulated vsize (Kb) 199696 [startup+120.011 s] Raw data (loadavg): 0.97 0.93 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 56366 0 0 0 11536 222 0 0 25 0 1 0 1844196832 188243968 45648 4294967295 134512640 135167914 3221224448 3221041996 134844675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 45958 45648 162 162 0 45796 0 [pid=27513] vsize: 183832 Current children cumulated CPU time (s) 117.7 Current children cumulated vsize (Kb) 185960 [startup+130.011 s] Raw data (loadavg): 0.98 0.93 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 59575 0 0 0 12501 236 0 0 25 0 1 0 1844196832 201388032 48857 4294967295 134512640 135167914 3221224448 3221040796 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 49167 48857 162 162 0 49005 0 [pid=27513] vsize: 196668 Current children cumulated CPU time (s) 127.49 Current children cumulated vsize (Kb) 198796 [startup+140.012 s] Raw data (loadavg): 0.98 0.93 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 62407 0 0 0 13471 249 0 0 25 0 1 0 1844196832 212987904 51689 4294967295 134512640 135167914 3221224448 3221048032 134695583 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 51999 51689 162 162 0 51837 0 [pid=27513] vsize: 207996 Current children cumulated CPU time (s) 137.32 Current children cumulated vsize (Kb) 210124 [startup+150.014 s] Raw data (loadavg): 0.98 0.93 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 65465 0 0 0 14437 263 0 0 25 0 1 0 1844196832 225513472 54747 4294967295 134512640 135167914 3221224448 3221040224 134844676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 55057 54747 162 162 0 54895 0 [pid=27513] vsize: 220228 Current children cumulated CPU time (s) 147.12 Current children cumulated vsize (Kb) 222356 [startup+160.015 s] Raw data (loadavg): 0.98 0.93 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 68243 0 0 0 15406 277 0 0 25 0 1 0 1844196832 236892160 57525 4294967295 134512640 135167914 3221224448 3221038560 134843153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 57835 57525 162 162 0 57673 0 [pid=27513] vsize: 231340 Current children cumulated CPU time (s) 156.95 Current children cumulated vsize (Kb) 233468 [startup+170.015 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 71147 0 0 0 16372 291 0 0 25 0 1 0 1844196832 248786944 60429 4294967295 134512640 135167914 3221224448 3221045296 134693566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 60739 60429 162 162 0 60577 0 [pid=27513] vsize: 242956 Current children cumulated CPU time (s) 166.75 Current children cumulated vsize (Kb) 245084 [startup+180.016 s] Raw data (loadavg): 0.99 0.94 0.91 1/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 73919 0 0 0 17342 303 0 0 25 0 1 0 1844196832 260141056 63201 4294967295 134512640 135167914 3221224448 3221037996 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 63511 63201 162 162 0 63349 0 [pid=27513] vsize: 254044 Current children cumulated CPU time (s) 176.57 Current children cumulated vsize (Kb) 256172 [startup+190.017 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 76614 0 0 0 18312 316 0 0 25 0 1 0 1844196832 271179776 65896 4294967295 134512640 135167914 3221224448 3221040352 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 66206 65896 162 162 0 66044 0 [pid=27513] vsize: 264824 Current children cumulated CPU time (s) 186.4 Current children cumulated vsize (Kb) 266952 [startup+200.017 s] Raw data (loadavg): 0.99 0.94 0.91 1/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 79462 0 0 0 19284 327 0 0 25 0 1 0 1844196832 282845184 68744 4294967295 134512640 135167914 3221224448 3221036700 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 69054 68744 162 162 0 68892 0 [pid=27513] vsize: 276216 Current children cumulated CPU time (s) 196.23 Current children cumulated vsize (Kb) 278344 [startup+210.018 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 82152 0 0 0 20256 339 0 0 25 0 1 0 1844196832 293863424 71434 4294967295 134512640 135167914 3221224448 3221048228 134624790 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 71744 71434 162 162 0 71582 0 [pid=27513] vsize: 286976 Current children cumulated CPU time (s) 206.07 Current children cumulated vsize (Kb) 289104 [startup+220.019 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 84808 0 0 0 21224 353 0 0 25 0 1 0 1844196832 304742400 74090 4294967295 134512640 135167914 3221224448 3221041312 134695622 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 74400 74090 162 162 0 74238 0 [pid=27513] vsize: 297600 Current children cumulated CPU time (s) 215.89 Current children cumulated vsize (Kb) 299728 [startup+230.019 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 107412 0 0 0 22160 409 0 0 25 0 1 0 1844196832 397328384 96694 4294967295 134512640 135167914 3221224448 3221057056 134625423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 97004 96694 162 162 0 96842 0 [pid=27513] vsize: 388016 Current children cumulated CPU time (s) 225.81 Current children cumulated vsize (Kb) 390144 [startup+240.02 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 108926 0 0 0 23141 419 0 0 25 0 1 0 1844196832 360333312 87662 4294967295 134512640 135167914 3221224448 3221056544 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 87972 87662 162 162 0 87810 0 [pid=27513] vsize: 351888 Current children cumulated CPU time (s) 235.72 Current children cumulated vsize (Kb) 354016 [startup+250.021 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 111573 0 0 0 24110 432 0 0 25 0 1 0 1844196832 371175424 90309 4294967295 134512640 135167914 3221224448 3221043712 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 90619 90309 162 162 0 90457 0 [pid=27513] vsize: 362476 Current children cumulated CPU time (s) 245.54 Current children cumulated vsize (Kb) 364604 [startup+260.021 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 114219 0 0 0 25082 444 0 0 25 0 1 0 1844196832 382013440 92955 4294967295 134512640 135167914 3221224448 3221055600 134516629 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 93265 92955 162 162 0 93103 0 [pid=27513] vsize: 373060 Current children cumulated CPU time (s) 255.38 Current children cumulated vsize (Kb) 375188 [startup+270.022 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 116792 0 0 0 26055 455 0 0 25 0 1 0 1844196832 392552448 95528 4294967295 134512640 135167914 3221224448 3221040464 134849102 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 95838 95528 162 162 0 95676 0 [pid=27513] vsize: 383352 Current children cumulated CPU time (s) 265.22 Current children cumulated vsize (Kb) 385480 [startup+280.023 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 119767 0 0 0 27021 469 0 0 25 0 1 0 1844196832 404738048 98503 4294967295 134512640 135167914 3221224448 3221049308 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 98813 98503 162 162 0 98651 0 [pid=27513] vsize: 395252 Current children cumulated CPU time (s) 275.02 Current children cumulated vsize (Kb) 397380 [startup+290.024 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 122321 0 0 0 27993 480 0 0 25 0 1 0 1844196832 415199232 101057 4294967295 134512640 135167914 3221224448 3221038704 134845913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 101367 101057 162 162 0 101205 0 [pid=27513] vsize: 405468 Current children cumulated CPU time (s) 284.85 Current children cumulated vsize (Kb) 407596 [startup+300.025 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 124896 0 0 0 28966 491 0 0 25 0 1 0 1844196832 425746432 103632 4294967295 134512640 135167914 3221224448 3221042844 134694368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 103942 103632 162 162 0 103780 0 [pid=27513] vsize: 415768 Current children cumulated CPU time (s) 294.69 Current children cumulated vsize (Kb) 417896 [startup+310.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 127400 0 0 0 29938 503 0 0 25 0 1 0 1844196832 436002816 106136 4294967295 134512640 135167914 3221224448 3221038268 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 106446 106136 162 162 0 106284 0 [pid=27513] vsize: 425784 Current children cumulated CPU time (s) 304.53 Current children cumulated vsize (Kb) 427912 [startup+320.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 130317 0 0 0 30906 517 0 0 25 0 1 0 1844196832 447950848 109053 4294967295 134512640 135167914 3221224448 3221047776 134624134 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 109363 109053 162 162 0 109201 0 [pid=27513] vsize: 437452 Current children cumulated CPU time (s) 314.35 Current children cumulated vsize (Kb) 439580 [startup+330.027 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 132800 0 0 0 31877 530 0 0 25 0 1 0 1844196832 458121216 111536 4294967295 134512640 135167914 3221224448 3221037456 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 111846 111536 162 162 0 111684 0 [pid=27513] vsize: 447384 Current children cumulated CPU time (s) 324.19 Current children cumulated vsize (Kb) 449512 [startup+340.028 s] Raw data (loadavg): 0.99 0.96 0.91 1/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 135318 0 0 0 32852 540 0 0 25 0 1 0 1844196832 468434944 114054 4294967295 134512640 135167914 3221224448 3221046332 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 114364 114054 162 162 0 114202 0 [pid=27513] vsize: 457456 Current children cumulated CPU time (s) 334.04 Current children cumulated vsize (Kb) 459584 [startup+350.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 137775 0 0 0 33824 551 0 0 25 0 1 0 1844196832 478498816 116511 4294967295 134512640 135167914 3221224448 3221038112 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 116821 116511 162 162 0 116659 0 [pid=27513] vsize: 467284 Current children cumulated CPU time (s) 343.87 Current children cumulated vsize (Kb) 469412 [startup+360.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 140438 0 0 0 34796 564 0 0 25 0 1 0 1844196832 489406464 119174 4294967295 134512640 135167914 3221224448 3221038332 134722225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 119484 119174 162 162 0 119322 0 [pid=27513] vsize: 477936 Current children cumulated CPU time (s) 353.72 Current children cumulated vsize (Kb) 480064 [startup+370.03 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 142901 0 0 0 35768 576 0 0 25 0 1 0 1844196832 499494912 121637 4294967295 134512640 135167914 3221224448 3221050812 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 121947 121637 162 162 0 121785 0 [pid=27513] vsize: 487788 Current children cumulated CPU time (s) 363.56 Current children cumulated vsize (Kb) 489916 [startup+380.031 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 145426 0 0 0 36742 586 0 0 25 0 1 0 1844196832 509837312 124162 4294967295 134512640 135167914 3221224448 3221042016 134694528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 124472 124162 162 162 0 124310 0 [pid=27513] vsize: 497888 Current children cumulated CPU time (s) 373.4 Current children cumulated vsize (Kb) 500016 [startup+390.032 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 147846 0 0 0 37715 596 0 0 25 0 1 0 1844196832 519749632 126582 4294967295 134512640 135167914 3221224448 3221068360 134846935 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 126892 126582 162 162 0 126730 0 [pid=27513] vsize: 507568 Current children cumulated CPU time (s) 383.23 Current children cumulated vsize (Kb) 509696 [startup+400.033 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 150464 0 0 0 38686 609 0 0 25 0 1 0 1844196832 530472960 129200 4294967295 134512640 135167914 3221224448 3221047328 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 129510 129200 162 162 0 129348 0 [pid=27513] vsize: 518040 Current children cumulated CPU time (s) 393.07 Current children cumulated vsize (Kb) 520168 [startup+410.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 152896 0 0 0 39658 619 0 0 25 0 1 0 1844196832 540434432 131632 4294967295 134512640 135167914 3221224448 3221042464 134843402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 131942 131632 162 162 0 131780 0 [pid=27513] vsize: 527768 Current children cumulated CPU time (s) 402.89 Current children cumulated vsize (Kb) 529896 [startup+420.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 155363 0 0 0 40633 629 0 0 25 0 1 0 1844196832 550539264 134099 4294967295 134512640 135167914 3221224448 3221043264 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 134409 134099 162 162 0 134247 0 [pid=27513] vsize: 537636 Current children cumulated CPU time (s) 412.74 Current children cumulated vsize (Kb) 539764 [startup+430.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 157745 0 0 0 41606 639 0 0 25 0 1 0 1844196832 560295936 136481 4294967295 134512640 135167914 3221224448 3221041744 134624420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 136791 136481 162 162 0 136629 0 [pid=27513] vsize: 547164 Current children cumulated CPU time (s) 422.57 Current children cumulated vsize (Kb) 549292 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 160430 0 0 0 42574 652 0 0 25 0 1 0 1844196832 571293696 139166 4294967295 134512640 135167914 3221224448 3221063472 134623813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 139476 139166 162 162 0 139314 0 [pid=27513] vsize: 557904 Current children cumulated CPU time (s) 432.38 Current children cumulated vsize (Kb) 560032 [startup+450.036 s] Raw data (loadavg): 1.07 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 162947 0 0 0 43544 663 0 0 25 0 1 0 1844196832 581603328 141683 4294967295 134512640 135167914 3221224448 3221056608 134847226 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 141993 141683 162 162 0 141831 0 [pid=27513] vsize: 567972 Current children cumulated CPU time (s) 442.19 Current children cumulated vsize (Kb) 570100 [startup+460.036 s] Raw data (loadavg): 1.06 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 165387 0 0 0 44517 674 0 0 25 0 1 0 1844196832 591597568 144123 4294967295 134512640 135167914 3221224448 3221046880 134843113 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 144433 144123 162 162 0 144271 0 [pid=27513] vsize: 577732 Current children cumulated CPU time (s) 452.03 Current children cumulated vsize (Kb) 579860 [startup+470.037 s] Raw data (loadavg): 1.05 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 167802 0 0 0 45491 685 0 0 25 0 1 0 1844196832 601489408 146538 4294967295 134512640 135167914 3221224448 3221040608 134844703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 146848 146538 162 162 0 146686 0 [pid=27513] vsize: 587392 Current children cumulated CPU time (s) 461.88 Current children cumulated vsize (Kb) 589520 [startup+480.038 s] Raw data (loadavg): 1.04 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 170303 0 0 0 46464 698 0 0 25 0 1 0 1844196832 611733504 149039 4294967295 134512640 135167914 3221224448 3221046400 134694383 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 149349 149039 162 162 0 149187 0 [pid=27513] vsize: 597396 Current children cumulated CPU time (s) 471.74 Current children cumulated vsize (Kb) 599524 [startup+490.038 s] Raw data (loadavg): 1.04 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 213185 0 0 0 47359 798 0 0 25 0 1 0 1844196832 787378176 191921 4294967295 134512640 135167914 3221224448 3221065472 134845881 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 192231 191921 162 162 0 192069 0 [pid=27513] vsize: 768924 Current children cumulated CPU time (s) 481.69 Current children cumulated vsize (Kb) 771052 [startup+500.039 s] Raw data (loadavg): 1.03 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 213185 0 0 0 48359 798 0 0 25 0 1 0 1844196832 787378176 191921 4294967295 134512640 135167914 3221224448 3221065488 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 192231 191921 162 162 0 192069 0 [pid=27513] vsize: 768924 Current children cumulated CPU time (s) 491.69 Current children cumulated vsize (Kb) 771052 [startup+510.04 s] Raw data (loadavg): 1.03 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 215502 0 0 0 49330 815 0 0 25 0 1 0 1844196832 710479872 173147 4294967295 134512640 135167914 3221224448 3221052960 134695981 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 173457 173147 162 162 0 173295 0 [pid=27513] vsize: 693828 Current children cumulated CPU time (s) 501.57 Current children cumulated vsize (Kb) 695956 [startup+520.04 s] Raw data (loadavg): 1.02 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 217918 0 0 0 50301 828 0 0 25 0 1 0 1844196832 720375808 175563 4294967295 134512640 135167914 3221224448 3221040156 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 175873 175563 162 162 0 175711 0 [pid=27513] vsize: 703492 Current children cumulated CPU time (s) 511.41 Current children cumulated vsize (Kb) 705620 [startup+530.041 s] Raw data (loadavg): 1.02 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 220365 0 0 0 51276 838 0 0 25 0 1 0 1844196832 730398720 178010 4294967295 134512640 135167914 3221224448 3221068672 134849187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 178320 178010 162 162 0 178158 0 [pid=27513] vsize: 713280 Current children cumulated CPU time (s) 521.26 Current children cumulated vsize (Kb) 715408 [startup+540.042 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 222797 0 0 0 52250 849 0 0 25 0 1 0 1844196832 740360192 180442 4294967295 134512640 135167914 3221224448 3221054464 134694405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 180752 180442 162 162 0 180590 0 [pid=27513] vsize: 723008 Current children cumulated CPU time (s) 531.11 Current children cumulated vsize (Kb) 725136 [startup+550.043 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 225301 0 0 0 53222 860 0 0 25 0 1 0 1844196832 750616576 182946 4294967295 134512640 135167914 3221224448 3221036316 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 183256 182946 162 162 0 183094 0 [pid=27513] vsize: 733024 Current children cumulated CPU time (s) 540.94 Current children cumulated vsize (Kb) 735152 [startup+560.043 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 227678 0 0 0 54195 871 0 0 25 0 1 0 1844196832 760352768 185323 4294967295 134512640 135167914 3221224448 3221040544 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 185633 185323 162 162 0 185471 0 [pid=27513] vsize: 742532 Current children cumulated CPU time (s) 550.78 Current children cumulated vsize (Kb) 744660 [startup+570.043 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 230076 0 0 0 55171 880 0 0 25 0 1 0 1844196832 770174976 187721 4294967295 134512640 135167914 3221224448 3221071776 134695967 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 188031 187721 162 162 0 187869 0 [pid=27513] vsize: 752124 Current children cumulated CPU time (s) 560.63 Current children cumulated vsize (Kb) 754252 [startup+580.044 s] Raw data (loadavg): 1.01 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 232503 0 0 0 56143 891 0 0 25 0 1 0 1844196832 780115968 190148 4294967295 134512640 135167914 3221224448 3221039456 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 190458 190148 162 162 0 190296 0 [pid=27513] vsize: 761832 Current children cumulated CPU time (s) 570.46 Current children cumulated vsize (Kb) 763960 [startup+590.044 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 234939 0 0 0 57119 900 0 0 25 0 1 0 1844196832 790093824 192584 4294967295 134512640 135167914 3221224448 3221039920 134693561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 192894 192584 162 162 0 192732 0 [pid=27513] vsize: 771576 Current children cumulated CPU time (s) 580.31 Current children cumulated vsize (Kb) 773704 [startup+600.045 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 237324 0 0 0 58092 911 0 0 25 0 1 0 1844196832 799862784 194969 4294967295 134512640 135167914 3221224448 3221048512 134844653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 195279 194969 162 162 0 195117 0 [pid=27513] vsize: 781116 Current children cumulated CPU time (s) 590.15 Current children cumulated vsize (Kb) 783244 [startup+610.046 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 239974 0 0 0 59061 923 0 0 17 0 1 0 1844196832 810717184 197619 4294967295 134512640 135167914 3221224448 3221075180 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 197929 197619 162 162 0 197767 0 [pid=27513] vsize: 791716 Current children cumulated CPU time (s) 599.96 Current children cumulated vsize (Kb) 793844 [startup+620.047 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 242484 0 0 0 60033 935 0 0 25 0 1 0 1844196832 820998144 200129 4294967295 134512640 135167914 3221224448 3221068448 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 200439 200129 162 162 0 200277 0 [pid=27513] vsize: 801756 Current children cumulated CPU time (s) 609.8 Current children cumulated vsize (Kb) 803884 [startup+630.047 s] Raw data (loadavg): 1.00 0.98 0.91 1/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 244852 0 0 0 61008 944 0 0 25 0 1 0 1844196832 830697472 202497 4294967295 134512640 135167914 3221224448 3221060956 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27513/statm): 202807 202497 162 162 0 202645 0 [pid=27513] vsize: 811228 Current children cumulated CPU time (s) 619.64 Current children cumulated vsize (Kb) 813356 [startup+640.048 s] Raw data (loadavg): 1.00 0.98 0.91 1/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 247339 0 0 0 61982 955 0 0 25 0 1 0 1844196832 840884224 204984 4294967295 134512640 135167914 3221224448 3221040124 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 205294 204984 162 162 0 205132 0 [pid=27513] vsize: 821176 Current children cumulated CPU time (s) 629.49 Current children cumulated vsize (Kb) 823304 [startup+650.05 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 249682 0 0 0 62958 965 0 0 25 0 1 0 1844196832 850481152 207327 4294967295 134512640 135167914 3221224448 3221041696 134694377 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 207637 207327 162 162 0 207475 0 [pid=27513] vsize: 830548 Current children cumulated CPU time (s) 639.35 Current children cumulated vsize (Kb) 832676 [startup+660.05 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 252112 0 0 0 63929 978 0 0 25 0 1 0 1844196832 860434432 209757 4294967295 134512640 135167914 3221224448 3221040840 134693631 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 210067 209757 162 162 0 209905 0 [pid=27513] vsize: 840268 Current children cumulated CPU time (s) 649.19 Current children cumulated vsize (Kb) 842396 [startup+670.05 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 254439 0 0 0 64906 988 0 0 25 0 1 0 1844196832 869965824 212084 4294967295 134512640 135167914 3221224448 3221040960 134844751 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 212394 212084 162 162 0 212232 0 [pid=27513] vsize: 849576 Current children cumulated CPU time (s) 659.06 Current children cumulated vsize (Kb) 851704 [startup+680.051 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 257324 0 0 0 65875 1002 0 0 25 0 1 0 1844196832 881782784 214969 4294967295 134512640 135167914 3221224448 3221036444 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 215279 214969 162 162 0 215117 0 [pid=27513] vsize: 861116 Current children cumulated CPU time (s) 668.89 Current children cumulated vsize (Kb) 863244 [startup+690.051 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 259681 0 0 0 66850 1012 0 0 25 0 1 0 1844196832 891387904 217326 4294967295 134512640 135167914 3221224448 3221054304 134845881 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 217624 217326 162 162 0 217462 0 [pid=27513] vsize: 870496 Current children cumulated CPU time (s) 678.74 Current children cumulated vsize (Kb) 872624 [startup+700.052 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 262128 0 0 0 67822 1022 0 0 25 0 1 0 1844196832 901373952 219773 4294967295 134512640 135167914 3221224448 3221062752 134849201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 220062 219773 162 162 0 219900 0 [pid=27513] vsize: 880248 Current children cumulated CPU time (s) 688.56 Current children cumulated vsize (Kb) 882376 [startup+710.054 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 264479 0 0 0 68795 1033 0 0 25 0 1 0 1844196832 911003648 222124 4294967295 134512640 135167914 3221224448 3221041764 134843000 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 222413 222124 162 162 0 222251 0 [pid=27513] vsize: 889652 Current children cumulated CPU time (s) 698.4 Current children cumulated vsize (Kb) 891780 [startup+720.053 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 266822 0 0 0 69769 1043 0 0 25 0 1 0 1844196832 920600576 224467 4294967295 134512640 135167914 3221224448 3221046652 134693552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 224756 224467 162 162 0 224594 0 [pid=27513] vsize: 899024 Current children cumulated CPU time (s) 708.24 Current children cumulated vsize (Kb) 901152 [startup+730.054 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 269276 0 0 0 70742 1056 0 0 25 0 1 0 1844196832 930635776 226921 4294967295 134512640 135167914 3221224448 3221063924 134697276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 227206 226921 162 162 0 227044 0 [pid=27513] vsize: 908824 Current children cumulated CPU time (s) 718.1 Current children cumulated vsize (Kb) 910952 [startup+740.055 s] Raw data (loadavg): 1.00 0.98 0.91 2/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) R 27508 27508 20728 0 -1 0 271624 0 8 0 71710 1070 0 0 25 0 1 0 1844196832 940187648 229150 4294967295 134512640 135167914 3221224448 3221065568 134619209 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27513/statm): 229538 229150 162 162 0 229376 0 [pid=27513] vsize: 918152 Current children cumulated CPU time (s) 727.92 Current children cumulated vsize (Kb) 920280 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+741.561 s] Raw data (loadavg): 1.00 0.98 0.91 1/57 27513 Raw data (/proc/27508/stat): 27508 (minisat+_script) S 27507 27508 20728 0 -1 0 314 592 0 0 0 1 8 3 17 0 1 0 1844196815 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27508/statm): 532 234 485 147 0 385 0 [pid=27508] vsize: 2128 Raw data (/proc/27513/stat): 27513 (minisat+_bignum) T 27508 27508 20728 0 -1 0 271987 0 15 0 71853 1071 0 0 25 0 1 0 1844196832 941543424 229475 4294967295 134512640 135167914 3221224448 3221040444 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27513/statm): 229869 229475 162 162 0 229707 0 [pid=27513] vsize: 919476 Current children cumulated CPU time (s) 729.36 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -27508 Sleeping 2 seconds One traced child (pid=27508) ended because it received signal 15 (SIGTERM) One traced child (pid=27513) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 741.995 CPU time (s): 729.671 CPU user time (s): 718.532 CPU system time (s): 11.1393 CPU usage (%): 98.339 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !