Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-gesa2_o.opb |
MD5SUM | 70d38efa2ca4db2a9200144005e211ed |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 10368 |
Biggest coefficient in the objective function | 418848431931392 |
Number of bits for the biggest coefficient in the objective function | 49 |
Sum of the numbers in the objective function | 180197911475330400 |
Number of bits of the sum of numbers in the objective function | 58 |
Biggest number in a constraint | 418848431931392 |
Number of bits of the biggest number in a constraint | 49 |
Biggest sum of numbers in a constraint | 180197911475330400 |
Number of bits of the biggest sum of numbers | 58 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 16224 |
Total number of constraints | 1584 |
Number of constraints which are clauses | 192 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 1392 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 309 |
LAUNCH ON wulflinc7 THE 2005-09-19 17:52:15 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2975 boxname=wulflinc7 idbench=631 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 70d38efa2ca4db2a9200144005e211ed /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-gesa2_o.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-gesa2_o.opb IDLAUNCH: 2975 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 902440 kB Buffers: 29100 kB Cached: 77808 kB SwapCached: 736 kB Active: 31368 kB Inactive: 78140 kB HighTotal: 131008 kB HighFree: 49532 kB LowTotal: 903652 kB LowFree: 852908 kB SwapTotal: 2097136 kB SwapFree: 2095896 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5720 kB Slab: 16952 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 18:12:25 (client local time) WITH STATUS 0 IN 1201.73 SECONDS stats: 2975 7 1201.73 0
c Parsing PB file... c PARSE ERROR! [line 1228] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead...
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/3756/stat): 3756 (minisat+_script) R 3755 3756 15400 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793636831 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3756/statm): 174 3 169 147 0 27 0 [pid=3756] 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=3757 New process pid=3758 New process pid=3759 execve syscall for /bin/sed executable One traced child (pid=3758) 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=3759) exited with status: 0 One traced child (pid=3757) exited with status: 0 New process pid=3760 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-gesa2_o.opb One traced child (pid=3760) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=3761 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-gesa2_o.opb [startup+10.0046 s] Raw data (loadavg): 0.94 0.98 0.79 1/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 4379 0 3 0 934 23 0 0 25 0 1 0 1793636837 17514496 3982 4294967295 134512640 135167914 3221224448 3221193084 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 4276 3982 162 162 0 4114 0 [pid=3761] vsize: 17104 Current children cumulated CPU time (s) 9.59 Current children cumulated vsize (Kb) 19232 [startup+20.0072 s] Raw data (loadavg): 0.95 0.98 0.79 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 10452 0 3 0 1883 51 0 0 25 0 1 0 1793636837 38338560 9066 4294967295 134512640 135167914 3221224448 3221193408 134522502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 9360 9066 162 162 0 9198 0 [pid=3761] vsize: 37440 Current children cumulated CPU time (s) 19.36 Current children cumulated vsize (Kb) 39568 [startup+30.0079 s] Raw data (loadavg): 0.95 0.98 0.80 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 17021 0 3 0 2832 76 0 0 25 0 1 0 1793636837 59846656 14317 4294967295 134512640 135167914 3221224448 3221199064 134849057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 14611 14317 162 162 0 14449 0 [pid=3761] vsize: 58444 Current children cumulated CPU time (s) 29.1 Current children cumulated vsize (Kb) 60572 [startup+40.0085 s] Raw data (loadavg): 0.96 0.98 0.80 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 21393 0 3 0 3783 97 0 0 25 0 1 0 1793636837 77754368 18689 4294967295 134512640 135167914 3221224448 3221197952 134620469 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 18983 18689 162 162 0 18821 0 [pid=3761] vsize: 75932 Current children cumulated CPU time (s) 38.82 Current children cumulated vsize (Kb) 78060 [startup+50.0092 s] Raw data (loadavg): 0.97 0.98 0.80 1/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 30083 0 3 0 4734 127 0 0 25 0 1 0 1793636837 102551552 24742 4294967295 134512640 135167914 3221224448 3221195548 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 25037 24742 162 162 0 24875 0 [pid=3761] vsize: 100148 Current children cumulated CPU time (s) 48.63 Current children cumulated vsize (Kb) 102276 [startup+60.0098 s] Raw data (loadavg): 0.97 0.98 0.80 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 34387 0 3 0 5691 144 0 0 25 0 1 0 1793636837 120176640 29046 4294967295 134512640 135167914 3221224448 3221193288 134847145 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3761/statm): 29340 29046 162 162 0 29178 0 [pid=3761] vsize: 117360 Current children cumulated CPU time (s) 58.37 Current children cumulated vsize (Kb) 119488 [startup+70.0104 s] Raw data (loadavg): 0.97 0.98 0.80 1/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 38582 0 3 0 6645 164 0 0 25 0 1 0 1793636837 137359360 33241 4294967295 134512640 135167914 3221224448 3221194652 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 33535 33241 162 162 0 33373 0 [pid=3761] vsize: 134140 Current children cumulated CPU time (s) 68.11 Current children cumulated vsize (Kb) 136268 [startup+80.0121 s] Raw data (loadavg): 0.98 0.98 0.81 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 42729 0 3 0 7600 184 0 0 25 0 1 0 1793636837 154345472 37388 4294967295 134512640 135167914 3221224448 3221194144 134621031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 37682 37388 162 162 0 37520 0 [pid=3761] vsize: 150728 Current children cumulated CPU time (s) 77.86 Current children cumulated vsize (Kb) 152856 [startup+90.0127 s] Raw data (loadavg): 0.98 0.98 0.81 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 55572 0 3 0 8551 219 0 0 25 0 1 0 1793636837 185352192 44958 4294967295 134512640 135167914 3221224448 3221195680 134694410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 45252 44958 162 162 0 45090 0 [pid=3761] vsize: 181008 Current children cumulated CPU time (s) 87.72 Current children cumulated vsize (Kb) 183136 [startup+100.012 s] Raw data (loadavg): 0.98 0.98 0.81 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 59713 0 3 0 9504 238 0 0 25 0 1 0 1793636837 202313728 49099 4294967295 134512640 135167914 3221224448 3221195264 134620419 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 49393 49099 162 162 0 49231 0 [pid=3761] vsize: 197572 Current children cumulated CPU time (s) 97.44 Current children cumulated vsize (Kb) 199700 [startup+110.013 s] Raw data (loadavg): 0.99 0.98 0.81 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 63837 0 3 0 10455 259 0 0 25 0 1 0 1793636837 219213824 53223 4294967295 134512640 135167914 3221224448 3221194480 134693561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 53519 53223 162 162 0 53357 0 [pid=3761] vsize: 214076 Current children cumulated CPU time (s) 107.16 Current children cumulated vsize (Kb) 216204 [startup+120.014 s] Raw data (loadavg): 0.99 0.98 0.81 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 67836 0 3 0 11412 276 0 0 25 0 1 0 1793636837 235593728 57222 4294967295 134512640 135167914 3221224448 3221196112 134522462 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 57518 57222 162 162 0 57356 0 [pid=3761] vsize: 230072 Current children cumulated CPU time (s) 116.9 Current children cumulated vsize (Kb) 232200 [startup+130.014 s] Raw data (loadavg): 0.99 0.98 0.82 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 71888 0 3 0 12365 298 0 0 25 0 1 0 1793636837 252190720 61274 4294967295 134512640 135167914 3221224448 3221194828 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3761/statm): 61570 61274 162 162 0 61408 0 [pid=3761] vsize: 246280 Current children cumulated CPU time (s) 126.65 Current children cumulated vsize (Kb) 248408 [startup+140.015 s] Raw data (loadavg): 1.06 1.00 0.82 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 75866 0 3 0 13322 315 0 0 25 0 1 0 1793636837 268480512 65252 4294967295 134512640 135167914 3221224448 3221194796 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 65547 65252 162 162 0 65385 0 [pid=3761] vsize: 262188 Current children cumulated CPU time (s) 136.39 Current children cumulated vsize (Kb) 264316 [startup+150.016 s] Raw data (loadavg): 1.05 1.00 0.82 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 79779 0 3 0 14276 334 0 0 25 0 1 0 1793636837 284508160 69165 4294967295 134512640 135167914 3221224448 3221194332 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 69460 69165 162 162 0 69298 0 [pid=3761] vsize: 277840 Current children cumulated CPU time (s) 146.12 Current children cumulated vsize (Kb) 279968 [startup+160.016 s] Raw data (loadavg): 1.04 1.00 0.82 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 83549 0 3 0 15233 352 0 0 25 0 1 0 1793636837 299950080 72935 4294967295 134512640 135167914 3221224448 3221194396 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 73230 72935 162 162 0 73068 0 [pid=3761] vsize: 292920 Current children cumulated CPU time (s) 155.87 Current children cumulated vsize (Kb) 295048 [startup+170.016 s] Raw data (loadavg): 1.04 1.00 0.83 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 107591 0 3 0 16151 414 0 0 25 0 1 0 1793636837 398426112 96977 4294967295 134512640 135167914 3221224448 3221194072 134849057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 97272 96977 162 162 0 97110 0 [pid=3761] vsize: 389088 Current children cumulated CPU time (s) 165.67 Current children cumulated vsize (Kb) 391216 [startup+180.016 s] Raw data (loadavg): 1.03 1.00 0.83 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 108790 0 3 0 17137 422 0 0 25 0 1 0 1793636837 360140800 87630 4294967295 134512640 135167914 3221224448 3221194256 134624994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 87925 87630 162 162 0 87763 0 [pid=3761] vsize: 351700 Current children cumulated CPU time (s) 175.61 Current children cumulated vsize (Kb) 353828 [startup+190.017 s] Raw data (loadavg): 1.03 1.00 0.83 1/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 112488 0 3 0 18097 439 0 0 25 0 1 0 1793636837 375287808 91328 4294967295 134512640 135167914 3221224448 3221193756 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 91623 91328 162 162 0 91461 0 [pid=3761] vsize: 366492 Current children cumulated CPU time (s) 185.38 Current children cumulated vsize (Kb) 368620 [startup+200.017 s] Raw data (loadavg): 1.02 1.00 0.83 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 116214 0 3 0 19058 455 0 0 25 0 1 0 1793636837 390549504 95054 4294967295 134512640 135167914 3221224448 3221194880 134844641 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 95349 95054 162 162 0 95187 0 [pid=3761] vsize: 381396 Current children cumulated CPU time (s) 195.15 Current children cumulated vsize (Kb) 383524 [startup+210.017 s] Raw data (loadavg): 1.02 1.00 0.83 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 119976 0 3 0 20018 470 0 0 25 0 1 0 1793636837 405958656 98816 4294967295 134512640 135167914 3221224448 3221198460 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 99111 98816 162 162 0 98949 0 [pid=3761] vsize: 396444 Current children cumulated CPU time (s) 204.9 Current children cumulated vsize (Kb) 398572 [startup+220.018 s] Raw data (loadavg): 1.01 1.00 0.83 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 123768 0 3 0 20975 488 0 0 25 0 1 0 1793636837 421490688 102608 4294967295 134512640 135167914 3221224448 3221193760 134844694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 102903 102608 162 162 0 102741 0 [pid=3761] vsize: 411612 Current children cumulated CPU time (s) 214.65 Current children cumulated vsize (Kb) 413740 [startup+230.019 s] Raw data (loadavg): 1.01 1.00 0.83 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 127392 0 3 0 21937 505 0 0 25 0 1 0 1793636837 436334592 106232 4294967295 134512640 135167914 3221224448 3221195840 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 106527 106232 162 162 0 106365 0 [pid=3761] vsize: 426108 Current children cumulated CPU time (s) 224.44 Current children cumulated vsize (Kb) 428236 [startup+240.019 s] Raw data (loadavg): 1.01 1.00 0.83 1/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 130994 0 3 0 22899 521 0 0 25 0 1 0 1793636837 451088384 109834 4294967295 134512640 135167914 3221224448 3221192988 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 110129 109834 162 162 0 109967 0 [pid=3761] vsize: 440516 Current children cumulated CPU time (s) 234.22 Current children cumulated vsize (Kb) 442644 [startup+250.02 s] Raw data (loadavg): 1.01 1.00 0.83 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 134717 0 3 0 23862 536 0 0 25 0 1 0 1793636837 466337792 113557 4294967295 134512640 135167914 3221224448 3221197184 134845930 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 113852 113557 162 162 0 113690 0 [pid=3761] vsize: 455408 Current children cumulated CPU time (s) 244 Current children cumulated vsize (Kb) 457536 [startup+260.021 s] Raw data (loadavg): 1.01 1.00 0.83 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 138480 0 3 0 24823 551 0 0 25 0 1 0 1793636837 481751040 117320 4294967295 134512640 135167914 3221224448 3221194912 134843404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 117615 117320 162 162 0 117453 0 [pid=3761] vsize: 470460 Current children cumulated CPU time (s) 253.76 Current children cumulated vsize (Kb) 472588 [startup+270.021 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 142256 0 3 0 25784 566 0 0 25 0 1 0 1793636837 497217536 121096 4294967295 134512640 135167914 3221224448 3221196416 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 121391 121096 162 162 0 121229 0 [pid=3761] vsize: 485564 Current children cumulated CPU time (s) 263.52 Current children cumulated vsize (Kb) 487692 [startup+280.022 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 145907 0 3 0 26747 582 0 0 25 0 1 0 1793636837 512172032 124747 4294967295 134512640 135167914 3221224448 3221195008 134843068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 125042 124747 162 162 0 124880 0 [pid=3761] vsize: 500168 Current children cumulated CPU time (s) 273.31 Current children cumulated vsize (Kb) 502296 [startup+290.022 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 149530 0 3 0 27705 600 0 0 25 0 1 0 1793636837 527007744 128370 4294967295 134512640 135167914 3221224448 3221194348 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 128664 128370 162 162 0 128502 0 [pid=3761] vsize: 514656 Current children cumulated CPU time (s) 283.07 Current children cumulated vsize (Kb) 516784 [startup+300.022 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 153227 0 3 0 28665 615 0 0 25 0 1 0 1793636837 542171136 132067 4294967295 134512640 135167914 3221224448 3221195232 134843404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 132366 132067 162 162 0 132204 0 [pid=3761] vsize: 529464 Current children cumulated CPU time (s) 292.82 Current children cumulated vsize (Kb) 531592 [startup+310.023 s] Raw data (loadavg): 1.00 1.00 0.84 1/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 156864 0 3 0 29628 631 0 0 25 0 1 0 1793636837 557068288 135704 4294967295 134512640 135167914 3221224448 3221194844 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136003 135704 162 162 0 135841 0 [pid=3761] vsize: 544012 Current children cumulated CPU time (s) 302.61 Current children cumulated vsize (Kb) 546140 [startup+320.023 s] Raw data (loadavg): 1.00 1.00 0.84 1/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 160357 0 3 0 30591 648 0 0 25 0 1 0 1793636837 571375616 139197 4294967295 134512640 135167914 3221224448 3221194428 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 139496 139197 162 162 0 139334 0 [pid=3761] vsize: 557984 Current children cumulated CPU time (s) 312.41 Current children cumulated vsize (Kb) 560112 [startup+330.024 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 163858 0 3 0 31554 664 0 0 25 0 1 0 1793636837 585715712 142698 4294967295 134512640 135167914 3221224448 3221198324 134697299 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 142997 142698 162 162 0 142835 0 [pid=3761] vsize: 571988 Current children cumulated CPU time (s) 322.2 Current children cumulated vsize (Kb) 574116 [startup+340.025 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 167525 0 3 0 32516 680 0 0 25 0 1 0 1793636837 600727552 146365 4294967295 134512640 135167914 3221224448 3221196412 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 146662 146365 162 162 0 146500 0 [pid=3761] vsize: 586648 Current children cumulated CPU time (s) 331.98 Current children cumulated vsize (Kb) 588776 [startup+350.024 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 173474 0 3 0 33471 703 0 0 25 0 1 0 1793636837 788549632 152314 4294967295 134512640 135167914 3221224448 3221196608 134625368 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 192517 152321 162 162 0 192355 0 [pid=3761] vsize: 770068 Current children cumulated CPU time (s) 341.76 Current children cumulated vsize (Kb) 772196 [startup+360.025 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 213380 0 3 0 34372 803 0 0 25 0 1 0 1793636837 788549632 192220 4294967295 134512640 135167914 3221224448 3221196576 134624957 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 192517 192220 162 162 0 192355 0 [pid=3761] vsize: 770068 Current children cumulated CPU time (s) 351.77 Current children cumulated vsize (Kb) 772196 [startup+370.026 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 214235 0 3 0 35359 811 0 0 25 0 1 0 1793636837 705662976 171984 4294967295 134512640 135167914 3221224448 3221194620 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 172281 171984 162 162 0 172119 0 [pid=3761] vsize: 689124 Current children cumulated CPU time (s) 361.72 Current children cumulated vsize (Kb) 691252 [startup+380.026 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) T 3756 3756 15400 0 -1 0 217817 0 3 0 36318 829 0 0 25 0 1 0 1793636837 720334848 175566 4294967295 134512640 135167914 3221224448 3221195964 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3761/statm): 175863 175566 162 162 0 175701 0 [pid=3761] vsize: 703452 Current children cumulated CPU time (s) 371.49 Current children cumulated vsize (Kb) 705580 [startup+390.027 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220785 0 3 0 37286 843 0 0 25 0 1 0 1793636837 732491776 178534 4294967295 134512640 135167914 3221224448 3221223200 134693573 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 178831 178534 162 162 0 178669 0 [pid=3761] vsize: 715324 Current children cumulated CPU time (s) 381.31 Current children cumulated vsize (Kb) 717452 [startup+400.027 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 38278 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221222984 134846907 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 391.31 Current children cumulated vsize (Kb) 548724 [startup+410.028 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 39278 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221222984 134846907 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 401.31 Current children cumulated vsize (Kb) 548724 [startup+420.029 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 40278 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219440 134844713 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 411.31 Current children cumulated vsize (Kb) 548724 [startup+430.03 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 41279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219712 134630858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 421.32 Current children cumulated vsize (Kb) 548724 [startup+440.031 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 42279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220400 134849096 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 431.32 Current children cumulated vsize (Kb) 548724 [startup+450.031 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 43279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219804 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 441.32 Current children cumulated vsize (Kb) 548724 [startup+460.031 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 44279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219452 134723267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 451.32 Current children cumulated vsize (Kb) 548724 [startup+470.031 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 45279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220224 134694351 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 461.32 Current children cumulated vsize (Kb) 548724 [startup+480.031 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 46279 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219716 134629088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 471.32 Current children cumulated vsize (Kb) 548724 [startup+490.032 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 47280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220432 134844647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 481.33 Current children cumulated vsize (Kb) 548724 [startup+500.033 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 48280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219792 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 491.33 Current children cumulated vsize (Kb) 548724 [startup+510.033 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 49280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219692 134722542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 501.33 Current children cumulated vsize (Kb) 548724 [startup+520.034 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 50280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219776 134845921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 511.33 Current children cumulated vsize (Kb) 548724 [startup+530.035 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 51280 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220144 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 521.33 Current children cumulated vsize (Kb) 548724 [startup+540.035 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 52281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219896 134629265 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 531.34 Current children cumulated vsize (Kb) 548724 [startup+550.036 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 53281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219532 134694320 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 541.34 Current children cumulated vsize (Kb) 548724 [startup+560.037 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 54281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219856 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 551.34 Current children cumulated vsize (Kb) 548724 [startup+570.037 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 55281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220368 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 561.34 Current children cumulated vsize (Kb) 548724 [startup+580.038 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 56281 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219616 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 571.34 Current children cumulated vsize (Kb) 548724 [startup+590.038 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 57282 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220560 134694377 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 581.35 Current children cumulated vsize (Kb) 548724 [startup+600.039 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 58282 851 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220220 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 591.35 Current children cumulated vsize (Kb) 548724 [startup+610.04 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 59282 852 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220528 134720503 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 601.36 Current children cumulated vsize (Kb) 548724 [startup+620.04 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 60281 852 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219836 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 611.35 Current children cumulated vsize (Kb) 548724 [startup+630.041 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 61281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220144 134844691 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 621.36 Current children cumulated vsize (Kb) 548724 [startup+640.042 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 62281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219392 134844668 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 631.36 Current children cumulated vsize (Kb) 548724 [startup+650.041 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 63281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220400 134694351 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 641.36 Current children cumulated vsize (Kb) 548724 [startup+660.042 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 64281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220496 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 651.36 Current children cumulated vsize (Kb) 548724 [startup+670.043 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 65281 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219656 134844633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 661.36 Current children cumulated vsize (Kb) 548724 [startup+680.043 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 66282 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219904 134845933 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 671.37 Current children cumulated vsize (Kb) 548724 [startup+690.044 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 67282 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219692 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 681.37 Current children cumulated vsize (Kb) 548724 [startup+700.044 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 68282 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219712 134628817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 691.37 Current children cumulated vsize (Kb) 548724 [startup+710.045 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 69282 853 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219676 134722542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 701.37 Current children cumulated vsize (Kb) 548724 [startup+720.045 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 70282 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220332 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 711.38 Current children cumulated vsize (Kb) 548724 [startup+730.045 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 71282 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220960 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 721.38 Current children cumulated vsize (Kb) 548724 [startup+740.046 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 72283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220752 134694329 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 731.39 Current children cumulated vsize (Kb) 548724 [startup+750.046 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 73283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220672 134844713 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 741.39 Current children cumulated vsize (Kb) 548724 [startup+760.046 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 74283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219452 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 751.39 Current children cumulated vsize (Kb) 548724 [startup+770.046 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 75283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220624 134844703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 761.39 Current children cumulated vsize (Kb) 548724 [startup+780.047 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 76283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219744 134844731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 771.39 Current children cumulated vsize (Kb) 548724 [startup+790.047 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 77284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220844 134718504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 781.4 Current children cumulated vsize (Kb) 548724 [startup+800.048 s] Raw data (loadavg): 1.00 1.00 0.89 3/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 78283 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220848 134844700 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 791.39 Current children cumulated vsize (Kb) 548724 [startup+810.048 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 79284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219296 134718497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 801.4 Current children cumulated vsize (Kb) 548724 [startup+820.048 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 80284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221222284 134845882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 811.4 Current children cumulated vsize (Kb) 548724 [startup+830.049 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 81284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220368 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 821.4 Current children cumulated vsize (Kb) 548724 [startup+840.049 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 82284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220412 134522184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 831.4 Current children cumulated vsize (Kb) 548724 [startup+850.049 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 83284 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221932 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 841.4 Current children cumulated vsize (Kb) 548724 [startup+860.05 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 84285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220496 134696321 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 851.41 Current children cumulated vsize (Kb) 548724 [startup+870.05 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 85285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219616 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 861.41 Current children cumulated vsize (Kb) 548724 [startup+880.051 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 86285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220412 134849056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 871.41 Current children cumulated vsize (Kb) 548724 [startup+890.052 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 87285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219952 134845903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 881.41 Current children cumulated vsize (Kb) 548724 [startup+900.052 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 88285 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220208 134694517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 891.41 Current children cumulated vsize (Kb) 548724 [startup+910.053 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 89286 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219628 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 901.42 Current children cumulated vsize (Kb) 548724 [startup+920.053 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 90286 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221808 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 911.42 Current children cumulated vsize (Kb) 548724 [startup+930.054 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 91286 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220144 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 921.42 Current children cumulated vsize (Kb) 548724 [startup+940.055 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 92286 854 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220400 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 931.42 Current children cumulated vsize (Kb) 548724 [startup+950.054 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 93286 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221176 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 941.43 Current children cumulated vsize (Kb) 548724 [startup+960.055 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 94287 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220756 134843000 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 951.44 Current children cumulated vsize (Kb) 548724 [startup+970.056 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 95287 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221024 134843036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 961.44 Current children cumulated vsize (Kb) 548724 [startup+980.056 s] Raw data (loadavg): 1.00 1.00 0.90 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 96287 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221221104 134849102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 971.44 Current children cumulated vsize (Kb) 548724 [startup+990.057 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 97287 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220048 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 981.44 Current children cumulated vsize (Kb) 548724 [startup+1000.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 98288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220960 134630883 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 991.45 Current children cumulated vsize (Kb) 548724 [startup+1010.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 99288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220912 134694517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1001.45 Current children cumulated vsize (Kb) 548724 [startup+1020.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 100288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220188 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1011.45 Current children cumulated vsize (Kb) 548724 [startup+1030.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 101288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220380 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1021.45 Current children cumulated vsize (Kb) 548724 [startup+1040.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 102288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219872 134693570 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1031.45 Current children cumulated vsize (Kb) 548724 [startup+1050.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 103288 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220760 134694481 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1041.45 Current children cumulated vsize (Kb) 548724 [startup+1060.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 104289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220384 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1051.46 Current children cumulated vsize (Kb) 548724 [startup+1070.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 105289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219792 134844718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1061.46 Current children cumulated vsize (Kb) 548724 [startup+1080.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 106289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221219984 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1071.46 Current children cumulated vsize (Kb) 548724 [startup+1090.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 107289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220672 134844718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1081.46 Current children cumulated vsize (Kb) 548724 [startup+1100.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 108289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220316 134844675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1091.46 Current children cumulated vsize (Kb) 548724 [startup+1110.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 109289 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220904 134845877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1101.46 Current children cumulated vsize (Kb) 548724 [startup+1120.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 110290 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220764 134696560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1111.47 Current children cumulated vsize (Kb) 548724 [startup+1130.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220786 0 3 0 111290 855 0 0 25 0 1 0 1793636837 559714304 136353 4294967295 134512640 135167914 3221224448 3221220892 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136649 136353 162 162 0 136487 0 [pid=3761] vsize: 546596 Current children cumulated CPU time (s) 1121.47 Current children cumulated vsize (Kb) 548724 [startup+1140.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 112290 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221196384 134847159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0 [pid=3761] vsize: 545116 Current children cumulated CPU time (s) 1131.47 Current children cumulated vsize (Kb) 547244 [startup+1150.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 113290 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221196064 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0 [pid=3761] vsize: 545116 Current children cumulated CPU time (s) 1141.47 Current children cumulated vsize (Kb) 547244 [startup+1160.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 114290 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221194528 134691221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0 [pid=3761] vsize: 545116 Current children cumulated CPU time (s) 1151.47 Current children cumulated vsize (Kb) 547244 [startup+1170.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 115291 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221194576 134843030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0 [pid=3761] vsize: 545116 Current children cumulated CPU time (s) 1161.48 Current children cumulated vsize (Kb) 547244 [startup+1180.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 116291 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221194332 134722208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0 [pid=3761] vsize: 545116 Current children cumulated CPU time (s) 1171.48 Current children cumulated vsize (Kb) 547244 [startup+1190.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 117291 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221195840 134845921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0 [pid=3761] vsize: 545116 Current children cumulated CPU time (s) 1181.48 Current children cumulated vsize (Kb) 547244 [startup+1200.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 118291 855 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221194048 134624188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0 [pid=3761] vsize: 545116 Current children cumulated CPU time (s) 1191.48 Current children cumulated vsize (Kb) 547244 [startup+1210.06 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 119291 856 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221195008 134624957 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0 [pid=3761] vsize: 545116 Current children cumulated CPU time (s) 1201.49 Current children cumulated vsize (Kb) 547244 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 1.00 1.00 0.91 2/57 3761 Raw data (/proc/3756/stat): 3756 (minisat+_script) S 3755 3756 15400 0 -1 0 314 332 0 0 0 1 0 1 16 0 1 0 1793636831 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3756/statm): 532 234 485 147 0 385 0 [pid=3756] vsize: 2128 Raw data (/proc/3761/stat): 3761 (minisat+_bignum) R 3756 3756 15400 0 -1 0 220790 0 3 0 119291 856 0 0 25 0 1 0 1793636837 558198784 135987 4294967295 134512640 135167914 3221224448 3221195040 134625423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3761/statm): 136279 135987 162 162 0 136117 0 [pid=3761] vsize: 545116 Current children cumulated CPU time (s) 1201.49 Current children cumulated vsize (Kb) 547244 Sending SIGTERM to -3756 Sleeping 2 seconds One traced child (pid=3756) ended because it received signal 15 (SIGTERM) One traced child (pid=3761) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.32 CPU time (s): 1201.73 CPU user time (s): 1192.91 CPU system time (s): 8.81466 CPU usage (%): 99.2902 Max. virtual memory (cumulated for all children) (Kb): 772196
ERROR: no interpretation found !