Name | submitted/aloul/FPGA_SAT05/normalized-chnl15_16_pb.cnf.cr.opb |
MD5SUM | 3f8902c4e8af50006f671e2bddb3e9aa |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 17 |
Number of bits of the biggest sum of numbers | 5 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.017996 |
Number of variables | 480 |
Total number of constraints | 62 |
Number of constraints which are clauses | 32 |
Number of constraints which are cardinality constraints (but not clauses) | 30 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 15 |
Maximum length of a constraint | 16 |
LAUNCH ON wulflinc1 THE 2005-09-18 12:23:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2347 boxname=wulflinc1 idbench=3 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3f8902c4e8af50006f671e2bddb3e9aa /oldhome/oroussel/tmp/wulflinc1/normalized-chnl15_16_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-chnl15_16_pb.cnf.cr.opb IDLAUNCH: 2347 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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: 907324 kB Buffers: 37160 kB Cached: 60396 kB SwapCached: 908 kB Active: 83108 kB Inactive: 17292 kB HighTotal: 131008 kB HighFree: 74480 kB LowTotal: 903652 kB LowFree: 832844 kB SwapTotal: 2097136 kB SwapFree: 2095620 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5992 kB Slab: 21132 kB Committed_AS: 93132 kB PageTables: 344 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 12:44:02 (client local time) WITH STATUS 0 IN 1209.99 SECONDS stats: 2347 7 1209.99 0
c Parsing PB file... c Converting 62 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................ c ---[ 29]---> BDD-cost: 29 c ---[ 28]---> BDD-cost: 29 c ---[ 27]---> BDD-cost: 29 c ---[ 26]---> BDD-cost: 29 c ---[ 25]---> BDD-cost: 29 c ---[ 24]---> BDD-cost: 29 c ---[ 23]---> BDD-cost: 29 c ---[ 22]---> BDD-cost: 29 c ---[ 21]---> BDD-cost: 29 c ---[ 20]---> BDD-cost: 29 c ---[ 19]---> BDD-cost: 29 c ---[ 18]---> BDD-cost: 29 c ---[ 17]---> BDD-cost: 29 c ---[ 16]---> BDD-cost: 29 c ---[ 15]---> BDD-cost: 29 c ---[ 14]---> BDD-cost: 29 c ---[ 13]---> BDD-cost: 29 c ---[ 12]---> BDD-cost: 29 c ---[ 11]---> BDD-cost: 29 c ---[ 10]---> BDD-cost: 29 c ---[ 9]---> BDD-cost: 29 c ---[ 8]---> BDD-cost: 29 c ---[ 7]---> BDD-cost: 29 c ---[ 6]---> BDD-cost: 29 c ---[ 5]---> BDD-cost: 29 c ---[ 4]---> BDD-cost: 29 c ---[ 3]---> BDD-cost: 29 c ---[ 2]---> BDD-cost: 29 c ---[ 1]---> BDD-cost: 29 c ---[ 0]---> BDD-cost: 29 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 2162 6030 | 720 0 0 nan | 0.000 % | c | 102 | 2162 6030 | 792 102 5686 55.7 | 2.222 % | c | 252 | 2162 6030 | 871 252 14004 55.6 | 2.222 % | c | 478 | 2162 6030 | 958 478 28490 59.6 | 2.222 % | c | 815 | 2162 6030 | 1054 815 57080 70.0 | 2.222 % | c | 1322 | 2162 6030 | 1159 1322 104342 78.9 | 2.222 % | c | 2084 | 2162 6030 | 1275 1423 130456 91.7 | 2.222 % | c | 3226 | 2162 6030 | 1403 1038 95866 92.4 | 2.222 % | c | 4934 | 2162 6030 | 1543 1033 102989 99.7 | 2.222 % | c | 7499 | 2162 6030 | 1697 1732 186615 107.7 | 2.222 % | c | 11345 | 2162 6030 | 1867 1717 162221 94.5 | 2.222 % | c | 17111 | 2162 6030 | 2054 1970 199253 101.1 | 2.222 % | c | 25760 | 2162 6030 | 2259 2320 271642 117.1 | 2.222 % | c | 38735 | 2162 6030 | 2485 2566 270521 105.4 | 2.222 % | c | 58199 | 2162 6030 | 2734 2477 258968 104.5 | 2.222 % | c | 87394 | 2162 6030 | 3007 2810 295638 105.2 | 2.222 % | c | 131184 | 2162 6030 | 3308 1846 187402 101.5 | 2.222 % | c | 196869 | 2162 6030 | 3639 3043 323650 106.4 | 2.222 % | c | 295396 | 2162 6030 | 4003 3086 314350 101.9 | 2.222 % | c | 443187 | 2162 6030 | 4403 2851 287482 100.8 | 2.222 % | c | 664871 | 2162 6030 | 4843 3470 330999 95.4 | 2.222 % | c | 997401 | 2162 6030 | 5328 4395 477257 108.6 | 2.222 % | c | 1496194 | 2162 6030 | 5860 4647 485933 104.6 | 2.222 % |
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/21538/stat): 21538 (minisat+_script) R 21537 21538 17733 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1726145431 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/21538/statm): 174 3 169 147 0 27 0 [pid=21538] 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=21539 New process pid=21540 New process pid=21541 execve syscall for /bin/sed executable One traced child (pid=21540) 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=21541) exited with status: 0 One traced child (pid=21539) exited with status: 0 New process pid=21542 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-chnl15_16_pb.cnf.cr.opb [startup+10.0047 s] Raw data (loadavg): 0.72 0.91 0.93 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 636 0 2 0 983 2 0 0 25 0 1 0 1726145436 2891776 625 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 706 625 145 145 0 561 0 [pid=21542] vsize: 2824 Current children cumulated CPU time (s) 9.86 Current children cumulated vsize (Kb) 4948 [startup+20.0065 s] Raw data (loadavg): 0.76 0.91 0.93 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 706 0 2 0 1982 3 0 0 25 0 1 0 1726145436 3178496 695 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 776 695 145 145 0 631 0 [pid=21542] vsize: 3104 Current children cumulated CPU time (s) 19.86 Current children cumulated vsize (Kb) 5228 [startup+30.0073 s] Raw data (loadavg): 0.80 0.91 0.93 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 770 0 2 0 2981 3 0 0 25 0 1 0 1726145436 3440640 759 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 840 759 145 145 0 695 0 [pid=21542] vsize: 3360 Current children cumulated CPU time (s) 29.85 Current children cumulated vsize (Kb) 5484 [startup+40.0071 s] Raw data (loadavg): 0.83 0.91 0.93 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 813 0 2 0 3980 4 0 0 25 0 1 0 1726145436 3616768 802 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 883 802 145 145 0 738 0 [pid=21542] vsize: 3532 Current children cumulated CPU time (s) 39.85 Current children cumulated vsize (Kb) 5656 [startup+50.0089 s] Raw data (loadavg): 1.01 0.95 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 841 0 2 0 4979 5 0 0 25 0 1 0 1726145436 3731456 830 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 911 830 145 145 0 766 0 [pid=21542] vsize: 3644 Current children cumulated CPU time (s) 49.85 Current children cumulated vsize (Kb) 5768 [startup+60.0097 s] Raw data (loadavg): 1.01 0.95 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 860 0 2 0 5979 5 0 0 25 0 1 0 1726145436 3809280 849 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 930 849 145 145 0 785 0 [pid=21542] vsize: 3720 Current children cumulated CPU time (s) 59.85 Current children cumulated vsize (Kb) 5844 [startup+70.0114 s] Raw data (loadavg): 1.00 0.95 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 860 0 2 0 6979 5 0 0 25 0 1 0 1726145436 3809280 849 4294967295 134512640 135094434 3221224432 3221222912 134780484 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 930 849 145 145 0 785 0 [pid=21542] vsize: 3720 Current children cumulated CPU time (s) 69.85 Current children cumulated vsize (Kb) 5844 [startup+80.0132 s] Raw data (loadavg): 1.00 0.95 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 948 0 2 0 7977 6 0 0 25 0 1 0 1726145436 4173824 937 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1019 937 145 145 0 874 0 [pid=21542] vsize: 4076 Current children cumulated CPU time (s) 79.84 Current children cumulated vsize (Kb) 6200 [startup+90.013 s] Raw data (loadavg): 1.00 0.95 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 968 0 2 0 8977 7 0 0 25 0 1 0 1726145436 4259840 957 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1040 957 145 145 0 895 0 [pid=21542] vsize: 4160 Current children cumulated CPU time (s) 89.85 Current children cumulated vsize (Kb) 6284 [startup+100.014 s] Raw data (loadavg): 1.00 0.95 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 977 0 2 0 9976 7 0 0 25 0 1 0 1726145436 4300800 966 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1050 966 145 145 0 905 0 [pid=21542] vsize: 4200 Current children cumulated CPU time (s) 99.84 Current children cumulated vsize (Kb) 6324 [startup+110.015 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 977 0 2 0 10976 7 0 0 25 0 1 0 1726145436 4300800 966 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1050 966 145 145 0 905 0 [pid=21542] vsize: 4200 Current children cumulated CPU time (s) 109.84 Current children cumulated vsize (Kb) 6324 [startup+120.016 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1000 0 2 0 11976 7 0 0 25 0 1 0 1726145436 4395008 989 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1073 989 145 145 0 928 0 [pid=21542] vsize: 4292 Current children cumulated CPU time (s) 119.84 Current children cumulated vsize (Kb) 6416 [startup+130.017 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1049 0 2 0 12975 8 0 0 25 0 1 0 1726145436 4603904 1038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1124 1038 145 145 0 979 0 [pid=21542] vsize: 4496 Current children cumulated CPU time (s) 129.84 Current children cumulated vsize (Kb) 6620 [startup+140.018 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1056 0 2 0 13975 8 0 0 25 0 1 0 1726145436 4632576 1045 4294967295 134512640 135094434 3221224432 3221223104 134555453 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1131 1045 145 145 0 986 0 [pid=21542] vsize: 4524 Current children cumulated CPU time (s) 139.84 Current children cumulated vsize (Kb) 6648 [startup+150.02 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1094 0 2 0 14974 8 0 0 25 0 1 0 1726145436 4804608 1083 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1173 1083 145 145 0 1028 0 [pid=21542] vsize: 4692 Current children cumulated CPU time (s) 149.83 Current children cumulated vsize (Kb) 6816 [startup+160.021 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1141 0 2 0 15975 8 0 0 25 0 1 0 1726145436 5009408 1130 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1223 1130 145 145 0 1078 0 [pid=21542] vsize: 4892 Current children cumulated CPU time (s) 159.84 Current children cumulated vsize (Kb) 7016 [startup+170.021 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1157 0 2 0 16974 8 0 0 25 0 1 0 1726145436 5091328 1146 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1243 1146 145 145 0 1098 0 [pid=21542] vsize: 4972 Current children cumulated CPU time (s) 169.83 Current children cumulated vsize (Kb) 7096 [startup+180.022 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1247 0 2 0 17973 9 0 0 25 0 1 0 1726145436 5459968 1236 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1333 1236 145 145 0 1188 0 [pid=21542] vsize: 5332 Current children cumulated CPU time (s) 179.83 Current children cumulated vsize (Kb) 7456 [startup+190.023 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1247 0 2 0 18973 9 0 0 25 0 1 0 1726145436 5459968 1236 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1333 1236 145 145 0 1188 0 [pid=21542] vsize: 5332 Current children cumulated CPU time (s) 189.83 Current children cumulated vsize (Kb) 7456 [startup+200.024 s] Raw data (loadavg): 1.00 0.96 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1258 0 2 0 19973 9 0 0 25 0 1 0 1726145436 5505024 1247 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1344 1247 145 145 0 1199 0 [pid=21542] vsize: 5376 Current children cumulated CPU time (s) 199.83 Current children cumulated vsize (Kb) 7500 [startup+210.023 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1278 0 2 0 20973 9 0 0 25 0 1 0 1726145436 5591040 1267 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1365 1267 145 145 0 1220 0 [pid=21542] vsize: 5460 Current children cumulated CPU time (s) 209.83 Current children cumulated vsize (Kb) 7584 [startup+220.024 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1301 0 2 0 21973 9 0 0 25 0 1 0 1726145436 5705728 1290 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1393 1290 145 145 0 1248 0 [pid=21542] vsize: 5572 Current children cumulated CPU time (s) 219.83 Current children cumulated vsize (Kb) 7696 [startup+230.025 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1302 0 2 0 22973 9 0 0 25 0 1 0 1726145436 5705728 1291 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1393 1291 145 145 0 1248 0 [pid=21542] vsize: 5572 Current children cumulated CPU time (s) 229.83 Current children cumulated vsize (Kb) 7696 [startup+240.025 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1302 0 2 0 23974 9 0 0 25 0 1 0 1726145436 5705728 1291 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1393 1291 145 145 0 1248 0 [pid=21542] vsize: 5572 Current children cumulated CPU time (s) 239.84 Current children cumulated vsize (Kb) 7696 [startup+250.026 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1306 0 2 0 24974 9 0 0 25 0 1 0 1726145436 5722112 1295 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1397 1295 145 145 0 1252 0 [pid=21542] vsize: 5588 Current children cumulated CPU time (s) 249.84 Current children cumulated vsize (Kb) 7712 [startup+260.026 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1391 0 2 0 25972 10 0 0 25 0 1 0 1726145436 6070272 1380 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1482 1380 145 145 0 1337 0 [pid=21542] vsize: 5928 Current children cumulated CPU time (s) 259.83 Current children cumulated vsize (Kb) 8052 [startup+270.027 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1408 0 2 0 26972 10 0 0 25 0 1 0 1726145436 6144000 1397 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1500 1397 145 145 0 1355 0 [pid=21542] vsize: 6000 Current children cumulated CPU time (s) 269.83 Current children cumulated vsize (Kb) 8124 [startup+280.028 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1409 0 2 0 27973 10 0 0 25 0 1 0 1726145436 6144000 1398 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1500 1398 145 145 0 1355 0 [pid=21542] vsize: 6000 Current children cumulated CPU time (s) 279.84 Current children cumulated vsize (Kb) 8124 [startup+290.029 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1431 0 2 0 28973 11 0 0 25 0 1 0 1726145436 6242304 1420 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1524 1420 145 145 0 1379 0 [pid=21542] vsize: 6096 Current children cumulated CPU time (s) 289.85 Current children cumulated vsize (Kb) 8220 [startup+300.03 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1473 0 2 0 29973 11 0 0 25 0 1 0 1726145436 6418432 1462 4294967295 134512640 135094434 3221224432 3221223104 134555413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1567 1462 145 145 0 1422 0 [pid=21542] vsize: 6268 Current children cumulated CPU time (s) 299.85 Current children cumulated vsize (Kb) 8392 [startup+310.029 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1480 0 2 0 30973 11 0 0 25 0 1 0 1726145436 6451200 1469 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1575 1469 145 145 0 1430 0 [pid=21542] vsize: 6300 Current children cumulated CPU time (s) 309.85 Current children cumulated vsize (Kb) 8424 [startup+320.03 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1481 0 2 0 31973 11 0 0 25 0 1 0 1726145436 6451200 1470 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1575 1470 145 145 0 1430 0 [pid=21542] vsize: 6300 Current children cumulated CPU time (s) 319.85 Current children cumulated vsize (Kb) 8424 [startup+330.031 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1481 0 2 0 32973 11 0 0 25 0 1 0 1726145436 6451200 1470 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1575 1470 145 145 0 1430 0 [pid=21542] vsize: 6300 Current children cumulated CPU time (s) 329.85 Current children cumulated vsize (Kb) 8424 [startup+340.031 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1491 0 2 0 33973 11 0 0 25 0 1 0 1726145436 6500352 1480 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1587 1480 145 145 0 1442 0 [pid=21542] vsize: 6348 Current children cumulated CPU time (s) 339.85 Current children cumulated vsize (Kb) 8472 [startup+350.032 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1512 0 2 0 34973 11 0 0 25 0 1 0 1726145436 6598656 1501 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1611 1501 145 145 0 1466 0 [pid=21542] vsize: 6444 Current children cumulated CPU time (s) 349.85 Current children cumulated vsize (Kb) 8568 [startup+360.032 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1512 0 2 0 35974 11 0 0 25 0 1 0 1726145436 6598656 1501 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1611 1501 145 145 0 1466 0 [pid=21542] vsize: 6444 Current children cumulated CPU time (s) 359.86 Current children cumulated vsize (Kb) 8568 [startup+370.033 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1525 0 2 0 36973 11 0 0 25 0 1 0 1726145436 6664192 1514 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1627 1514 145 145 0 1482 0 [pid=21542] vsize: 6508 Current children cumulated CPU time (s) 369.85 Current children cumulated vsize (Kb) 8632 [startup+380.034 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1525 0 2 0 37973 11 0 0 25 0 1 0 1726145436 6664192 1514 4294967295 134512640 135094434 3221224432 3221223104 134555753 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1627 1514 145 145 0 1482 0 [pid=21542] vsize: 6508 Current children cumulated CPU time (s) 379.85 Current children cumulated vsize (Kb) 8632 [startup+390.035 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1593 0 2 0 38972 11 0 0 25 0 1 0 1726145436 6942720 1582 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1695 1582 145 145 0 1550 0 [pid=21542] vsize: 6780 Current children cumulated CPU time (s) 389.84 Current children cumulated vsize (Kb) 8904 [startup+400.036 s] Raw data (loadavg): 1.00 0.97 0.94 1/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) T 21538 21538 17733 0 -1 0 1615 0 2 0 39972 12 0 0 25 0 1 0 1726145436 7032832 1604 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1717 1604 145 145 0 1572 0 [pid=21542] vsize: 6868 Current children cumulated CPU time (s) 399.85 Current children cumulated vsize (Kb) 8992 [startup+410.035 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1641 0 2 0 40972 12 0 0 25 0 1 0 1726145436 7139328 1630 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1743 1630 145 145 0 1598 0 [pid=21542] vsize: 6972 Current children cumulated CPU time (s) 409.85 Current children cumulated vsize (Kb) 9096 [startup+420.036 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1655 0 2 0 41972 12 0 0 25 0 1 0 1726145436 7192576 1644 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1756 1644 145 145 0 1611 0 [pid=21542] vsize: 7024 Current children cumulated CPU time (s) 419.85 Current children cumulated vsize (Kb) 9148 [startup+430.037 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1655 0 2 0 42972 12 0 0 25 0 1 0 1726145436 7192576 1644 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1756 1644 145 145 0 1611 0 [pid=21542] vsize: 7024 Current children cumulated CPU time (s) 429.85 Current children cumulated vsize (Kb) 9148 [startup+440.038 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1656 0 2 0 43972 12 0 0 25 0 1 0 1726145436 7192576 1645 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1756 1645 145 145 0 1611 0 [pid=21542] vsize: 7024 Current children cumulated CPU time (s) 439.85 Current children cumulated vsize (Kb) 9148 [startup+450.038 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1668 0 2 0 44973 12 0 0 25 0 1 0 1726145436 7245824 1657 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1769 1657 145 145 0 1624 0 [pid=21542] vsize: 7076 Current children cumulated CPU time (s) 449.86 Current children cumulated vsize (Kb) 9200 [startup+460.039 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1682 0 2 0 45972 12 0 0 25 0 1 0 1726145436 7307264 1671 4294967295 134512640 135094434 3221224432 3221223024 134556793 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1784 1671 145 145 0 1639 0 [pid=21542] vsize: 7136 Current children cumulated CPU time (s) 459.85 Current children cumulated vsize (Kb) 9260 [startup+470.04 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1696 0 2 0 46973 12 0 0 25 0 1 0 1726145436 7368704 1685 4294967295 134512640 135094434 3221224432 3221223104 134555666 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1799 1685 145 145 0 1654 0 [pid=21542] vsize: 7196 Current children cumulated CPU time (s) 469.86 Current children cumulated vsize (Kb) 9320 [startup+480.041 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1700 0 2 0 47973 12 0 0 25 0 1 0 1726145436 7385088 1689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1803 1689 145 145 0 1658 0 [pid=21542] vsize: 7212 Current children cumulated CPU time (s) 479.86 Current children cumulated vsize (Kb) 9336 [startup+490.041 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1704 0 2 0 48973 12 0 0 25 0 1 0 1726145436 7401472 1693 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1807 1693 145 145 0 1662 0 [pid=21542] vsize: 7228 Current children cumulated CPU time (s) 489.86 Current children cumulated vsize (Kb) 9352 [startup+500.041 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1707 0 2 0 49973 12 0 0 25 0 1 0 1726145436 7401472 1696 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1807 1696 145 145 0 1662 0 [pid=21542] vsize: 7228 Current children cumulated CPU time (s) 499.86 Current children cumulated vsize (Kb) 9352 [startup+510.041 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1716 0 2 0 50973 12 0 0 25 0 1 0 1726145436 7438336 1705 4294967295 134512640 135094434 3221224432 3221223104 134556465 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1816 1705 145 145 0 1671 0 [pid=21542] vsize: 7264 Current children cumulated CPU time (s) 509.86 Current children cumulated vsize (Kb) 9388 [startup+520.042 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1720 0 2 0 51973 12 0 0 25 0 1 0 1726145436 7454720 1709 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1820 1709 145 145 0 1675 0 [pid=21542] vsize: 7280 Current children cumulated CPU time (s) 519.86 Current children cumulated vsize (Kb) 9404 [startup+530.043 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1727 0 2 0 52973 12 0 0 25 0 1 0 1726145436 7483392 1716 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1827 1716 145 145 0 1682 0 [pid=21542] vsize: 7308 Current children cumulated CPU time (s) 529.86 Current children cumulated vsize (Kb) 9432 [startup+540.043 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1735 0 2 0 53973 12 0 0 25 0 1 0 1726145436 7516160 1724 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1835 1724 145 145 0 1690 0 [pid=21542] vsize: 7340 Current children cumulated CPU time (s) 539.86 Current children cumulated vsize (Kb) 9464 [startup+550.043 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1736 0 2 0 54974 12 0 0 25 0 1 0 1726145436 7516160 1725 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1835 1725 145 145 0 1690 0 [pid=21542] vsize: 7340 Current children cumulated CPU time (s) 549.87 Current children cumulated vsize (Kb) 9464 [startup+560.044 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1746 0 2 0 55974 12 0 0 25 0 1 0 1726145436 7557120 1735 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1845 1735 145 145 0 1700 0 [pid=21542] vsize: 7380 Current children cumulated CPU time (s) 559.87 Current children cumulated vsize (Kb) 9504 [startup+570.045 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1748 0 2 0 56974 13 0 0 25 0 1 0 1726145436 7565312 1737 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1847 1737 145 145 0 1702 0 [pid=21542] vsize: 7388 Current children cumulated CPU time (s) 569.88 Current children cumulated vsize (Kb) 9512 [startup+580.046 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1763 0 2 0 57974 13 0 0 25 0 1 0 1726145436 7626752 1752 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1862 1752 145 145 0 1717 0 [pid=21542] vsize: 7448 Current children cumulated CPU time (s) 579.88 Current children cumulated vsize (Kb) 9572 [startup+590.046 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1780 0 2 0 58973 13 0 0 25 0 1 0 1726145436 7692288 1769 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 1878 1769 145 145 0 1733 0 [pid=21542] vsize: 7512 Current children cumulated CPU time (s) 589.87 Current children cumulated vsize (Kb) 9636 [startup+600.047 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1832 0 2 0 59972 14 0 0 25 0 1 0 1726145436 7905280 1821 4294967295 134512640 135094434 3221224432 3221222896 134780635 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1930 1821 145 145 0 1785 0 [pid=21542] vsize: 7720 Current children cumulated CPU time (s) 599.87 Current children cumulated vsize (Kb) 9844 [startup+610.047 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1839 0 2 0 60973 14 0 0 25 0 1 0 1726145436 7938048 1828 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1938 1828 145 145 0 1793 0 [pid=21542] vsize: 7752 Current children cumulated CPU time (s) 609.88 Current children cumulated vsize (Kb) 9876 [startup+620.048 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1852 0 2 0 61973 14 0 0 25 0 1 0 1726145436 7991296 1841 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1951 1841 145 145 0 1806 0 [pid=21542] vsize: 7804 Current children cumulated CPU time (s) 619.88 Current children cumulated vsize (Kb) 9928 [startup+630.049 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1859 0 2 0 62972 15 0 0 25 0 1 0 1726145436 8024064 1848 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1959 1848 145 145 0 1814 0 [pid=21542] vsize: 7836 Current children cumulated CPU time (s) 629.88 Current children cumulated vsize (Kb) 9960 [startup+640.049 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1859 0 2 0 63972 15 0 0 25 0 1 0 1726145436 8024064 1848 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1959 1848 145 145 0 1814 0 [pid=21542] vsize: 7836 Current children cumulated CPU time (s) 639.88 Current children cumulated vsize (Kb) 9960 [startup+650.05 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1859 0 2 0 64972 15 0 0 25 0 1 0 1726145436 8024064 1848 4294967295 134512640 135094434 3221224432 3221221728 134562794 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1959 1848 145 145 0 1814 0 [pid=21542] vsize: 7836 Current children cumulated CPU time (s) 649.88 Current children cumulated vsize (Kb) 9960 [startup+660.05 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1869 0 2 0 65972 15 0 0 25 0 1 0 1726145436 8073216 1858 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1971 1858 145 145 0 1826 0 [pid=21542] vsize: 7884 Current children cumulated CPU time (s) 659.88 Current children cumulated vsize (Kb) 10008 [startup+670.051 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1870 0 2 0 66972 16 0 0 25 0 1 0 1726145436 8073216 1859 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1971 1859 145 145 0 1826 0 [pid=21542] vsize: 7884 Current children cumulated CPU time (s) 669.89 Current children cumulated vsize (Kb) 10008 [startup+680.052 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1881 0 2 0 67972 16 0 0 25 0 1 0 1726145436 8122368 1870 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1983 1870 145 145 0 1838 0 [pid=21542] vsize: 7932 Current children cumulated CPU time (s) 679.89 Current children cumulated vsize (Kb) 10056 [startup+690.051 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1884 0 2 0 68972 16 0 0 25 0 1 0 1726145436 8138752 1873 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1987 1873 145 145 0 1842 0 [pid=21542] vsize: 7948 Current children cumulated CPU time (s) 689.89 Current children cumulated vsize (Kb) 10072 [startup+700.052 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1892 0 2 0 69972 16 0 0 25 0 1 0 1726145436 8171520 1881 4294967295 134512640 135094434 3221224432 3221223104 134556471 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1995 1881 145 145 0 1850 0 [pid=21542] vsize: 7980 Current children cumulated CPU time (s) 699.89 Current children cumulated vsize (Kb) 10104 [startup+710.053 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1893 0 2 0 70972 16 0 0 25 0 1 0 1726145436 8171520 1882 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1995 1882 145 145 0 1850 0 [pid=21542] vsize: 7980 Current children cumulated CPU time (s) 709.89 Current children cumulated vsize (Kb) 10104 [startup+720.054 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1897 0 2 0 71973 16 0 0 25 0 1 0 1726145436 8187904 1886 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1999 1886 145 145 0 1854 0 [pid=21542] vsize: 7996 Current children cumulated CPU time (s) 719.9 Current children cumulated vsize (Kb) 10120 [startup+730.055 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1899 0 2 0 72973 16 0 0 25 0 1 0 1726145436 8187904 1888 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1999 1888 145 145 0 1854 0 [pid=21542] vsize: 7996 Current children cumulated CPU time (s) 729.9 Current children cumulated vsize (Kb) 10120 [startup+740.055 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1899 0 2 0 73973 16 0 0 25 0 1 0 1726145436 8187904 1888 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1999 1888 145 145 0 1854 0 [pid=21542] vsize: 7996 Current children cumulated CPU time (s) 739.9 Current children cumulated vsize (Kb) 10120 [startup+750.056 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1900 0 2 0 74973 16 0 0 25 0 1 0 1726145436 8187904 1889 4294967295 134512640 135094434 3221224432 3221223096 134556595 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 1999 1889 145 145 0 1854 0 [pid=21542] vsize: 7996 Current children cumulated CPU time (s) 749.9 Current children cumulated vsize (Kb) 10120 [startup+760.056 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1947 0 2 0 75973 16 0 0 25 0 1 0 1726145436 8372224 1936 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2044 1936 145 145 0 1899 0 [pid=21542] vsize: 8176 Current children cumulated CPU time (s) 759.9 Current children cumulated vsize (Kb) 10300 [startup+770.057 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1947 0 2 0 76973 17 0 0 25 0 1 0 1726145436 8372224 1936 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2044 1936 145 145 0 1899 0 [pid=21542] vsize: 8176 Current children cumulated CPU time (s) 769.91 Current children cumulated vsize (Kb) 10300 [startup+780.058 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1949 0 2 0 77973 17 0 0 25 0 1 0 1726145436 8372224 1938 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2044 1938 145 145 0 1899 0 [pid=21542] vsize: 8176 Current children cumulated CPU time (s) 779.91 Current children cumulated vsize (Kb) 10300 [startup+790.057 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1949 0 2 0 78973 17 0 0 25 0 1 0 1726145436 8372224 1938 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2044 1938 145 145 0 1899 0 [pid=21542] vsize: 8176 Current children cumulated CPU time (s) 789.91 Current children cumulated vsize (Kb) 10300 [startup+800.058 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1953 0 2 0 79974 17 0 0 25 0 1 0 1726145436 8384512 1942 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2047 1942 145 145 0 1902 0 [pid=21542] vsize: 8188 Current children cumulated CPU time (s) 799.92 Current children cumulated vsize (Kb) 10312 [startup+810.059 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1953 0 2 0 80973 17 0 0 25 0 1 0 1726145436 8384512 1942 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2047 1942 145 145 0 1902 0 [pid=21542] vsize: 8188 Current children cumulated CPU time (s) 809.91 Current children cumulated vsize (Kb) 10312 [startup+820.06 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1954 0 2 0 81974 17 0 0 25 0 1 0 1726145436 8384512 1943 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2047 1943 145 145 0 1902 0 [pid=21542] vsize: 8188 Current children cumulated CPU time (s) 819.92 Current children cumulated vsize (Kb) 10312 [startup+830.061 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1954 0 2 0 82974 17 0 0 25 0 1 0 1726145436 8384512 1943 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2047 1943 145 145 0 1902 0 [pid=21542] vsize: 8188 Current children cumulated CPU time (s) 829.92 Current children cumulated vsize (Kb) 10312 [startup+840.061 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1954 0 2 0 83974 17 0 0 25 0 1 0 1726145436 8384512 1943 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2047 1943 145 145 0 1902 0 [pid=21542] vsize: 8188 Current children cumulated CPU time (s) 839.92 Current children cumulated vsize (Kb) 10312 [startup+850.062 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1955 0 2 0 84975 17 0 0 25 0 1 0 1726145436 8384512 1944 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2047 1944 145 145 0 1902 0 [pid=21542] vsize: 8188 Current children cumulated CPU time (s) 849.93 Current children cumulated vsize (Kb) 10312 [startup+860.063 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1955 0 2 0 85975 17 0 0 25 0 1 0 1726145436 8384512 1944 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2047 1944 145 145 0 1902 0 [pid=21542] vsize: 8188 Current children cumulated CPU time (s) 859.93 Current children cumulated vsize (Kb) 10312 [startup+870.064 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1964 0 2 0 86975 17 0 0 25 0 1 0 1726145436 8421376 1953 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2056 1953 145 145 0 1911 0 [pid=21542] vsize: 8224 Current children cumulated CPU time (s) 869.93 Current children cumulated vsize (Kb) 10348 [startup+880.064 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1964 0 2 0 87975 17 0 0 25 0 1 0 1726145436 8421376 1953 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2056 1953 145 145 0 1911 0 [pid=21542] vsize: 8224 Current children cumulated CPU time (s) 879.93 Current children cumulated vsize (Kb) 10348 [startup+890.064 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1964 0 2 0 88975 17 0 0 25 0 1 0 1726145436 8421376 1953 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2056 1953 145 145 0 1911 0 [pid=21542] vsize: 8224 Current children cumulated CPU time (s) 889.93 Current children cumulated vsize (Kb) 10348 [startup+900.065 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1964 0 2 0 89976 17 0 0 25 0 1 0 1726145436 8421376 1953 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2056 1953 145 145 0 1911 0 [pid=21542] vsize: 8224 Current children cumulated CPU time (s) 899.94 Current children cumulated vsize (Kb) 10348 [startup+910.066 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1991 0 2 0 90975 17 0 0 25 0 1 0 1726145436 8527872 1980 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2082 1980 145 145 0 1937 0 [pid=21542] vsize: 8328 Current children cumulated CPU time (s) 909.93 Current children cumulated vsize (Kb) 10452 [startup+920.067 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2072 0 2 0 91974 18 0 0 25 0 1 0 1726145436 8855552 2061 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 2162 2061 145 145 0 2017 0 [pid=21542] vsize: 8648 Current children cumulated CPU time (s) 919.93 Current children cumulated vsize (Kb) 10772 [startup+930.067 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2073 0 2 0 92973 19 0 0 25 0 1 0 1726145436 8859648 2062 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21542/statm): 2163 2062 145 145 0 2018 0 [pid=21542] vsize: 8652 Current children cumulated CPU time (s) 929.93 Current children cumulated vsize (Kb) 10776 [startup+940.068 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2106 0 2 0 93972 19 0 0 25 0 1 0 1726145436 8994816 2095 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2196 2095 145 145 0 2051 0 [pid=21542] vsize: 8784 Current children cumulated CPU time (s) 939.92 Current children cumulated vsize (Kb) 10908 [startup+950.069 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2106 0 2 0 94972 19 0 0 25 0 1 0 1726145436 8994816 2095 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2196 2095 145 145 0 2051 0 [pid=21542] vsize: 8784 Current children cumulated CPU time (s) 949.92 Current children cumulated vsize (Kb) 10908 [startup+960.069 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2106 0 2 0 95972 19 0 0 25 0 1 0 1726145436 8994816 2095 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2196 2095 145 145 0 2051 0 [pid=21542] vsize: 8784 Current children cumulated CPU time (s) 959.92 Current children cumulated vsize (Kb) 10908 [startup+970.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2106 0 2 0 96972 19 0 0 25 0 1 0 1726145436 8994816 2095 4294967295 134512640 135094434 3221224432 3221223024 134557221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2196 2095 145 145 0 2051 0 [pid=21542] vsize: 8784 Current children cumulated CPU time (s) 969.92 Current children cumulated vsize (Kb) 10908 [startup+980.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2108 0 2 0 97973 19 0 0 25 0 1 0 1726145436 8994816 2097 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2196 2097 145 145 0 2051 0 [pid=21542] vsize: 8784 Current children cumulated CPU time (s) 979.93 Current children cumulated vsize (Kb) 10908 [startup+990.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2108 0 2 0 98973 19 0 0 25 0 1 0 1726145436 8994816 2097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2196 2097 145 145 0 2051 0 [pid=21542] vsize: 8784 Current children cumulated CPU time (s) 989.93 Current children cumulated vsize (Kb) 10908 [startup+1000.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2109 0 2 0 99973 19 0 0 25 0 1 0 1726145436 8994816 2098 4294967295 134512640 135094434 3221224432 3221223088 134557771 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2196 2098 145 145 0 2051 0 [pid=21542] vsize: 8784 Current children cumulated CPU time (s) 999.93 Current children cumulated vsize (Kb) 10908 [startup+1010.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 100973 19 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0 [pid=21542] vsize: 8816 Current children cumulated CPU time (s) 1009.93 Current children cumulated vsize (Kb) 10940 [startup+1020.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 101973 19 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0 [pid=21542] vsize: 8816 Current children cumulated CPU time (s) 1019.93 Current children cumulated vsize (Kb) 10940 [startup+1030.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 102974 19 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0 [pid=21542] vsize: 8816 Current children cumulated CPU time (s) 1029.94 Current children cumulated vsize (Kb) 10940 [startup+1040.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 103974 20 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0 [pid=21542] vsize: 8816 Current children cumulated CPU time (s) 1039.95 Current children cumulated vsize (Kb) 10940 [startup+1050.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 104974 20 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0 [pid=21542] vsize: 8816 Current children cumulated CPU time (s) 1049.95 Current children cumulated vsize (Kb) 10940 [startup+1060.07 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 105974 20 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223120 134554751 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0 [pid=21542] vsize: 8816 Current children cumulated CPU time (s) 1059.95 Current children cumulated vsize (Kb) 10940 [startup+1070.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2115 0 2 0 106974 20 0 0 25 0 1 0 1726145436 9027584 2104 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2204 2104 145 145 0 2059 0 [pid=21542] vsize: 8816 Current children cumulated CPU time (s) 1069.95 Current children cumulated vsize (Kb) 10940 [startup+1080.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2115 0 2 0 107975 20 0 0 25 0 1 0 1726145436 9027584 2104 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2204 2104 145 145 0 2059 0 [pid=21542] vsize: 8816 Current children cumulated CPU time (s) 1079.96 Current children cumulated vsize (Kb) 10940 [startup+1090.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2125 0 2 0 108975 20 0 0 25 0 1 0 1726145436 9093120 2114 4294967295 134512640 135094434 3221224432 3221222912 134781511 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2220 2114 145 145 0 2075 0 [pid=21542] vsize: 8880 Current children cumulated CPU time (s) 1089.96 Current children cumulated vsize (Kb) 11004 [startup+1100.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 109975 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223024 134557389 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0 [pid=21542] vsize: 8912 Current children cumulated CPU time (s) 1099.96 Current children cumulated vsize (Kb) 11036 [startup+1110.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 110975 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0 [pid=21542] vsize: 8912 Current children cumulated CPU time (s) 1109.96 Current children cumulated vsize (Kb) 11036 [startup+1120.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 111975 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0 [pid=21542] vsize: 8912 Current children cumulated CPU time (s) 1119.96 Current children cumulated vsize (Kb) 11036 [startup+1130.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 112975 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0 [pid=21542] vsize: 8912 Current children cumulated CPU time (s) 1129.96 Current children cumulated vsize (Kb) 11036 [startup+1140.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 113976 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0 [pid=21542] vsize: 8912 Current children cumulated CPU time (s) 1139.97 Current children cumulated vsize (Kb) 11036 [startup+1150.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2135 0 2 0 114976 20 0 0 25 0 1 0 1726145436 9158656 2124 4294967295 134512640 135094434 3221224432 3221223024 134551897 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2236 2124 145 145 0 2091 0 [pid=21542] vsize: 8944 Current children cumulated CPU time (s) 1149.97 Current children cumulated vsize (Kb) 11068 [startup+1160.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 115976 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0 [pid=21542] vsize: 8976 Current children cumulated CPU time (s) 1159.97 Current children cumulated vsize (Kb) 11100 [startup+1170.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 116976 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223072 134562224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0 [pid=21542] vsize: 8976 Current children cumulated CPU time (s) 1169.97 Current children cumulated vsize (Kb) 11100 [startup+1180.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 117977 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0 [pid=21542] vsize: 8976 Current children cumulated CPU time (s) 1179.98 Current children cumulated vsize (Kb) 11100 [startup+1190.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 118977 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0 [pid=21542] vsize: 8976 Current children cumulated CPU time (s) 1189.98 Current children cumulated vsize (Kb) 11100 [startup+1200.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 119977 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0 [pid=21542] vsize: 8976 Current children cumulated CPU time (s) 1199.98 Current children cumulated vsize (Kb) 11100 [startup+1210.08 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2146 0 2 0 120977 20 0 0 25 0 1 0 1726145436 9224192 2135 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2252 2135 145 145 0 2107 0 [pid=21542] vsize: 9008 Current children cumulated CPU time (s) 1209.98 Current children cumulated vsize (Kb) 11132 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.00 0.97 0.94 2/58 21542 Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21538/statm): 531 226 485 147 0 384 0 [pid=21538] vsize: 2124 Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2146 0 2 0 120977 20 0 0 25 0 1 0 1726145436 9224192 2135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21542/statm): 2252 2135 145 145 0 2107 0 [pid=21542] vsize: 9008 Current children cumulated CPU time (s) 1209.98 Current children cumulated vsize (Kb) 11132 Sending SIGTERM to -21538 Sleeping 2 seconds One traced child (pid=21538) ended because it received signal 15 (SIGTERM) One traced child (pid=21542) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.09 CPU time (s): 1209.99 CPU user time (s): 1209.78 CPU system time (s): 0.210967 CPU usage (%): 99.9912 Max. virtual memory (cumulated for all children) (Kb): 11132
ERROR: no interpretation found !