Name | submitted/aloul/FPGA_SAT05/normalized-chnl35_40_pb.cnf.cr.opb |
MD5SUM | 85d4e2fa5fd7a61a85d3ecb1e311bddb |
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 | 41 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.092985 |
Number of variables | 2800 |
Total number of constraints | 150 |
Number of constraints which are clauses | 80 |
Number of constraints which are cardinality constraints (but not clauses) | 70 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 35 |
Maximum length of a constraint | 40 |
LAUNCH ON wulflinc29 THE 2005-09-18 12:25:32 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2357 boxname=wulflinc29 idbench=13 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 85d4e2fa5fd7a61a85d3ecb1e311bddb /oldhome/oroussel/tmp/wulflinc29/normalized-chnl35_40_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-chnl35_40_pb.cnf.cr.opb IDLAUNCH: 2357 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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 : 3 cpu MHz : 451.020 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: 937280 kB Buffers: 29688 kB Cached: 38132 kB SwapCached: 792 kB Active: 18484 kB Inactive: 52060 kB HighTotal: 131008 kB HighFree: 91532 kB LowTotal: 903652 kB LowFree: 845748 kB SwapTotal: 2097892 kB SwapFree: 2096664 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5736 kB Slab: 21004 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 12:45:42 (client local time) WITH STATUS 0 IN 1208.86 SECONDS stats: 2357 7 1208.86 0
c Parsing PB file... c Converting 150 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................................................................ c ---[ 69]---> BDD-cost: 77 c ---[ 68]---> BDD-cost: 77 c ---[ 67]---> BDD-cost: 77 c ---[ 66]---> BDD-cost: 77 c ---[ 65]---> BDD-cost: 77 c ---[ 64]---> BDD-cost: 77 c ---[ 63]---> BDD-cost: 77 c ---[ 62]---> BDD-cost: 77 c ---[ 61]---> BDD-cost: 77 c ---[ 60]---> BDD-cost: 77 c ---[ 59]---> BDD-cost: 77 c ---[ 58]---> BDD-cost: 77 c ---[ 57]---> BDD-cost: 77 c ---[ 56]---> BDD-cost: 77 c ---[ 55]---> BDD-cost: 77 c ---[ 54]---> BDD-cost: 77 c ---[ 53]---> BDD-cost: 77 c ---[ 52]---> BDD-cost: 77 c ---[ 51]---> BDD-cost: 77 c ---[ 50]---> BDD-cost: 77 c ---[ 49]---> BDD-cost: 77 c ---[ 48]---> BDD-cost: 77 c ---[ 47]---> BDD-cost: 77 c ---[ 46]---> BDD-cost: 77 c ---[ 45]---> BDD-cost: 77 c ---[ 44]---> BDD-cost: 77 c ---[ 43]---> BDD-cost: 77 c ---[ 42]---> BDD-cost: 77 c ---[ 41]---> BDD-cost: 77 c ---[ 40]---> BDD-cost: 77 c ---[ 39]---> BDD-cost: 77 c ---[ 38]---> BDD-cost: 77 c ---[ 37]---> BDD-cost: 77 c ---[ 36]---> BDD-cost: 77 c ---[ 35]---> BDD-cost: 77 c ---[ 34]---> BDD-cost: 77 c ---[ 33]---> BDD-cost: 77 c ---[ 32]---> BDD-cost: 77 c ---[ 31]---> BDD-cost: 77 c ---[ 30]---> BDD-cost: 77 c ---[ 29]---> BDD-cost: 77 c ---[ 28]---> BDD-cost: 77 c ---[ 27]---> BDD-cost: 77 c ---[ 26]---> BDD-cost: 77 c ---[ 25]---> BDD-cost: 77 c ---[ 24]---> BDD-cost: 77 c ---[ 23]---> BDD-cost: 77 c ---[ 22]---> BDD-cost: 77 c ---[ 21]---> BDD-cost: 77 c ---[ 20]---> BDD-cost: 77 c ---[ 19]---> BDD-cost: 77 c ---[ 18]---> BDD-cost: 77 c ---[ 17]---> BDD-cost: 77 c ---[ 16]---> BDD-cost: 77 c ---[ 15]---> BDD-cost: 77 c ---[ 14]---> BDD-cost: 77 c ---[ 13]---> BDD-cost: 77 c ---[ 12]---> BDD-cost: 77 c ---[ 11]---> BDD-cost: 77 c ---[ 10]---> BDD-cost: 77 c ---[ 9]---> BDD-cost: 77 c ---[ 8]---> BDD-cost: 77 c ---[ 7]---> BDD-cost: 77 c ---[ 6]---> BDD-cost: 77 c ---[ 5]---> BDD-cost: 77 c ---[ 4]---> BDD-cost: 77 c ---[ 3]---> BDD-cost: 77 c ---[ 2]---> BDD-cost: 77 c ---[ 1]---> BDD-cost: 77 c ---[ 0]---> BDD-cost: 77 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 13450 37590 | 4483 0 0 nan | 0.000 % | c | 105 | 13450 37590 | 4931 105 13790 131.3 | 0.855 % | c | 257 | 13450 37590 | 5424 257 35944 139.9 | 0.855 % | c | 482 | 13450 37590 | 5966 482 76174 158.0 | 0.855 % | c | 821 | 13450 37590 | 6563 821 135160 164.6 | 0.855 % | c | 1328 | 13450 37590 | 7219 1328 240970 181.5 | 0.855 % | c | 2087 | 13450 37590 | 7941 2087 409018 196.0 | 0.855 % | c | 3228 | 13450 37590 | 8736 3228 633540 196.3 | 0.855 % | c | 4936 | 13450 37590 | 9609 4936 1078151 218.4 | 0.855 % | c | 7501 | 13450 37590 | 10570 7501 1705202 227.3 | 0.855 % | c | 11350 | 13450 37590 | 11627 11350 2634616 232.1 | 0.855 % | c | 17117 | 13450 37590 | 12790 10826 2688531 248.3 | 0.855 % | c | 25768 | 13450 37590 | 14069 11465 2829373 246.8 | 0.855 % | c | 38743 | 13450 37590 | 15476 15813 5417503 342.6 | 0.855 % | c | 58205 | 13450 37590 | 17024 17974 5112296 284.4 | 0.855 % | c | 87402 | 13450 37590 | 18726 15116 4555281 301.4 | 0.855 % | c | 131192 | 13450 37590 | 20599 11825 3888204 328.8 | 0.855 % | c | 196876 | 13450 37590 | 22659 21414 6424762 300.0 | 0.855 % | c | 295403 | 13450 37590 | 24925 24280 8845785 364.3 | 0.855 % |
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/22174/stat): 22174 (minisat+_script) R 22173 22174 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841228190 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/22174/statm): 174 3 169 147 0 27 0 [pid=22174] 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=22175 New process pid=22176 New process pid=22177 execve syscall for /bin/sed executable One traced child (pid=22176) 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=22177) exited with status: 0 One traced child (pid=22175) exited with status: 0 New process pid=22178 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-chnl35_40_pb.cnf.cr.opb [startup+10.0054 s] Raw data (loadavg): 0.93 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 2595 0 2 0 961 11 0 0 25 0 1 0 1841228195 11272192 2580 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 2752 2580 145 145 0 2607 0 [pid=22178] vsize: 11008 Current children cumulated CPU time (s) 9.73 Current children cumulated vsize (Kb) 13132 [startup+20.0062 s] Raw data (loadavg): 0.94 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 3978 0 2 0 1940 20 0 0 25 0 1 0 1841228195 16961536 3963 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 4141 3963 145 145 0 3996 0 [pid=22178] vsize: 16564 Current children cumulated CPU time (s) 19.61 Current children cumulated vsize (Kb) 18688 [startup+30.008 s] Raw data (loadavg): 0.95 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 4018 0 2 0 2940 20 0 0 25 0 1 0 1841228195 17125376 4003 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 4181 4003 145 145 0 4036 0 [pid=22178] vsize: 16724 Current children cumulated CPU time (s) 29.61 Current children cumulated vsize (Kb) 18848 [startup+40.0088 s] Raw data (loadavg): 0.96 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 5073 0 2 0 3925 27 0 0 25 0 1 0 1841228195 21471232 5058 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 5242 5058 145 145 0 5097 0 [pid=22178] vsize: 20968 Current children cumulated CPU time (s) 39.53 Current children cumulated vsize (Kb) 23092 [startup+50.0096 s] Raw data (loadavg): 0.96 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 5241 0 2 0 4922 29 0 0 25 0 1 0 1841228195 22155264 5226 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 5409 5226 145 145 0 5264 0 [pid=22178] vsize: 21636 Current children cumulated CPU time (s) 49.52 Current children cumulated vsize (Kb) 23760 [startup+60.0103 s] Raw data (loadavg): 0.97 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 5700 0 2 0 5915 33 0 0 25 0 1 0 1841228195 24043520 5685 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 5870 5685 145 145 0 5725 0 [pid=22178] vsize: 23480 Current children cumulated CPU time (s) 59.49 Current children cumulated vsize (Kb) 25604 [startup+70.0111 s] Raw data (loadavg): 0.97 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6062 0 2 0 6910 34 0 0 25 0 1 0 1841228195 25579520 6047 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 6245 6047 145 145 0 6100 0 [pid=22178] vsize: 24980 Current children cumulated CPU time (s) 69.45 Current children cumulated vsize (Kb) 27104 [startup+80.0129 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6062 0 2 0 7911 34 0 0 25 0 1 0 1841228195 25579520 6047 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 6245 6047 145 145 0 6100 0 [pid=22178] vsize: 24980 Current children cumulated CPU time (s) 79.46 Current children cumulated vsize (Kb) 27104 [startup+90.0137 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6424 0 2 0 8906 36 0 0 25 0 1 0 1841228195 27090944 6409 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 6614 6409 145 145 0 6469 0 [pid=22178] vsize: 26456 Current children cumulated CPU time (s) 89.43 Current children cumulated vsize (Kb) 28580 [startup+100.014 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6921 0 2 0 9898 40 0 0 25 0 1 0 1841228195 29130752 6906 4294967295 134512640 135094434 3221224432 3221223104 134556507 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 7112 6906 145 145 0 6967 0 [pid=22178] vsize: 28448 Current children cumulated CPU time (s) 99.39 Current children cumulated vsize (Kb) 30572 [startup+110.015 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 6921 0 2 0 10898 40 0 0 25 0 1 0 1841228195 29130752 6906 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 7112 6906 145 145 0 6967 0 [pid=22178] vsize: 28448 Current children cumulated CPU time (s) 109.39 Current children cumulated vsize (Kb) 30572 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7708 0 2 0 11887 44 0 0 25 0 1 0 1841228195 32358400 7693 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 7900 7693 145 145 0 7755 0 [pid=22178] vsize: 31600 Current children cumulated CPU time (s) 119.32 Current children cumulated vsize (Kb) 33724 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7709 0 2 0 12887 44 0 0 25 0 1 0 1841228195 32358400 7694 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 7900 7694 145 145 0 7755 0 [pid=22178] vsize: 31600 Current children cumulated CPU time (s) 129.32 Current children cumulated vsize (Kb) 33724 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 13887 44 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0 [pid=22178] vsize: 31600 Current children cumulated CPU time (s) 139.32 Current children cumulated vsize (Kb) 33724 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 14888 44 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0 [pid=22178] vsize: 31600 Current children cumulated CPU time (s) 149.33 Current children cumulated vsize (Kb) 33724 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 15888 45 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0 [pid=22178] vsize: 31600 Current children cumulated CPU time (s) 159.34 Current children cumulated vsize (Kb) 33724 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 16888 45 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0 [pid=22178] vsize: 31600 Current children cumulated CPU time (s) 169.34 Current children cumulated vsize (Kb) 33724 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7710 0 2 0 17888 45 0 0 25 0 1 0 1841228195 32358400 7695 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 7900 7695 145 145 0 7755 0 [pid=22178] vsize: 31600 Current children cumulated CPU time (s) 179.34 Current children cumulated vsize (Kb) 33724 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 7847 0 2 0 18886 46 0 0 25 0 1 0 1841228195 32923648 7832 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 8038 7832 145 145 0 7893 0 [pid=22178] vsize: 32152 Current children cumulated CPU time (s) 189.33 Current children cumulated vsize (Kb) 34276 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8517 0 2 0 19876 50 0 0 25 0 1 0 1841228195 35688448 8502 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 8713 8502 145 145 0 8568 0 [pid=22178] vsize: 34852 Current children cumulated CPU time (s) 199.27 Current children cumulated vsize (Kb) 36976 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8517 0 2 0 20876 50 0 0 25 0 1 0 1841228195 35688448 8502 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 8713 8502 145 145 0 8568 0 [pid=22178] vsize: 34852 Current children cumulated CPU time (s) 209.27 Current children cumulated vsize (Kb) 36976 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8517 0 2 0 21876 50 0 0 25 0 1 0 1841228195 35688448 8502 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 8713 8502 145 145 0 8568 0 [pid=22178] vsize: 34852 Current children cumulated CPU time (s) 219.27 Current children cumulated vsize (Kb) 36976 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8531 0 2 0 22876 51 0 0 25 0 1 0 1841228195 35753984 8516 4294967295 134512640 135094434 3221224432 3221223024 134557494 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 8729 8516 145 145 0 8584 0 [pid=22178] vsize: 34916 Current children cumulated CPU time (s) 229.28 Current children cumulated vsize (Kb) 37040 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8794 0 2 0 23872 53 0 0 25 0 1 0 1841228195 36851712 8779 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 8997 8779 145 145 0 8852 0 [pid=22178] vsize: 35988 Current children cumulated CPU time (s) 239.26 Current children cumulated vsize (Kb) 38112 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8838 0 2 0 24871 53 0 0 25 0 1 0 1841228195 37031936 8823 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9041 8823 145 145 0 8896 0 [pid=22178] vsize: 36164 Current children cumulated CPU time (s) 249.25 Current children cumulated vsize (Kb) 38288 [startup+260.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 8838 0 2 0 25871 53 0 0 25 0 1 0 1841228195 37031936 8823 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9041 8823 145 145 0 8896 0 [pid=22178] vsize: 36164 Current children cumulated CPU time (s) 259.25 Current children cumulated vsize (Kb) 38288 [startup+270.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9212 0 2 0 26868 55 0 0 25 0 1 0 1841228195 38576128 9197 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9418 9197 145 145 0 9273 0 [pid=22178] vsize: 37672 Current children cumulated CPU time (s) 269.24 Current children cumulated vsize (Kb) 39796 [startup+280.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9212 0 2 0 27868 55 0 0 25 0 1 0 1841228195 38576128 9197 4294967295 134512640 135094434 3221224432 3221223008 134551616 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9418 9197 145 145 0 9273 0 [pid=22178] vsize: 37672 Current children cumulated CPU time (s) 279.24 Current children cumulated vsize (Kb) 39796 [startup+290.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9212 0 2 0 28868 55 0 0 25 0 1 0 1841228195 38576128 9197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9418 9197 145 145 0 9273 0 [pid=22178] vsize: 37672 Current children cumulated CPU time (s) 289.24 Current children cumulated vsize (Kb) 39796 [startup+300.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9222 0 2 0 29868 55 0 0 25 0 1 0 1841228195 38641664 9207 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9434 9207 145 145 0 9289 0 [pid=22178] vsize: 37736 Current children cumulated CPU time (s) 299.24 Current children cumulated vsize (Kb) 39860 [startup+310.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9234 0 2 0 30868 56 0 0 25 0 1 0 1841228195 38707200 9219 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9450 9219 145 145 0 9305 0 [pid=22178] vsize: 37800 Current children cumulated CPU time (s) 309.25 Current children cumulated vsize (Kb) 39924 [startup+320.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9381 0 2 0 31866 57 0 0 25 0 1 0 1841228195 39325696 9366 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9601 9366 145 145 0 9456 0 [pid=22178] vsize: 38404 Current children cumulated CPU time (s) 319.24 Current children cumulated vsize (Kb) 40528 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9451 0 2 0 32864 58 0 0 25 0 1 0 1841228195 39612416 9436 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9671 9436 145 145 0 9526 0 [pid=22178] vsize: 38684 Current children cumulated CPU time (s) 329.23 Current children cumulated vsize (Kb) 40808 [startup+340.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9451 0 2 0 33865 58 0 0 25 0 1 0 1841228195 39612416 9436 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9671 9436 145 145 0 9526 0 [pid=22178] vsize: 38684 Current children cumulated CPU time (s) 339.24 Current children cumulated vsize (Kb) 40808 [startup+350.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9451 0 2 0 34865 58 0 0 25 0 1 0 1841228195 39612416 9436 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9671 9436 145 145 0 9526 0 [pid=22178] vsize: 38684 Current children cumulated CPU time (s) 349.24 Current children cumulated vsize (Kb) 40808 [startup+360.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9451 0 2 0 35865 58 0 0 25 0 1 0 1841228195 39612416 9436 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9671 9436 145 145 0 9526 0 [pid=22178] vsize: 38684 Current children cumulated CPU time (s) 359.24 Current children cumulated vsize (Kb) 40808 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9461 0 2 0 36865 58 0 0 25 0 1 0 1841228195 39677952 9446 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9687 9446 145 145 0 9542 0 [pid=22178] vsize: 38748 Current children cumulated CPU time (s) 369.24 Current children cumulated vsize (Kb) 40872 [startup+380.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9461 0 2 0 37865 58 0 0 25 0 1 0 1841228195 39677952 9446 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9687 9446 145 145 0 9542 0 [pid=22178] vsize: 38748 Current children cumulated CPU time (s) 379.24 Current children cumulated vsize (Kb) 40872 [startup+390.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 9461 0 2 0 38865 58 0 0 25 0 1 0 1841228195 39677952 9446 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 9687 9446 145 145 0 9542 0 [pid=22178] vsize: 38748 Current children cumulated CPU time (s) 389.24 Current children cumulated vsize (Kb) 40872 [startup+400.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10081 0 2 0 39857 62 0 0 25 0 1 0 1841228195 42237952 10066 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 10312 10066 145 145 0 10167 0 [pid=22178] vsize: 41248 Current children cumulated CPU time (s) 399.2 Current children cumulated vsize (Kb) 43372 [startup+410.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10487 0 2 0 40851 65 0 0 25 0 1 0 1841228195 43900928 10472 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 10718 10472 145 145 0 10573 0 [pid=22178] vsize: 42872 Current children cumulated CPU time (s) 409.17 Current children cumulated vsize (Kb) 44996 [startup+420.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10487 0 2 0 41851 65 0 0 25 0 1 0 1841228195 43900928 10472 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 10718 10472 145 145 0 10573 0 [pid=22178] vsize: 42872 Current children cumulated CPU time (s) 419.17 Current children cumulated vsize (Kb) 44996 [startup+430.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 42846 67 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0 [pid=22178] vsize: 44556 Current children cumulated CPU time (s) 429.14 Current children cumulated vsize (Kb) 46680 [startup+440.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 43845 67 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0 [pid=22178] vsize: 44556 Current children cumulated CPU time (s) 439.13 Current children cumulated vsize (Kb) 46680 [startup+450.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 44844 68 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0 [pid=22178] vsize: 44556 Current children cumulated CPU time (s) 449.13 Current children cumulated vsize (Kb) 46680 [startup+460.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 45844 68 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0 [pid=22178] vsize: 44556 Current children cumulated CPU time (s) 459.13 Current children cumulated vsize (Kb) 46680 [startup+470.043 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10910 0 2 0 46844 68 0 0 25 0 1 0 1841228195 45625344 10895 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11139 10895 145 145 0 10994 0 [pid=22178] vsize: 44556 Current children cumulated CPU time (s) 469.13 Current children cumulated vsize (Kb) 46680 [startup+480.043 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 10942 0 2 0 47843 69 0 0 25 0 1 0 1841228195 45756416 10927 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11171 10927 145 145 0 11026 0 [pid=22178] vsize: 44684 Current children cumulated CPU time (s) 479.13 Current children cumulated vsize (Kb) 46808 [startup+490.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11197 0 2 0 48839 71 0 0 25 0 1 0 1841228195 46800896 11182 4294967295 134512640 135094434 3221224432 3221223024 134556823 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11426 11182 145 145 0 11281 0 [pid=22178] vsize: 45704 Current children cumulated CPU time (s) 489.11 Current children cumulated vsize (Kb) 47828 [startup+500.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11197 0 2 0 49838 71 0 0 25 0 1 0 1841228195 46800896 11182 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11426 11182 145 145 0 11281 0 [pid=22178] vsize: 45704 Current children cumulated CPU time (s) 499.1 Current children cumulated vsize (Kb) 47828 [startup+510.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11197 0 2 0 50838 71 0 0 25 0 1 0 1841228195 46800896 11182 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11426 11182 145 145 0 11281 0 [pid=22178] vsize: 45704 Current children cumulated CPU time (s) 509.1 Current children cumulated vsize (Kb) 47828 [startup+520.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11197 0 2 0 51838 71 0 0 25 0 1 0 1841228195 46800896 11182 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11426 11182 145 145 0 11281 0 [pid=22178] vsize: 45704 Current children cumulated CPU time (s) 519.1 Current children cumulated vsize (Kb) 47828 [startup+530.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 52831 75 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 529.07 Current children cumulated vsize (Kb) 49696 [startup+540.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 53831 75 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 539.07 Current children cumulated vsize (Kb) 49696 [startup+550.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 54830 76 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223024 134557531 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 549.07 Current children cumulated vsize (Kb) 49696 [startup+560.05 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 55830 76 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 559.07 Current children cumulated vsize (Kb) 49696 [startup+570.05 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 56830 76 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 569.07 Current children cumulated vsize (Kb) 49696 [startup+580.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 57829 77 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 579.07 Current children cumulated vsize (Kb) 49696 [startup+590.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 58829 77 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 589.07 Current children cumulated vsize (Kb) 49696 [startup+600.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 59829 77 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 599.07 Current children cumulated vsize (Kb) 49696 [startup+610.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 60829 77 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 609.07 Current children cumulated vsize (Kb) 49696 [startup+620.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 61828 78 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 619.07 Current children cumulated vsize (Kb) 49696 [startup+630.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 62828 78 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 629.07 Current children cumulated vsize (Kb) 49696 [startup+640.057 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 63828 78 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 639.07 Current children cumulated vsize (Kb) 49696 [startup+650.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 64827 79 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 649.07 Current children cumulated vsize (Kb) 49696 [startup+660.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 65827 79 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223072 134557059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 659.07 Current children cumulated vsize (Kb) 49696 [startup+670.059 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11664 0 2 0 66827 79 0 0 25 0 1 0 1841228195 48713728 11649 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 11893 11649 145 145 0 11748 0 [pid=22178] vsize: 47572 Current children cumulated CPU time (s) 669.07 Current children cumulated vsize (Kb) 49696 [startup+680.061 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 11781 0 2 0 67825 79 0 0 25 0 1 0 1841228195 49213440 11766 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 12015 11766 145 145 0 11870 0 [pid=22178] vsize: 48060 Current children cumulated CPU time (s) 679.05 Current children cumulated vsize (Kb) 50184 [startup+690.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12133 0 2 0 68819 82 0 0 25 0 1 0 1841228195 50667520 12118 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 12370 12118 145 145 0 12225 0 [pid=22178] vsize: 49480 Current children cumulated CPU time (s) 689.02 Current children cumulated vsize (Kb) 51604 [startup+700.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12133 0 2 0 69819 82 0 0 25 0 1 0 1841228195 50667520 12118 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 12370 12118 145 145 0 12225 0 [pid=22178] vsize: 49480 Current children cumulated CPU time (s) 699.02 Current children cumulated vsize (Kb) 51604 [startup+710.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12145 0 2 0 70819 82 0 0 25 0 1 0 1841228195 50733056 12130 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 12386 12130 145 145 0 12241 0 [pid=22178] vsize: 49544 Current children cumulated CPU time (s) 709.02 Current children cumulated vsize (Kb) 51668 [startup+720.064 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12169 0 2 0 71819 82 0 0 25 0 1 0 1841228195 50864128 12154 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 12418 12154 145 145 0 12273 0 [pid=22178] vsize: 49672 Current children cumulated CPU time (s) 719.02 Current children cumulated vsize (Kb) 51796 [startup+730.065 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12182 0 2 0 72818 82 0 0 25 0 1 0 1841228195 50929664 12167 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 12434 12167 145 145 0 12289 0 [pid=22178] vsize: 49736 Current children cumulated CPU time (s) 729.01 Current children cumulated vsize (Kb) 51860 [startup+740.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12199 0 2 0 73818 83 0 0 25 0 1 0 1841228195 50995200 12184 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 12450 12184 145 145 0 12305 0 [pid=22178] vsize: 49800 Current children cumulated CPU time (s) 739.02 Current children cumulated vsize (Kb) 51924 [startup+750.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12199 0 2 0 74818 83 0 0 25 0 1 0 1841228195 50995200 12184 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 12450 12184 145 145 0 12305 0 [pid=22178] vsize: 49800 Current children cumulated CPU time (s) 749.02 Current children cumulated vsize (Kb) 51924 [startup+760.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12564 0 2 0 75812 86 0 0 25 0 1 0 1841228195 52539392 12549 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 12827 12549 145 145 0 12682 0 [pid=22178] vsize: 51308 Current children cumulated CPU time (s) 758.99 Current children cumulated vsize (Kb) 53432 [startup+770.069 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 76807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0 [pid=22178] vsize: 52304 Current children cumulated CPU time (s) 768.96 Current children cumulated vsize (Kb) 54428 [startup+780.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 77807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0 [pid=22178] vsize: 52304 Current children cumulated CPU time (s) 778.96 Current children cumulated vsize (Kb) 54428 [startup+790.071 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 78807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0 [pid=22178] vsize: 52304 Current children cumulated CPU time (s) 788.96 Current children cumulated vsize (Kb) 54428 [startup+800.071 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 79807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0 [pid=22178] vsize: 52304 Current children cumulated CPU time (s) 798.96 Current children cumulated vsize (Kb) 54428 [startup+810.072 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 80807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0 [pid=22178] vsize: 52304 Current children cumulated CPU time (s) 808.96 Current children cumulated vsize (Kb) 54428 [startup+820.073 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 81807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0 [pid=22178] vsize: 52304 Current children cumulated CPU time (s) 818.96 Current children cumulated vsize (Kb) 54428 [startup+830.074 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12813 0 2 0 82807 88 0 0 25 0 1 0 1841228195 53559296 12798 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13076 12798 145 145 0 12931 0 [pid=22178] vsize: 52304 Current children cumulated CPU time (s) 828.96 Current children cumulated vsize (Kb) 54428 [startup+840.074 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 12827 0 2 0 83807 89 0 0 25 0 1 0 1841228195 53624832 12812 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13092 12812 145 145 0 12947 0 [pid=22178] vsize: 52368 Current children cumulated CPU time (s) 838.97 Current children cumulated vsize (Kb) 54492 [startup+850.074 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 84802 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0 [pid=22178] vsize: 53576 Current children cumulated CPU time (s) 848.93 Current children cumulated vsize (Kb) 55700 [startup+860.075 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 85803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0 [pid=22178] vsize: 53576 Current children cumulated CPU time (s) 858.94 Current children cumulated vsize (Kb) 55700 [startup+870.076 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 86803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0 [pid=22178] vsize: 53576 Current children cumulated CPU time (s) 868.94 Current children cumulated vsize (Kb) 55700 [startup+880.077 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 87803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223024 134556914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0 [pid=22178] vsize: 53576 Current children cumulated CPU time (s) 878.94 Current children cumulated vsize (Kb) 55700 [startup+890.077 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 88803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223024 134556876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0 [pid=22178] vsize: 53576 Current children cumulated CPU time (s) 888.94 Current children cumulated vsize (Kb) 55700 [startup+900.078 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13131 0 2 0 89803 90 0 0 25 0 1 0 1841228195 54861824 13116 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13394 13116 145 145 0 13249 0 [pid=22178] vsize: 53576 Current children cumulated CPU time (s) 898.94 Current children cumulated vsize (Kb) 55700 [startup+910.079 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13142 0 2 0 90804 90 0 0 25 0 1 0 1841228195 54923264 13127 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13409 13127 145 145 0 13264 0 [pid=22178] vsize: 53636 Current children cumulated CPU time (s) 908.95 Current children cumulated vsize (Kb) 55760 [startup+920.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 91798 93 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0 [pid=22178] vsize: 54812 Current children cumulated CPU time (s) 918.92 Current children cumulated vsize (Kb) 56936 [startup+930.081 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 92798 93 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0 [pid=22178] vsize: 54812 Current children cumulated CPU time (s) 928.92 Current children cumulated vsize (Kb) 56936 [startup+940.081 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 93799 93 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0 [pid=22178] vsize: 54812 Current children cumulated CPU time (s) 938.93 Current children cumulated vsize (Kb) 56936 [startup+950.082 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 94799 93 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0 [pid=22178] vsize: 54812 Current children cumulated CPU time (s) 948.93 Current children cumulated vsize (Kb) 56936 [startup+960.083 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 95799 94 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0 [pid=22178] vsize: 54812 Current children cumulated CPU time (s) 958.94 Current children cumulated vsize (Kb) 56936 [startup+970.084 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13434 0 2 0 96799 94 0 0 25 0 1 0 1841228195 56127488 13419 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13703 13419 145 145 0 13558 0 [pid=22178] vsize: 54812 Current children cumulated CPU time (s) 968.94 Current children cumulated vsize (Kb) 56936 [startup+980.085 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13506 0 2 0 97798 94 0 0 25 0 1 0 1841228195 56426496 13491 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 13776 13491 145 145 0 13631 0 [pid=22178] vsize: 55104 Current children cumulated CPU time (s) 978.93 Current children cumulated vsize (Kb) 57228 [startup+990.085 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 13909 0 2 0 98792 96 0 0 25 0 1 0 1841228195 58122240 13894 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14190 13894 145 145 0 14045 0 [pid=22178] vsize: 56760 Current children cumulated CPU time (s) 988.89 Current children cumulated vsize (Kb) 58884 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14051 0 2 0 99790 97 0 0 25 0 1 0 1841228195 58728448 14036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14338 14036 145 145 0 14193 0 [pid=22178] vsize: 57352 Current children cumulated CPU time (s) 998.88 Current children cumulated vsize (Kb) 59476 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14052 0 2 0 100790 97 0 0 25 0 1 0 1841228195 58728448 14037 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14338 14037 145 145 0 14193 0 [pid=22178] vsize: 57352 Current children cumulated CPU time (s) 1008.88 Current children cumulated vsize (Kb) 59476 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14063 0 2 0 101790 97 0 0 25 0 1 0 1841228195 58793984 14048 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14048 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1018.88 Current children cumulated vsize (Kb) 59540 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14064 0 2 0 102789 99 0 0 25 0 1 0 1841228195 58793984 14049 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14049 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1028.89 Current children cumulated vsize (Kb) 59540 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14064 0 2 0 103788 99 0 0 25 0 1 0 1841228195 58793984 14049 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14049 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1038.88 Current children cumulated vsize (Kb) 59540 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.98 3/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 104788 100 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1048.89 Current children cumulated vsize (Kb) 59540 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 105788 100 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1058.89 Current children cumulated vsize (Kb) 59540 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 106788 101 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1068.9 Current children cumulated vsize (Kb) 59540 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 107788 101 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1078.9 Current children cumulated vsize (Kb) 59540 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 108788 101 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1088.9 Current children cumulated vsize (Kb) 59540 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 109788 101 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1098.9 Current children cumulated vsize (Kb) 59540 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 110788 102 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1108.91 Current children cumulated vsize (Kb) 59540 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 111788 102 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1118.91 Current children cumulated vsize (Kb) 59540 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 14065 0 2 0 112788 102 0 0 25 0 1 0 1841228195 58793984 14050 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 14354 14050 145 145 0 14209 0 [pid=22178] vsize: 57416 Current children cumulated CPU time (s) 1128.91 Current children cumulated vsize (Kb) 59540 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15312 0 2 0 113772 109 0 0 25 0 1 0 1841228195 63893504 15297 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 15599 15297 145 145 0 15454 0 [pid=22178] vsize: 62396 Current children cumulated CPU time (s) 1138.82 Current children cumulated vsize (Kb) 64520 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15312 0 2 0 114772 109 0 0 25 0 1 0 1841228195 63893504 15297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 15599 15297 145 145 0 15454 0 [pid=22178] vsize: 62396 Current children cumulated CPU time (s) 1148.82 Current children cumulated vsize (Kb) 64520 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15312 0 2 0 115772 109 0 0 25 0 1 0 1841228195 63893504 15297 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 15599 15297 145 145 0 15454 0 [pid=22178] vsize: 62396 Current children cumulated CPU time (s) 1158.82 Current children cumulated vsize (Kb) 64520 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 116772 109 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0 [pid=22178] vsize: 62396 Current children cumulated CPU time (s) 1168.82 Current children cumulated vsize (Kb) 64520 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 117772 109 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0 [pid=22178] vsize: 62396 Current children cumulated CPU time (s) 1178.82 Current children cumulated vsize (Kb) 64520 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 118772 110 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0 [pid=22178] vsize: 62396 Current children cumulated CPU time (s) 1188.83 Current children cumulated vsize (Kb) 64520 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 119772 110 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0 [pid=22178] vsize: 62396 Current children cumulated CPU time (s) 1198.83 Current children cumulated vsize (Kb) 64520 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 120772 110 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0 [pid=22178] vsize: 62396 Current children cumulated CPU time (s) 1208.83 Current children cumulated vsize (Kb) 64520 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22178 Raw data (/proc/22174/stat): 22174 (minisat+_script) S 22173 22174 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1841228190 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22174/statm): 531 226 485 147 0 384 0 [pid=22174] vsize: 2124 Raw data (/proc/22178/stat): 22178 (minisat+_64-bit) R 22174 22174 19818 0 -1 0 15313 0 2 0 120772 110 0 0 25 0 1 0 1841228195 63893504 15298 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22178/statm): 15599 15298 145 145 0 15454 0 [pid=22178] vsize: 62396 Current children cumulated CPU time (s) 1208.83 Current children cumulated vsize (Kb) 64520 Sending SIGTERM to -22174 Sleeping 2 seconds One traced child (pid=22174) ended because it received signal 15 (SIGTERM) One traced child (pid=22178) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.14 CPU time (s): 1208.86 CPU user time (s): 1207.73 CPU system time (s): 1.13583 CPU usage (%): 99.8947 Max. virtual memory (cumulated for all children) (Kb): 64520
ERROR: no interpretation found !