Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-core4872-1529.opb |
MD5SUM | 21523a021e6bde8cb1bd98f2664add6c |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2030592000000000 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 24975 |
Biggest coefficient in the objective function | 53687091200000000000 |
Number of bits for the biggest coefficient in the objective function | 66 |
Sum of the numbers in the objective function | 226603053881884901376 |
Number of bits of the sum of numbers in the objective function | 68 |
Biggest number in a constraint | 10240000000000000000000 |
Number of bits of the biggest number in a constraint | 74 |
Biggest sum of numbers in a constraint | 10466603053881885720576 |
Number of bits of the biggest sum of numbers | 74 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1206.69 |
Number of variables | 24975 |
Total number of constraints | 29520 |
Number of constraints which are clauses | 4872 |
Number of constraints which are cardinality constraints (but not clauses) | 24647 |
Number of constraints which are nor clauses,nor cardinality constraints | 1 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 24975 |
LAUNCH ON wulflinc23 THE 2005-09-20 02:05:43 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3102 boxname=wulflinc23 idbench=758 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 21523a021e6bde8cb1bd98f2664add6c /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-core4872-1529.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-core4872-1529.opb IDLAUNCH: 3102 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 921640 kB Buffers: 6948 kB Cached: 78344 kB SwapCached: 796 kB Active: 24104 kB Inactive: 63776 kB HighTotal: 131008 kB HighFree: 49420 kB LowTotal: 903652 kB LowFree: 872220 kB SwapTotal: 2097136 kB SwapFree: 2095788 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5552 kB Slab: 19384 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 02:25:53 (client local time) WITH STATUS 0 IN 1207.92 SECONDS stats: 3102 7 1207.92 0
c Parsing PB file... c PARSE ERROR! [line 24660] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 4760 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: =================================== c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[ 325]---> Adder-cost: 35658 maxlim: 8607 bits: 15/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 254172 1062419 | 84724 0 0 nan | 0.000 % | c | 100 | 254172 1062419 | 93196 100 307 3.1 | 0.091 % | c | 250 | 254172 1062419 | 102516 250 759 3.0 | 0.091 % | c | 475 | 254172 1062419 | 112767 475 1530 3.2 | 0.091 % | c | 812 | 254172 1062419 | 124044 812 2547 3.1 | 0.091 % | c | 1318 | 254172 1062419 | 136448 1318 4099 3.1 | 0.091 % | c | 2077 | 254172 1062419 | 150093 2077 6461 3.1 | 0.091 % | c | 3216 | 254172 1062419 | 165103 3216 10253 3.2 | 0.091 % | c | 4925 | 254172 1062419 | 181613 4925 15984 3.2 | 0.091 % | c | 7487 | 254172 1062419 | 199774 7487 24911 3.3 | 0.091 % | c | 11331 | 254172 1062419 | 219752 11331 38495 3.4 | 0.091 % | c | 17097 | 254172 1062419 | 241727 17097 59086 3.5 | 0.091 % | c | 25746 | 254172 1062419 | 265900 25746 92685 3.6 | 0.091 % | c | 38720 | 254172 1062419 | 292490 38720 146314 3.8 | 0.091 % | c | 58181 | 254172 1062419 | 321739 58181 247647 4.3 | 0.091 % |
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/26501/stat): 26501 (minisat+_script) R 26500 26501 5299 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854812399 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/26501/statm): 174 3 169 147 0 27 0 [pid=26501] 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=26502 New process pid=26503 New process pid=26504 execve syscall for /bin/sed executable One traced child (pid=26503) 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=26504) exited with status: 0 One traced child (pid=26502) exited with status: 0 New process pid=26505 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-core4872-1529.opb One traced child (pid=26505) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=26506 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-core4872-1529.opb [startup+10.0037 s] Raw data (loadavg): 0.93 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 3172 0 0 0 838 21 0 0 25 0 1 0 1854812514 13623296 3116 4294967295 134512640 135167914 3221224432 3221222168 134581185 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 3326 3116 162 162 0 3164 0 [pid=26506] vsize: 13304 Current children cumulated CPU time (s) 8.86 Current children cumulated vsize (Kb) 15432 [startup+20.0043 s] Raw data (loadavg): 0.94 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 8962 0 0 0 1785 46 0 0 25 0 1 0 1854812514 26963968 6377 4294967295 134512640 135167914 3221224432 3217629872 134844731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6583 6377 162 162 0 6421 0 [pid=26506] vsize: 26332 Current children cumulated CPU time (s) 18.58 Current children cumulated vsize (Kb) 28460 [startup+30.0049 s] Raw data (loadavg): 0.95 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 8996 0 0 0 2786 46 0 0 25 0 1 0 1854812514 27103232 6411 4294967295 134512640 135167914 3221224432 3218106576 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6617 6411 162 162 0 6455 0 [pid=26506] vsize: 26468 Current children cumulated CPU time (s) 28.59 Current children cumulated vsize (Kb) 28596 [startup+40.0056 s] Raw data (loadavg): 0.96 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9014 0 0 0 3786 46 0 0 25 0 1 0 1854812514 27209728 6429 4294967295 134512640 135167914 3221224432 3218396432 134845881 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6643 6429 162 162 0 6481 0 [pid=26506] vsize: 26572 Current children cumulated CPU time (s) 38.59 Current children cumulated vsize (Kb) 28700 [startup+50.0062 s] Raw data (loadavg): 0.96 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9058 0 0 0 4786 46 0 0 25 0 1 0 1854812514 27377664 6473 4294967295 134512640 135167914 3221224432 3218621280 134845895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6684 6473 162 162 0 6522 0 [pid=26506] vsize: 26736 Current children cumulated CPU time (s) 48.59 Current children cumulated vsize (Kb) 28864 [startup+60.0069 s] Raw data (loadavg): 0.97 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9061 0 0 0 5786 46 0 0 25 0 1 0 1854812514 27377664 6476 4294967295 134512640 135167914 3221224432 3218809520 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6684 6476 162 162 0 6522 0 [pid=26506] vsize: 26736 Current children cumulated CPU time (s) 58.59 Current children cumulated vsize (Kb) 28864 [startup+70.0065 s] Raw data (loadavg): 0.97 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9064 0 0 0 6786 46 0 0 25 0 1 0 1854812514 27381760 6479 4294967295 134512640 135167914 3221224432 3218972128 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6685 6479 162 162 0 6523 0 [pid=26506] vsize: 26740 Current children cumulated CPU time (s) 68.59 Current children cumulated vsize (Kb) 28868 [startup+80.0071 s] Raw data (loadavg): 0.98 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9092 0 0 0 7786 46 0 0 25 0 1 0 1854812514 27590656 6507 4294967295 134512640 135167914 3221224432 3219118192 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6736 6507 162 162 0 6574 0 [pid=26506] vsize: 26944 Current children cumulated CPU time (s) 78.59 Current children cumulated vsize (Kb) 29072 [startup+90.0068 s] Raw data (loadavg): 0.98 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 8786 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3218493260 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0 [pid=26506] vsize: 26944 Current children cumulated CPU time (s) 88.59 Current children cumulated vsize (Kb) 29072 [startup+100.007 s] Raw data (loadavg): 0.98 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 9786 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3218293424 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0 [pid=26506] vsize: 26944 Current children cumulated CPU time (s) 98.59 Current children cumulated vsize (Kb) 29072 [startup+110.008 s] Raw data (loadavg): 0.98 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 10787 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3218139984 134694428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0 [pid=26506] vsize: 26944 Current children cumulated CPU time (s) 108.6 Current children cumulated vsize (Kb) 29072 [startup+120.009 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 11787 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3217967528 134849087 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0 [pid=26506] vsize: 26944 Current children cumulated CPU time (s) 118.6 Current children cumulated vsize (Kb) 29072 [startup+130.009 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 12787 46 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3217732768 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0 [pid=26506] vsize: 26944 Current children cumulated CPU time (s) 128.6 Current children cumulated vsize (Kb) 29072 [startup+140.009 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9093 0 0 0 13787 47 0 0 25 0 1 0 1854812514 27590656 6508 4294967295 134512640 135167914 3221224432 3217452224 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6736 6508 162 162 0 6574 0 [pid=26506] vsize: 26944 Current children cumulated CPU time (s) 138.61 Current children cumulated vsize (Kb) 29072 [startup+150.01 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9160 0 0 0 14786 47 0 0 25 0 1 0 1854812514 27844608 6575 4294967295 134512640 135167914 3221224432 3217631072 134693566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6798 6575 162 162 0 6636 0 [pid=26506] vsize: 27192 Current children cumulated CPU time (s) 148.6 Current children cumulated vsize (Kb) 29320 [startup+160.01 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9258 0 0 0 15785 49 0 0 25 0 1 0 1854812514 28192768 6673 4294967295 134512640 135167914 3221224432 3218623172 134849086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6883 6673 162 162 0 6721 0 [pid=26506] vsize: 27532 Current children cumulated CPU time (s) 158.61 Current children cumulated vsize (Kb) 29660 [startup+170.01 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9282 0 0 0 16783 50 0 0 25 0 1 0 1854812514 28459008 6697 4294967295 134512640 135167914 3221224432 3219131852 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6948 6697 162 162 0 6786 0 [pid=26506] vsize: 27792 Current children cumulated CPU time (s) 168.6 Current children cumulated vsize (Kb) 29920 [startup+180.011 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9283 0 0 0 17783 51 0 0 25 0 1 0 1854812514 28463104 6698 4294967295 134512640 135167914 3221224432 3217868716 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6949 6698 162 162 0 6787 0 [pid=26506] vsize: 27796 Current children cumulated CPU time (s) 178.61 Current children cumulated vsize (Kb) 29924 [startup+190.011 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9324 0 0 0 18782 51 0 0 25 0 1 0 1854812514 28631040 6739 4294967295 134512640 135167914 3221224432 3217356240 134624000 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 6990 6739 162 162 0 6828 0 [pid=26506] vsize: 27960 Current children cumulated CPU time (s) 188.6 Current children cumulated vsize (Kb) 30088 [startup+200.012 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9578 0 0 0 19781 52 0 0 25 0 1 0 1854812514 29265920 6909 4294967295 134512640 135167914 3221224432 3218399132 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7145 6909 162 162 0 6983 0 [pid=26506] vsize: 28580 Current children cumulated CPU time (s) 198.6 Current children cumulated vsize (Kb) 30708 [startup+210.012 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9610 0 0 0 20781 52 0 0 25 0 1 0 1854812514 29364224 6941 4294967295 134512640 135167914 3221224432 3218999184 134845906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7169 6941 162 162 0 7007 0 [pid=26506] vsize: 28676 Current children cumulated CPU time (s) 208.6 Current children cumulated vsize (Kb) 30804 [startup+220.013 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9618 0 0 0 21781 52 0 0 25 0 1 0 1854812514 29388800 6949 4294967295 134512640 135167914 3221224432 3218470400 134693576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7175 6949 162 162 0 7013 0 [pid=26506] vsize: 28700 Current children cumulated CPU time (s) 218.6 Current children cumulated vsize (Kb) 30828 [startup+230.014 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9618 0 0 0 22781 53 0 0 25 0 1 0 1854812514 29388800 6949 4294967295 134512640 135167914 3221224432 3217953840 134694428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7175 6949 162 162 0 7013 0 [pid=26506] vsize: 28700 Current children cumulated CPU time (s) 228.61 Current children cumulated vsize (Kb) 30828 [startup+240.013 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9618 0 0 0 23781 53 0 0 25 0 1 0 1854812514 29388800 6949 4294967295 134512640 135167914 3221224432 3217560272 134843064 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7175 6949 162 162 0 7013 0 [pid=26506] vsize: 28700 Current children cumulated CPU time (s) 238.61 Current children cumulated vsize (Kb) 30828 [startup+250.014 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9710 0 0 0 24779 54 0 0 25 0 1 0 1854812514 29741056 7041 4294967295 134512640 135167914 3221224432 3217676528 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7261 7041 162 162 0 7099 0 [pid=26506] vsize: 29044 Current children cumulated CPU time (s) 248.6 Current children cumulated vsize (Kb) 31172 [startup+260.015 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9757 0 0 0 25778 54 0 0 25 0 1 0 1854812514 29884416 7088 4294967295 134512640 135167914 3221224432 3218576272 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7296 7088 162 162 0 7134 0 [pid=26506] vsize: 29184 Current children cumulated CPU time (s) 258.59 Current children cumulated vsize (Kb) 31312 [startup+270.014 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9787 0 0 0 26778 55 0 0 25 0 1 0 1854812514 30371840 7118 4294967295 134512640 135167914 3221224432 3218648440 134845939 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7415 7118 162 162 0 7253 0 [pid=26506] vsize: 29660 Current children cumulated CPU time (s) 268.6 Current children cumulated vsize (Kb) 31788 [startup+280.015 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9859 0 0 0 27777 56 0 0 25 0 1 0 1854812514 30662656 7190 4294967295 134512640 135167914 3221224432 3217311008 134624420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7486 7190 162 162 0 7324 0 [pid=26506] vsize: 29944 Current children cumulated CPU time (s) 278.6 Current children cumulated vsize (Kb) 32072 [startup+290.016 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 9927 0 0 0 28777 56 0 0 25 0 1 0 1854812514 30871552 7258 4294967295 134512640 135167914 3221224432 3218591616 134624732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7537 7258 162 162 0 7375 0 [pid=26506] vsize: 30148 Current children cumulated CPU time (s) 288.6 Current children cumulated vsize (Kb) 32276 [startup+300.016 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10286 0 0 0 29776 57 0 0 25 0 1 0 1854812514 31633408 7451 4294967295 134512640 135167914 3221224432 3219140640 134624732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7723 7451 162 162 0 7561 0 [pid=26506] vsize: 30892 Current children cumulated CPU time (s) 298.6 Current children cumulated vsize (Kb) 33020 [startup+310.017 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10287 0 0 0 30776 57 0 0 25 0 1 0 1854812514 31633408 7452 4294967295 134512640 135167914 3221224432 3218694320 134845913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7723 7452 162 162 0 7561 0 [pid=26506] vsize: 30892 Current children cumulated CPU time (s) 308.6 Current children cumulated vsize (Kb) 33020 [startup+320.017 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10287 0 0 0 31776 57 0 0 25 0 1 0 1854812514 31633408 7452 4294967295 134512640 135167914 3221224432 3218312892 134845940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7723 7452 162 162 0 7561 0 [pid=26506] vsize: 30892 Current children cumulated CPU time (s) 318.6 Current children cumulated vsize (Kb) 33020 [startup+330.017 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10287 0 0 0 32776 57 0 0 25 0 1 0 1854812514 31633408 7452 4294967295 134512640 135167914 3221224432 3217836280 134624136 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7723 7452 162 162 0 7561 0 [pid=26506] vsize: 30892 Current children cumulated CPU time (s) 328.6 Current children cumulated vsize (Kb) 33020 [startup+340.017 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10361 0 0 0 33775 58 0 0 25 0 1 0 1854812514 31932416 7526 4294967295 134512640 135167914 3221224432 3217357960 134842997 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7796 7526 162 162 0 7634 0 [pid=26506] vsize: 31184 Current children cumulated CPU time (s) 338.6 Current children cumulated vsize (Kb) 33312 [startup+350.017 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10409 0 0 0 34774 59 0 0 25 0 1 0 1854812514 32079872 7574 4294967295 134512640 135167914 3221224432 3218258080 134624772 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7832 7574 162 162 0 7670 0 [pid=26506] vsize: 31328 Current children cumulated CPU time (s) 348.6 Current children cumulated vsize (Kb) 33456 [startup+360.018 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10444 0 0 0 35774 59 0 0 25 0 1 0 1854812514 32186368 7609 4294967295 134512640 135167914 3221224432 3218925776 134694428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7858 7609 162 162 0 7696 0 [pid=26506] vsize: 31432 Current children cumulated CPU time (s) 358.6 Current children cumulated vsize (Kb) 33560 [startup+370.019 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10456 0 0 0 36774 59 0 0 25 0 1 0 1854812514 32223232 7621 4294967295 134512640 135167914 3221224432 3218341952 134845933 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7867 7621 162 162 0 7705 0 [pid=26506] vsize: 31468 Current children cumulated CPU time (s) 368.6 Current children cumulated vsize (Kb) 33596 [startup+380.019 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10475 0 0 0 37774 59 0 0 25 0 1 0 1854812514 32301056 7640 4294967295 134512640 135167914 3221224432 3217460592 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7886 7640 162 162 0 7724 0 [pid=26506] vsize: 31544 Current children cumulated CPU time (s) 378.6 Current children cumulated vsize (Kb) 33672 [startup+390.019 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10569 0 0 0 38773 60 0 0 25 0 1 0 1854812514 32641024 7734 4294967295 134512640 135167914 3221224432 3218090048 134693566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 7969 7734 162 162 0 7807 0 [pid=26506] vsize: 31876 Current children cumulated CPU time (s) 388.6 Current children cumulated vsize (Kb) 34004 [startup+400.021 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 10611 0 0 0 39772 60 0 0 25 0 1 0 1854812514 32772096 7776 4294967295 134512640 135167914 3221224432 3218877392 134694439 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 8001 7776 162 162 0 7839 0 [pid=26506] vsize: 32004 Current children cumulated CPU time (s) 398.59 Current children cumulated vsize (Kb) 34132 [startup+410.021 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 29645 0 0 0 40682 119 0 0 25 0 1 0 1854812514 110194688 24503 4294967295 134512640 135167914 3221224432 3221222176 134524032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 26903 24503 162 162 0 26741 0 [pid=26506] vsize: 107612 Current children cumulated CPU time (s) 408.28 Current children cumulated vsize (Kb) 109740 [startup+420.021 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36287 0 0 0 41633 145 0 0 25 0 1 0 1854812514 119820288 28409 4294967295 134512640 135167914 3221224432 3221223136 134566158 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29253 28409 162 162 0 29091 0 [pid=26506] vsize: 117012 Current children cumulated CPU time (s) 418.05 Current children cumulated vsize (Kb) 119140 [startup+430.023 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36314 0 0 0 42632 146 0 0 25 0 1 0 1854812514 119934976 28436 4294967295 134512640 135167914 3221224432 3221223104 134562382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29281 28436 162 162 0 29119 0 [pid=26506] vsize: 117124 Current children cumulated CPU time (s) 428.05 Current children cumulated vsize (Kb) 119252 [startup+440.023 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36322 0 0 0 43632 146 0 0 25 0 1 0 1854812514 119963648 28444 4294967295 134512640 135167914 3221224432 3221223168 134559404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29288 28444 162 162 0 29126 0 [pid=26506] vsize: 117152 Current children cumulated CPU time (s) 438.05 Current children cumulated vsize (Kb) 119280 [startup+450.024 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36336 0 0 0 44632 146 0 0 25 0 1 0 1854812514 120012800 28458 4294967295 134512640 135167914 3221224432 3221223136 134563082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29300 28458 162 162 0 29138 0 [pid=26506] vsize: 117200 Current children cumulated CPU time (s) 448.05 Current children cumulated vsize (Kb) 119328 [startup+460.024 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36353 0 0 0 45632 146 0 0 25 0 1 0 1854812514 120107008 28475 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29323 28475 162 162 0 29161 0 [pid=26506] vsize: 117292 Current children cumulated CPU time (s) 458.05 Current children cumulated vsize (Kb) 119420 [startup+470.025 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36360 0 0 0 46632 146 0 0 25 0 1 0 1854812514 120131584 28482 4294967295 134512640 135167914 3221224432 3221223120 134566738 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29329 28482 162 162 0 29167 0 [pid=26506] vsize: 117316 Current children cumulated CPU time (s) 468.05 Current children cumulated vsize (Kb) 119444 [startup+480.026 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36372 0 0 0 47632 147 0 0 25 0 1 0 1854812514 120168448 28494 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29338 28494 162 162 0 29176 0 [pid=26506] vsize: 117352 Current children cumulated CPU time (s) 478.06 Current children cumulated vsize (Kb) 119480 [startup+490.026 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36383 0 0 0 48633 147 0 0 25 0 1 0 1854812514 120205312 28505 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29347 28505 162 162 0 29185 0 [pid=26506] vsize: 117388 Current children cumulated CPU time (s) 488.07 Current children cumulated vsize (Kb) 119516 [startup+500.027 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36394 0 0 0 49632 147 0 0 25 0 1 0 1854812514 120246272 28516 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29357 28516 162 162 0 29195 0 [pid=26506] vsize: 117428 Current children cumulated CPU time (s) 498.06 Current children cumulated vsize (Kb) 119556 [startup+510.028 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36404 0 0 0 50632 147 0 0 25 0 1 0 1854812514 120283136 28526 4294967295 134512640 135167914 3221224432 3221223120 134566713 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29366 28526 162 162 0 29204 0 [pid=26506] vsize: 117464 Current children cumulated CPU time (s) 508.06 Current children cumulated vsize (Kb) 119592 [startup+520.027 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36411 0 0 0 51632 147 0 0 25 0 1 0 1854812514 120311808 28533 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29373 28533 162 162 0 29211 0 [pid=26506] vsize: 117492 Current children cumulated CPU time (s) 518.06 Current children cumulated vsize (Kb) 119620 [startup+530.028 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36430 0 0 0 52632 147 0 0 25 0 1 0 1854812514 120446976 28552 4294967295 134512640 135167914 3221224432 3221223092 134567790 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29406 28552 162 162 0 29244 0 [pid=26506] vsize: 117624 Current children cumulated CPU time (s) 528.06 Current children cumulated vsize (Kb) 119752 [startup+540.029 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36431 0 0 0 53632 147 0 0 25 0 1 0 1854812514 120446976 28553 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29406 28553 162 162 0 29244 0 [pid=26506] vsize: 117624 Current children cumulated CPU time (s) 538.06 Current children cumulated vsize (Kb) 119752 [startup+550.029 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36444 0 0 0 54632 147 0 0 25 0 1 0 1854812514 120483840 28566 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29415 28566 162 162 0 29253 0 [pid=26506] vsize: 117660 Current children cumulated CPU time (s) 548.06 Current children cumulated vsize (Kb) 119788 [startup+560.03 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36453 0 0 0 55633 147 0 0 25 0 1 0 1854812514 120516608 28575 4294967295 134512640 135167914 3221224432 3221223168 134559387 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29423 28575 162 162 0 29261 0 [pid=26506] vsize: 117692 Current children cumulated CPU time (s) 558.07 Current children cumulated vsize (Kb) 119820 [startup+570.031 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36464 0 0 0 56632 148 0 0 25 0 1 0 1854812514 120557568 28586 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29433 28586 162 162 0 29271 0 [pid=26506] vsize: 117732 Current children cumulated CPU time (s) 568.07 Current children cumulated vsize (Kb) 119860 [startup+580.031 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36472 0 0 0 57632 148 0 0 25 0 1 0 1854812514 120586240 28594 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29440 28594 162 162 0 29278 0 [pid=26506] vsize: 117760 Current children cumulated CPU time (s) 578.07 Current children cumulated vsize (Kb) 119888 [startup+590.032 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36483 0 0 0 58632 148 0 0 25 0 1 0 1854812514 120623104 28605 4294967295 134512640 135167914 3221224432 3221223092 134567717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29449 28605 162 162 0 29287 0 [pid=26506] vsize: 117796 Current children cumulated CPU time (s) 588.07 Current children cumulated vsize (Kb) 119924 [startup+600.032 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36490 0 0 0 59632 148 0 0 25 0 1 0 1854812514 120651776 28612 4294967295 134512640 135167914 3221224432 3221223092 134567717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29456 28612 162 162 0 29294 0 [pid=26506] vsize: 117824 Current children cumulated CPU time (s) 598.07 Current children cumulated vsize (Kb) 119952 [startup+610.033 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36499 0 0 0 60632 149 0 0 25 0 1 0 1854812514 120684544 28621 4294967295 134512640 135167914 3221224432 3221223092 134567717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29464 28621 162 162 0 29302 0 [pid=26506] vsize: 117856 Current children cumulated CPU time (s) 608.08 Current children cumulated vsize (Kb) 119984 [startup+620.033 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36508 0 0 0 61631 149 0 0 25 0 1 0 1854812514 120717312 28630 4294967295 134512640 135167914 3221224432 3221223168 134559407 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26506/statm): 29472 28630 162 162 0 29310 0 [pid=26506] vsize: 117888 Current children cumulated CPU time (s) 618.07 Current children cumulated vsize (Kb) 120016 [startup+630.033 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36517 0 0 0 62631 149 0 0 25 0 1 0 1854812514 120750080 28639 4294967295 134512640 135167914 3221224432 3221223136 134562815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29480 28639 162 162 0 29318 0 [pid=26506] vsize: 117920 Current children cumulated CPU time (s) 628.07 Current children cumulated vsize (Kb) 120048 [startup+640.034 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36525 0 0 0 63631 149 0 0 25 0 1 0 1854812514 120778752 28647 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29487 28647 162 162 0 29325 0 [pid=26506] vsize: 117948 Current children cumulated CPU time (s) 638.07 Current children cumulated vsize (Kb) 120076 [startup+650.035 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36534 0 0 0 64631 150 0 0 25 0 1 0 1854812514 120811520 28656 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29495 28656 162 162 0 29333 0 [pid=26506] vsize: 117980 Current children cumulated CPU time (s) 648.08 Current children cumulated vsize (Kb) 120108 [startup+660.035 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36542 0 0 0 65631 150 0 0 25 0 1 0 1854812514 120840192 28664 4294967295 134512640 135167914 3221224432 3221223116 134567636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29502 28664 162 162 0 29340 0 [pid=26506] vsize: 118008 Current children cumulated CPU time (s) 658.08 Current children cumulated vsize (Kb) 120136 [startup+670.036 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36550 0 0 0 66631 150 0 0 25 0 1 0 1854812514 120872960 28672 4294967295 134512640 135167914 3221224432 3221223136 134566347 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29510 28672 162 162 0 29348 0 [pid=26506] vsize: 118040 Current children cumulated CPU time (s) 668.08 Current children cumulated vsize (Kb) 120168 [startup+680.037 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36559 0 0 0 67631 150 0 0 25 0 1 0 1854812514 120905728 28681 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29518 28681 162 162 0 29356 0 [pid=26506] vsize: 118072 Current children cumulated CPU time (s) 678.08 Current children cumulated vsize (Kb) 120200 [startup+690.037 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36566 0 0 0 68631 150 0 0 25 0 1 0 1854812514 120934400 28688 4294967295 134512640 135167914 3221224432 3221223136 134566316 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29525 28688 162 162 0 29363 0 [pid=26506] vsize: 118100 Current children cumulated CPU time (s) 688.08 Current children cumulated vsize (Kb) 120228 [startup+700.038 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36599 0 0 0 69632 150 0 0 25 0 1 0 1854812514 121196544 28721 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29589 28721 162 162 0 29427 0 [pid=26506] vsize: 118356 Current children cumulated CPU time (s) 698.09 Current children cumulated vsize (Kb) 120484 [startup+710.038 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36600 0 0 0 70632 150 0 0 25 0 1 0 1854812514 121196544 28722 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29589 28722 162 162 0 29427 0 [pid=26506] vsize: 118356 Current children cumulated CPU time (s) 708.09 Current children cumulated vsize (Kb) 120484 [startup+720.038 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36601 0 0 0 71632 150 0 0 25 0 1 0 1854812514 121196544 28723 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29589 28723 162 162 0 29427 0 [pid=26506] vsize: 118356 Current children cumulated CPU time (s) 718.09 Current children cumulated vsize (Kb) 120484 [startup+730.039 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36602 0 0 0 72632 150 0 0 25 0 1 0 1854812514 121196544 28724 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29589 28724 162 162 0 29427 0 [pid=26506] vsize: 118356 Current children cumulated CPU time (s) 728.09 Current children cumulated vsize (Kb) 120484 [startup+740.039 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36606 0 0 0 73632 150 0 0 25 0 1 0 1854812514 121208832 28728 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29592 28728 162 162 0 29430 0 [pid=26506] vsize: 118368 Current children cumulated CPU time (s) 738.09 Current children cumulated vsize (Kb) 120496 [startup+750.04 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36614 0 0 0 74632 150 0 0 25 0 1 0 1854812514 121241600 28736 4294967295 134512640 135167914 3221224432 3221223136 134562874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29600 28736 162 162 0 29438 0 [pid=26506] vsize: 118400 Current children cumulated CPU time (s) 748.09 Current children cumulated vsize (Kb) 120528 [startup+760.041 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36622 0 0 0 75631 151 0 0 25 0 1 0 1854812514 121270272 28744 4294967295 134512640 135167914 3221224432 3221223092 134567727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29607 28744 162 162 0 29445 0 [pid=26506] vsize: 118428 Current children cumulated CPU time (s) 758.09 Current children cumulated vsize (Kb) 120556 [startup+770.04 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36628 0 0 0 76630 152 0 0 25 0 1 0 1854812514 121290752 28750 4294967295 134512640 135167914 3221224432 3221223156 134559539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26506/statm): 29612 28750 162 162 0 29450 0 [pid=26506] vsize: 118448 Current children cumulated CPU time (s) 768.09 Current children cumulated vsize (Kb) 120576 [startup+780.042 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36641 0 0 0 77628 153 0 0 25 0 1 0 1854812514 121339904 28763 4294967295 134512640 135167914 3221224432 3221223136 134562535 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29624 28763 162 162 0 29462 0 [pid=26506] vsize: 118496 Current children cumulated CPU time (s) 778.08 Current children cumulated vsize (Kb) 120624 [startup+790.043 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36648 0 0 0 78628 153 0 0 25 0 1 0 1854812514 121368576 28770 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29631 28770 162 162 0 29469 0 [pid=26506] vsize: 118524 Current children cumulated CPU time (s) 788.08 Current children cumulated vsize (Kb) 120652 [startup+800.043 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36656 0 0 0 79628 153 0 0 25 0 1 0 1854812514 121397248 28778 4294967295 134512640 135167914 3221224432 3221223128 134562693 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29638 28778 162 162 0 29476 0 [pid=26506] vsize: 118552 Current children cumulated CPU time (s) 798.08 Current children cumulated vsize (Kb) 120680 [startup+810.044 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36666 0 0 0 80628 154 0 0 25 0 1 0 1854812514 121434112 28788 4294967295 134512640 135167914 3221224432 3221223092 134567722 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29647 28788 162 162 0 29485 0 [pid=26506] vsize: 118588 Current children cumulated CPU time (s) 808.09 Current children cumulated vsize (Kb) 120716 [startup+820.044 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36674 0 0 0 81627 154 0 0 25 0 1 0 1854812514 121462784 28796 4294967295 134512640 135167914 3221224432 3221223168 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29654 28796 162 162 0 29492 0 [pid=26506] vsize: 118616 Current children cumulated CPU time (s) 818.08 Current children cumulated vsize (Kb) 120744 [startup+830.044 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36683 0 0 0 82627 155 0 0 25 0 1 0 1854812514 121499648 28805 4294967295 134512640 135167914 3221224432 3221223136 134562502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29663 28805 162 162 0 29501 0 [pid=26506] vsize: 118652 Current children cumulated CPU time (s) 828.09 Current children cumulated vsize (Kb) 120780 [startup+840.045 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36692 0 0 0 83627 155 0 0 25 0 1 0 1854812514 121532416 28814 4294967295 134512640 135167914 3221224432 3221223092 134567786 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29671 28814 162 162 0 29509 0 [pid=26506] vsize: 118684 Current children cumulated CPU time (s) 838.09 Current children cumulated vsize (Kb) 120812 [startup+850.047 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36701 0 0 0 84627 155 0 0 25 0 1 0 1854812514 121565184 28823 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29679 28823 162 162 0 29517 0 [pid=26506] vsize: 118716 Current children cumulated CPU time (s) 848.09 Current children cumulated vsize (Kb) 120844 [startup+860.047 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36711 0 0 0 85627 155 0 0 25 0 1 0 1854812514 121602048 28833 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29688 28833 162 162 0 29526 0 [pid=26506] vsize: 118752 Current children cumulated CPU time (s) 858.09 Current children cumulated vsize (Kb) 120880 [startup+870.047 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36720 0 0 0 86627 155 0 0 25 0 1 0 1854812514 121634816 28842 4294967295 134512640 135167914 3221224432 3221223136 134562618 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29696 28842 162 162 0 29534 0 [pid=26506] vsize: 118784 Current children cumulated CPU time (s) 868.09 Current children cumulated vsize (Kb) 120912 [startup+880.047 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36725 0 0 0 87627 156 0 0 25 0 1 0 1854812514 121655296 28847 4294967295 134512640 135167914 3221224432 3221223092 134567760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29701 28847 162 162 0 29539 0 [pid=26506] vsize: 118804 Current children cumulated CPU time (s) 878.1 Current children cumulated vsize (Kb) 120932 [startup+890.048 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36731 0 0 0 88627 156 0 0 25 0 1 0 1854812514 121675776 28853 4294967295 134512640 135167914 3221224432 3221223136 134562620 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29706 28853 162 162 0 29544 0 [pid=26506] vsize: 118824 Current children cumulated CPU time (s) 888.1 Current children cumulated vsize (Kb) 120952 [startup+900.049 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36741 0 0 0 89627 156 0 0 25 0 1 0 1854812514 121712640 28863 4294967295 134512640 135167914 3221224432 3221223136 134566415 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29715 28863 162 162 0 29553 0 [pid=26506] vsize: 118860 Current children cumulated CPU time (s) 898.1 Current children cumulated vsize (Kb) 120988 [startup+910.049 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36749 0 0 0 90627 156 0 0 25 0 1 0 1854812514 121745408 28871 4294967295 134512640 135167914 3221224432 3221223200 134566311 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29723 28871 162 162 0 29561 0 [pid=26506] vsize: 118892 Current children cumulated CPU time (s) 908.1 Current children cumulated vsize (Kb) 121020 [startup+920.05 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36758 0 0 0 91627 156 0 0 25 0 1 0 1854812514 121778176 28880 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29731 28880 162 162 0 29569 0 [pid=26506] vsize: 118924 Current children cumulated CPU time (s) 918.1 Current children cumulated vsize (Kb) 121052 [startup+930.051 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36767 0 0 0 92627 156 0 0 25 0 1 0 1854812514 121810944 28889 4294967295 134512640 135167914 3221224432 3221223132 134566190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29739 28889 162 162 0 29577 0 [pid=26506] vsize: 118956 Current children cumulated CPU time (s) 928.1 Current children cumulated vsize (Kb) 121084 [startup+940.051 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36775 0 0 0 93627 156 0 0 25 0 1 0 1854812514 121843712 28897 4294967295 134512640 135167914 3221224432 3221223152 134559542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29747 28897 162 162 0 29585 0 [pid=26506] vsize: 118988 Current children cumulated CPU time (s) 938.1 Current children cumulated vsize (Kb) 121116 [startup+950.052 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36786 0 0 0 94627 157 0 0 25 0 1 0 1854812514 121884672 28908 4294967295 134512640 135167914 3221224432 3221223136 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29757 28908 162 162 0 29595 0 [pid=26506] vsize: 119028 Current children cumulated CPU time (s) 948.11 Current children cumulated vsize (Kb) 121156 [startup+960.053 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36794 0 0 0 95627 157 0 0 25 0 1 0 1854812514 121913344 28916 4294967295 134512640 135167914 3221224432 3221223120 134566795 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29764 28916 162 162 0 29602 0 [pid=26506] vsize: 119056 Current children cumulated CPU time (s) 958.11 Current children cumulated vsize (Kb) 121184 [startup+970.053 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36810 0 0 0 96627 157 0 0 25 0 1 0 1854812514 121974784 28932 4294967295 134512640 135167914 3221224432 3221223092 134567697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29779 28932 162 162 0 29617 0 [pid=26506] vsize: 119116 Current children cumulated CPU time (s) 968.11 Current children cumulated vsize (Kb) 121244 [startup+980.054 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36822 0 0 0 97627 157 0 0 25 0 1 0 1854812514 122019840 28944 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29790 28944 162 162 0 29628 0 [pid=26506] vsize: 119160 Current children cumulated CPU time (s) 978.11 Current children cumulated vsize (Kb) 121288 [startup+990.054 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36834 0 0 0 98626 158 0 0 25 0 1 0 1854812514 122068992 28956 4294967295 134512640 135167914 3221224432 3221223092 134567711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29802 28956 162 162 0 29640 0 [pid=26506] vsize: 119208 Current children cumulated CPU time (s) 988.11 Current children cumulated vsize (Kb) 121336 [startup+1000.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36842 0 0 0 99626 158 0 0 25 0 1 0 1854812514 122097664 28964 4294967295 134512640 135167914 3221224432 3221223092 134567702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29809 28964 162 162 0 29647 0 [pid=26506] vsize: 119236 Current children cumulated CPU time (s) 998.11 Current children cumulated vsize (Kb) 121364 [startup+1010.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36855 0 0 0 100626 158 0 0 25 0 1 0 1854812514 122146816 28977 4294967295 134512640 135167914 3221224432 3221223092 134567763 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29821 28977 162 162 0 29659 0 [pid=26506] vsize: 119284 Current children cumulated CPU time (s) 1008.11 Current children cumulated vsize (Kb) 121412 [startup+1020.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36864 0 0 0 101626 158 0 0 25 0 1 0 1854812514 122179584 28986 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29829 28986 162 162 0 29667 0 [pid=26506] vsize: 119316 Current children cumulated CPU time (s) 1018.11 Current children cumulated vsize (Kb) 121444 [startup+1030.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36879 0 0 0 102626 158 0 0 25 0 1 0 1854812514 122236928 29001 4294967295 134512640 135167914 3221224432 3221223120 134566732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29843 29001 162 162 0 29681 0 [pid=26506] vsize: 119372 Current children cumulated CPU time (s) 1028.11 Current children cumulated vsize (Kb) 121500 [startup+1040.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36886 0 0 0 103626 158 0 0 25 0 1 0 1854812514 122265600 29008 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29850 29008 162 162 0 29688 0 [pid=26506] vsize: 119400 Current children cumulated CPU time (s) 1038.11 Current children cumulated vsize (Kb) 121528 [startup+1050.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36900 0 0 0 104625 159 0 0 25 0 1 0 1854812514 122318848 29022 4294967295 134512640 135167914 3221224432 3221223136 134562604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29863 29022 162 162 0 29701 0 [pid=26506] vsize: 119452 Current children cumulated CPU time (s) 1048.11 Current children cumulated vsize (Kb) 121580 [startup+1060.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36910 0 0 0 105625 159 0 0 25 0 1 0 1854812514 122355712 29032 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29872 29032 162 162 0 29710 0 [pid=26506] vsize: 119488 Current children cumulated CPU time (s) 1058.11 Current children cumulated vsize (Kb) 121616 [startup+1070.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36922 0 0 0 106625 159 0 0 25 0 1 0 1854812514 122400768 29044 4294967295 134512640 135167914 3221224432 3221223092 134567739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29883 29044 162 162 0 29721 0 [pid=26506] vsize: 119532 Current children cumulated CPU time (s) 1068.11 Current children cumulated vsize (Kb) 121660 [startup+1080.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36933 0 0 0 107625 159 0 0 25 0 1 0 1854812514 122445824 29055 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29894 29055 162 162 0 29732 0 [pid=26506] vsize: 119576 Current children cumulated CPU time (s) 1078.11 Current children cumulated vsize (Kb) 121704 [startup+1090.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36942 0 0 0 108625 159 0 0 25 0 1 0 1854812514 122478592 29064 4294967295 134512640 135167914 3221224432 3221223120 134566760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29902 29064 162 162 0 29740 0 [pid=26506] vsize: 119608 Current children cumulated CPU time (s) 1088.11 Current children cumulated vsize (Kb) 121736 [startup+1100.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36955 0 0 0 109625 159 0 0 25 0 1 0 1854812514 122527744 29077 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29914 29077 162 162 0 29752 0 [pid=26506] vsize: 119656 Current children cumulated CPU time (s) 1098.11 Current children cumulated vsize (Kb) 121784 [startup+1110.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36967 0 0 0 110624 160 0 0 25 0 1 0 1854812514 122576896 29089 4294967295 134512640 135167914 3221224432 3221223136 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29926 29089 162 162 0 29764 0 [pid=26506] vsize: 119704 Current children cumulated CPU time (s) 1108.11 Current children cumulated vsize (Kb) 121832 [startup+1120.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36977 0 0 0 111624 160 0 0 25 0 1 0 1854812514 122875904 29099 4294967295 134512640 135167914 3221224432 3221223136 134562604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 29999 29099 162 162 0 29837 0 [pid=26506] vsize: 119996 Current children cumulated CPU time (s) 1118.11 Current children cumulated vsize (Kb) 122124 [startup+1130.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36987 0 0 0 112624 160 0 0 25 0 1 0 1854812514 122912768 29109 4294967295 134512640 135167914 3221224432 3221223136 134562647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30008 29109 162 162 0 29846 0 [pid=26506] vsize: 120032 Current children cumulated CPU time (s) 1128.11 Current children cumulated vsize (Kb) 122160 [startup+1140.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 36996 0 0 0 113625 160 0 0 25 0 1 0 1854812514 122949632 29118 4294967295 134512640 135167914 3221224432 3221223092 134567736 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30017 29118 162 162 0 29855 0 [pid=26506] vsize: 120068 Current children cumulated CPU time (s) 1138.12 Current children cumulated vsize (Kb) 122196 [startup+1150.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37009 0 0 0 114625 160 0 0 25 0 1 0 1854812514 122998784 29131 4294967295 134512640 135167914 3221224432 3221223136 134566393 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30029 29131 162 162 0 29867 0 [pid=26506] vsize: 120116 Current children cumulated CPU time (s) 1148.12 Current children cumulated vsize (Kb) 122244 [startup+1160.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37024 0 0 0 115625 160 0 0 25 0 1 0 1854812514 123056128 29146 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30043 29146 162 162 0 29881 0 [pid=26506] vsize: 120172 Current children cumulated CPU time (s) 1158.12 Current children cumulated vsize (Kb) 122300 [startup+1170.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37034 0 0 0 116624 160 0 0 25 0 1 0 1854812514 123092992 29156 4294967295 134512640 135167914 3221224432 3221223136 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30052 29156 162 162 0 29890 0 [pid=26506] vsize: 120208 Current children cumulated CPU time (s) 1168.11 Current children cumulated vsize (Kb) 122336 [startup+1180.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37043 0 0 0 117624 160 0 0 25 0 1 0 1854812514 123129856 29165 4294967295 134512640 135167914 3221224432 3221223120 134566754 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30061 29165 162 162 0 29899 0 [pid=26506] vsize: 120244 Current children cumulated CPU time (s) 1178.11 Current children cumulated vsize (Kb) 122372 [startup+1190.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37059 0 0 0 118624 161 0 0 25 0 1 0 1854812514 123191296 29181 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30076 29181 162 162 0 29914 0 [pid=26506] vsize: 120304 Current children cumulated CPU time (s) 1188.12 Current children cumulated vsize (Kb) 122432 [startup+1200.07 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37073 0 0 0 119624 161 0 0 25 0 1 0 1854812514 123244544 29195 4294967295 134512640 135167914 3221224432 3221223136 134562874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30089 29195 162 162 0 29927 0 [pid=26506] vsize: 120356 Current children cumulated CPU time (s) 1198.12 Current children cumulated vsize (Kb) 122484 [startup+1210.07 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37089 0 0 0 120624 161 0 0 25 0 1 0 1854812514 123305984 29211 4294967295 134512640 135167914 3221224432 3221223136 134562556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30104 29211 162 162 0 29942 0 [pid=26506] vsize: 120416 Current children cumulated CPU time (s) 1208.12 Current children cumulated vsize (Kb) 122544 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 26506 Raw data (/proc/26501/stat): 26501 (minisat+_script) S 26500 26501 5299 0 -1 0 314 1251 0 0 0 0 20 7 17 0 1 0 1854812399 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26501/statm): 532 234 485 147 0 385 0 [pid=26501] vsize: 2128 Raw data (/proc/26506/stat): 26506 (minisat+_bignum) R 26501 26501 5299 0 -1 0 37089 0 0 0 120624 161 0 0 25 0 1 0 1854812514 123305984 29211 4294967295 134512640 135167914 3221224432 3221223092 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26506/statm): 30104 29211 162 162 0 29942 0 [pid=26506] vsize: 120416 Current children cumulated CPU time (s) 1208.12 Current children cumulated vsize (Kb) 122544 Sending SIGTERM to -26501 Sleeping 2 seconds One traced child (pid=26501) ended because it received signal 15 (SIGTERM) One traced child (pid=26506) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1207.92 CPU user time (s): 1206.25 CPU system time (s): 1.67174 CPU usage (%): 99.8175 Max. virtual memory (cumulated for all children) (Kb): 122544
ERROR: no interpretation found !