Name | submitted/aloul/FPGA_SAT05/normalized-chnl30_35_pb.cnf.cr.opb |
MD5SUM | b1c5adb5438ceaf1c654cfedb79b695e |
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 | 36 |
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.068989 |
Number of variables | 2100 |
Total number of constraints | 130 |
Number of constraints which are clauses | 70 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 35 |
LAUNCH ON wulflinc8 THE 2005-09-18 12:24:31 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2354 boxname=wulflinc8 idbench=10 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b1c5adb5438ceaf1c654cfedb79b695e /oldhome/oroussel/tmp/wulflinc8/normalized-chnl30_35_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-chnl30_35_pb.cnf.cr.opb IDLAUNCH: 2354 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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: 947196 kB Buffers: 33736 kB Cached: 29052 kB SwapCached: 792 kB Active: 53556 kB Inactive: 11916 kB HighTotal: 131008 kB HighFree: 98112 kB LowTotal: 903652 kB LowFree: 849084 kB SwapTotal: 2097136 kB SwapFree: 2095876 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5752 kB Slab: 16356 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 12:44:41 (client local time) WITH STATUS 0 IN 1208.88 SECONDS stats: 2354 7 1208.88 0
c Parsing PB file... c Converting 130 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ...................................................................... c ---[ 59]---> BDD-cost: 67 c ---[ 58]---> BDD-cost: 67 c ---[ 57]---> BDD-cost: 67 c ---[ 56]---> BDD-cost: 67 c ---[ 55]---> BDD-cost: 67 c ---[ 54]---> BDD-cost: 67 c ---[ 53]---> BDD-cost: 67 c ---[ 52]---> BDD-cost: 67 c ---[ 51]---> BDD-cost: 67 c ---[ 50]---> BDD-cost: 67 c ---[ 49]---> BDD-cost: 67 c ---[ 48]---> BDD-cost: 67 c ---[ 47]---> BDD-cost: 67 c ---[ 46]---> BDD-cost: 67 c ---[ 45]---> BDD-cost: 67 c ---[ 44]---> BDD-cost: 67 c ---[ 43]---> BDD-cost: 67 c ---[ 42]---> BDD-cost: 67 c ---[ 41]---> BDD-cost: 67 c ---[ 40]---> BDD-cost: 67 c ---[ 39]---> BDD-cost: 67 c ---[ 38]---> BDD-cost: 67 c ---[ 37]---> BDD-cost: 67 c ---[ 36]---> BDD-cost: 67 c ---[ 35]---> BDD-cost: 67 c ---[ 34]---> BDD-cost: 67 c ---[ 33]---> BDD-cost: 67 c ---[ 32]---> BDD-cost: 67 c ---[ 31]---> BDD-cost: 67 c ---[ 30]---> BDD-cost: 67 c ---[ 29]---> BDD-cost: 67 c ---[ 28]---> BDD-cost: 67 c ---[ 27]---> BDD-cost: 67 c ---[ 26]---> BDD-cost: 67 c ---[ 25]---> BDD-cost: 67 c ---[ 24]---> BDD-cost: 67 c ---[ 23]---> BDD-cost: 67 c ---[ 22]---> BDD-cost: 67 c ---[ 21]---> BDD-cost: 67 c ---[ 20]---> BDD-cost: 67 c ---[ 19]---> BDD-cost: 67 c ---[ 18]---> BDD-cost: 67 c ---[ 17]---> BDD-cost: 67 c ---[ 16]---> BDD-cost: 67 c ---[ 15]---> BDD-cost: 67 c ---[ 14]---> BDD-cost: 67 c ---[ 13]---> BDD-cost: 67 c ---[ 12]---> BDD-cost: 67 c ---[ 11]---> BDD-cost: 67 c ---[ 10]---> BDD-cost: 67 c ---[ 9]---> BDD-cost: 67 c ---[ 8]---> BDD-cost: 67 c ---[ 7]---> BDD-cost: 67 c ---[ 6]---> BDD-cost: 67 c ---[ 5]---> BDD-cost: 67 c ---[ 4]---> BDD-cost: 67 c ---[ 3]---> BDD-cost: 67 c ---[ 2]---> BDD-cost: 67 c ---[ 1]---> BDD-cost: 67 c ---[ 0]---> BDD-cost: 67 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 10030 28020 | 3343 0 0 nan | 0.000 % | c | 105 | 10030 28020 | 3677 105 11655 111.0 | 0.980 % | c | 257 | 10030 28020 | 4045 257 29832 116.1 | 0.980 % | c | 483 | 10030 28020 | 4449 483 70240 145.4 | 0.980 % | c | 822 | 10030 28020 | 4894 822 128798 156.7 | 0.980 % | c | 1332 | 10030 28020 | 5383 1332 212600 159.6 | 0.980 % | c | 2091 | 10030 28020 | 5922 2091 359695 172.0 | 0.980 % | c | 3231 | 10030 28020 | 6514 3231 581665 180.0 | 0.980 % | c | 4941 | 10030 28020 | 7166 4941 1128031 228.3 | 0.980 % | c | 7504 | 10030 28020 | 7882 7504 1889344 251.8 | 0.980 % | c | 11348 | 10030 28020 | 8670 6199 1605192 258.9 | 0.980 % | c | 17117 | 10030 28020 | 9537 6488 1486146 229.1 | 0.980 % | c | 25767 | 10030 28020 | 10491 9195 2320409 252.4 | 0.980 % | c | 38743 | 10030 28020 | 11540 9205 1749321 190.0 | 0.980 % | c | 58205 | 10030 28020 | 12695 7890 2211413 280.3 | 0.980 % | c | 87397 | 10030 28020 | 13964 8204 2185785 266.4 | 0.980 % | c | 131187 | 10030 28020 | 15360 10994 2976111 270.7 | 0.980 % | c | 196872 | 10030 28020 | 16897 18139 5203446 286.9 | 0.980 % | c | 295406 | 10030 28020 | 18586 16345 8504574 520.3 | 0.980 % |
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/29731/stat): 29731 (minisat+_script) R 29730 29731 27660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1769439868 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/29731/statm): 174 3 169 147 0 27 0 [pid=29731] 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=29732 New process pid=29733 New process pid=29734 execve syscall for /bin/sed executable One traced child (pid=29733) 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=29734) exited with status: 0 One traced child (pid=29732) exited with status: 0 New process pid=29735 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-chnl30_35_pb.cnf.cr.opb [startup+10.0055 s] Raw data (loadavg): 1.08 1.02 0.98 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 2672 0 2 0 950 14 0 0 25 0 1 0 1769439873 11337728 2660 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29735/statm): 2768 2660 145 145 0 2623 0 [pid=29735] vsize: 11072 Current children cumulated CPU time (s) 9.65 Current children cumulated vsize (Kb) 13196 [startup+20.0073 s] Raw data (loadavg): 1.07 1.02 0.98 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 3355 0 2 0 1940 19 0 0 25 0 1 0 1769439873 14155776 3343 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 3456 3343 145 145 0 3311 0 [pid=29735] vsize: 13824 Current children cumulated CPU time (s) 19.6 Current children cumulated vsize (Kb) 15948 [startup+30.0081 s] Raw data (loadavg): 1.06 1.01 0.98 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 3593 0 2 0 2936 20 0 0 25 0 1 0 1769439873 15134720 3581 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29735/statm): 3695 3581 145 145 0 3550 0 [pid=29735] vsize: 14780 Current children cumulated CPU time (s) 29.57 Current children cumulated vsize (Kb) 16904 [startup+40.0099 s] Raw data (loadavg): 1.05 1.01 0.98 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 3874 0 2 0 3932 22 0 0 25 0 1 0 1769439873 16289792 3862 4294967295 134512640 135094434 3221224432 3221223104 134556297 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 3977 3862 145 145 0 3832 0 [pid=29735] vsize: 15908 Current children cumulated CPU time (s) 39.55 Current children cumulated vsize (Kb) 18032 [startup+50.0106 s] Raw data (loadavg): 1.04 1.01 0.98 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 4161 0 2 0 4928 23 0 0 25 0 1 0 1769439873 17457152 4149 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 4262 4149 145 145 0 4117 0 [pid=29735] vsize: 17048 Current children cumulated CPU time (s) 49.52 Current children cumulated vsize (Kb) 19172 [startup+60.0114 s] Raw data (loadavg): 1.11 1.03 0.98 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 4161 0 2 0 5928 23 0 0 25 0 1 0 1769439873 17457152 4149 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 4262 4149 145 145 0 4117 0 [pid=29735] vsize: 17048 Current children cumulated CPU time (s) 59.52 Current children cumulated vsize (Kb) 19172 [startup+70.0132 s] Raw data (loadavg): 1.17 1.04 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 4161 0 2 0 6929 23 0 0 25 0 1 0 1769439873 17457152 4149 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 4262 4149 145 145 0 4117 0 [pid=29735] vsize: 17048 Current children cumulated CPU time (s) 69.53 Current children cumulated vsize (Kb) 19172 [startup+80.014 s] Raw data (loadavg): 1.14 1.04 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 4221 0 2 0 7928 24 0 0 25 0 1 0 1769439873 17698816 4209 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 4321 4209 145 145 0 4176 0 [pid=29735] vsize: 17284 Current children cumulated CPU time (s) 79.53 Current children cumulated vsize (Kb) 19408 [startup+90.0148 s] Raw data (loadavg): 1.12 1.04 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 4885 0 2 0 8918 28 0 0 25 0 1 0 1769439873 20422656 4873 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 4986 4873 145 145 0 4841 0 [pid=29735] vsize: 19944 Current children cumulated CPU time (s) 89.47 Current children cumulated vsize (Kb) 22068 [startup+100.016 s] Raw data (loadavg): 1.10 1.04 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5131 0 2 0 9914 29 0 0 25 0 1 0 1769439873 21446656 5119 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 5236 5119 145 145 0 5091 0 [pid=29735] vsize: 20944 Current children cumulated CPU time (s) 99.44 Current children cumulated vsize (Kb) 23068 [startup+110.016 s] Raw data (loadavg): 1.08 1.04 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5145 0 2 0 10914 29 0 0 25 0 1 0 1769439873 21512192 5133 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 5252 5133 145 145 0 5107 0 [pid=29735] vsize: 21008 Current children cumulated CPU time (s) 109.44 Current children cumulated vsize (Kb) 23132 [startup+120.017 s] Raw data (loadavg): 1.07 1.03 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5332 0 2 0 11912 30 0 0 25 0 1 0 1769439873 22310912 5320 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 5447 5320 145 145 0 5302 0 [pid=29735] vsize: 21788 Current children cumulated CPU time (s) 119.43 Current children cumulated vsize (Kb) 23912 [startup+130.018 s] Raw data (loadavg): 1.06 1.03 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5654 0 2 0 12908 32 0 0 25 0 1 0 1769439873 23674880 5642 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 5780 5642 145 145 0 5635 0 [pid=29735] vsize: 23120 Current children cumulated CPU time (s) 129.41 Current children cumulated vsize (Kb) 25244 [startup+140.02 s] Raw data (loadavg): 1.05 1.03 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5654 0 2 0 13908 32 0 0 25 0 1 0 1769439873 23674880 5642 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 5780 5642 145 145 0 5635 0 [pid=29735] vsize: 23120 Current children cumulated CPU time (s) 139.41 Current children cumulated vsize (Kb) 25244 [startup+150.02 s] Raw data (loadavg): 1.04 1.03 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5762 0 2 0 14906 34 0 0 25 0 1 0 1769439873 24137728 5750 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 5893 5750 145 145 0 5748 0 [pid=29735] vsize: 23572 Current children cumulated CPU time (s) 149.41 Current children cumulated vsize (Kb) 25696 [startup+160.021 s] Raw data (loadavg): 1.04 1.03 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5762 0 2 0 15907 34 0 0 25 0 1 0 1769439873 24137728 5750 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 5893 5750 145 145 0 5748 0 [pid=29735] vsize: 23572 Current children cumulated CPU time (s) 159.42 Current children cumulated vsize (Kb) 25696 [startup+170.022 s] Raw data (loadavg): 1.03 1.03 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5762 0 2 0 16907 34 0 0 25 0 1 0 1769439873 24137728 5750 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 5893 5750 145 145 0 5748 0 [pid=29735] vsize: 23572 Current children cumulated CPU time (s) 169.42 Current children cumulated vsize (Kb) 25696 [startup+180.023 s] Raw data (loadavg): 1.02 1.03 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5762 0 2 0 17907 34 0 0 25 0 1 0 1769439873 24137728 5750 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 5893 5750 145 145 0 5748 0 [pid=29735] vsize: 23572 Current children cumulated CPU time (s) 179.42 Current children cumulated vsize (Kb) 25696 [startup+190.025 s] Raw data (loadavg): 1.02 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5763 0 2 0 18907 34 0 0 25 0 1 0 1769439873 24137728 5751 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29735/statm): 5893 5751 145 145 0 5748 0 [pid=29735] vsize: 23572 Current children cumulated CPU time (s) 189.42 Current children cumulated vsize (Kb) 25696 [startup+200.026 s] Raw data (loadavg): 1.02 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 5763 0 2 0 19906 34 0 0 25 0 1 0 1769439873 24137728 5751 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29735/statm): 5893 5751 145 145 0 5748 0 [pid=29735] vsize: 23572 Current children cumulated CPU time (s) 199.41 Current children cumulated vsize (Kb) 25696 [startup+210.027 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6235 0 2 0 20897 39 0 0 25 0 1 0 1769439873 26189824 6223 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 6394 6223 145 145 0 6249 0 [pid=29735] vsize: 25576 Current children cumulated CPU time (s) 209.37 Current children cumulated vsize (Kb) 27700 [startup+220.028 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6237 0 2 0 21897 39 0 0 25 0 1 0 1769439873 26189824 6225 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 6394 6225 145 145 0 6249 0 [pid=29735] vsize: 25576 Current children cumulated CPU time (s) 219.37 Current children cumulated vsize (Kb) 27700 [startup+230.029 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6238 0 2 0 22897 39 0 0 25 0 1 0 1769439873 26189824 6226 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 6394 6226 145 145 0 6249 0 [pid=29735] vsize: 25576 Current children cumulated CPU time (s) 229.37 Current children cumulated vsize (Kb) 27700 [startup+240.031 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6238 0 2 0 23897 39 0 0 25 0 1 0 1769439873 26189824 6226 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 6394 6226 145 145 0 6249 0 [pid=29735] vsize: 25576 Current children cumulated CPU time (s) 239.37 Current children cumulated vsize (Kb) 27700 [startup+250.031 s] Raw data (loadavg): 1.01 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6328 0 2 0 24897 40 0 0 25 0 1 0 1769439873 26587136 6316 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 6491 6316 145 145 0 6346 0 [pid=29735] vsize: 25964 Current children cumulated CPU time (s) 249.38 Current children cumulated vsize (Kb) 28088 [startup+260.031 s] Raw data (loadavg): 1.00 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6328 0 2 0 25897 40 0 0 25 0 1 0 1769439873 26587136 6316 4294967295 134512640 135094434 3221224432 3221223024 134557283 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 6491 6316 145 145 0 6346 0 [pid=29735] vsize: 25964 Current children cumulated CPU time (s) 259.38 Current children cumulated vsize (Kb) 28088 [startup+270.033 s] Raw data (loadavg): 1.00 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6342 0 2 0 26897 40 0 0 25 0 1 0 1769439873 26652672 6330 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 6507 6330 145 145 0 6362 0 [pid=29735] vsize: 26028 Current children cumulated CPU time (s) 269.38 Current children cumulated vsize (Kb) 28152 [startup+280.034 s] Raw data (loadavg): 1.00 1.02 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6966 0 2 0 27888 44 0 0 25 0 1 0 1769439873 29204480 6954 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 7130 6954 145 145 0 6985 0 [pid=29735] vsize: 28520 Current children cumulated CPU time (s) 279.33 Current children cumulated vsize (Kb) 30644 [startup+290.034 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6968 0 2 0 28888 44 0 0 25 0 1 0 1769439873 29204480 6956 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 7130 6956 145 145 0 6985 0 [pid=29735] vsize: 28520 Current children cumulated CPU time (s) 289.33 Current children cumulated vsize (Kb) 30644 [startup+300.035 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6977 0 2 0 29888 44 0 0 25 0 1 0 1769439873 29270016 6965 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 7146 6965 145 145 0 7001 0 [pid=29735] vsize: 28584 Current children cumulated CPU time (s) 299.33 Current children cumulated vsize (Kb) 30708 [startup+310.036 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6977 0 2 0 30888 44 0 0 25 0 1 0 1769439873 29270016 6965 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 7146 6965 145 145 0 7001 0 [pid=29735] vsize: 28584 Current children cumulated CPU time (s) 309.33 Current children cumulated vsize (Kb) 30708 [startup+320.037 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6979 0 2 0 31889 44 0 0 25 0 1 0 1769439873 29270016 6967 4294967295 134512640 135094434 3221224432 3221223104 134556499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 7146 6967 145 145 0 7001 0 [pid=29735] vsize: 28584 Current children cumulated CPU time (s) 319.34 Current children cumulated vsize (Kb) 30708 [startup+330.038 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 6979 0 2 0 32889 45 0 0 25 0 1 0 1769439873 29270016 6967 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29735/statm): 7146 6967 145 145 0 7001 0 [pid=29735] vsize: 28584 Current children cumulated CPU time (s) 329.35 Current children cumulated vsize (Kb) 30708 [startup+340.039 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 7184 0 2 0 33885 46 0 0 25 0 1 0 1769439873 30101504 7172 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 7349 7172 145 145 0 7204 0 [pid=29735] vsize: 29396 Current children cumulated CPU time (s) 339.32 Current children cumulated vsize (Kb) 31520 [startup+350.04 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 7847 0 2 0 34877 50 0 0 25 0 1 0 1769439873 32817152 7835 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8012 7835 145 145 0 7867 0 [pid=29735] vsize: 32048 Current children cumulated CPU time (s) 349.28 Current children cumulated vsize (Kb) 34172 [startup+360.041 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 7847 0 2 0 35878 50 0 0 25 0 1 0 1769439873 32817152 7835 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8012 7835 145 145 0 7867 0 [pid=29735] vsize: 32048 Current children cumulated CPU time (s) 359.29 Current children cumulated vsize (Kb) 34172 [startup+370.042 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 7847 0 2 0 36878 50 0 0 25 0 1 0 1769439873 32817152 7835 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8012 7835 145 145 0 7867 0 [pid=29735] vsize: 32048 Current children cumulated CPU time (s) 369.29 Current children cumulated vsize (Kb) 34172 [startup+380.043 s] Raw data (loadavg): 1.00 1.01 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 7847 0 2 0 37878 50 0 0 25 0 1 0 1769439873 32817152 7835 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8012 7835 145 145 0 7867 0 [pid=29735] vsize: 32048 Current children cumulated CPU time (s) 379.29 Current children cumulated vsize (Kb) 34172 [startup+390.044 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8080 0 2 0 38874 51 0 0 25 0 1 0 1769439873 33771520 8068 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8245 8068 145 145 0 8100 0 [pid=29735] vsize: 32980 Current children cumulated CPU time (s) 389.26 Current children cumulated vsize (Kb) 35104 [startup+400.045 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8080 0 2 0 39875 51 0 0 25 0 1 0 1769439873 33771520 8068 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8245 8068 145 145 0 8100 0 [pid=29735] vsize: 32980 Current children cumulated CPU time (s) 399.27 Current children cumulated vsize (Kb) 35104 [startup+410.046 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8080 0 2 0 40875 51 0 0 25 0 1 0 1769439873 33771520 8068 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8245 8068 145 145 0 8100 0 [pid=29735] vsize: 32980 Current children cumulated CPU time (s) 409.27 Current children cumulated vsize (Kb) 35104 [startup+420.047 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8413 0 2 0 41870 53 0 0 25 0 1 0 1769439873 35160064 8401 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8584 8401 145 145 0 8439 0 [pid=29735] vsize: 34336 Current children cumulated CPU time (s) 419.24 Current children cumulated vsize (Kb) 36460 [startup+430.047 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8430 0 2 0 42870 54 0 0 25 0 1 0 1769439873 35250176 8418 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8606 8418 145 145 0 8461 0 [pid=29735] vsize: 34424 Current children cumulated CPU time (s) 429.25 Current children cumulated vsize (Kb) 36548 [startup+440.049 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8430 0 2 0 43870 54 0 0 25 0 1 0 1769439873 35250176 8418 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8606 8418 145 145 0 8461 0 [pid=29735] vsize: 34424 Current children cumulated CPU time (s) 439.25 Current children cumulated vsize (Kb) 36548 [startup+450.05 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8430 0 2 0 44871 54 0 0 25 0 1 0 1769439873 35250176 8418 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8606 8418 145 145 0 8461 0 [pid=29735] vsize: 34424 Current children cumulated CPU time (s) 449.26 Current children cumulated vsize (Kb) 36548 [startup+460.051 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8430 0 2 0 45870 54 0 0 25 0 1 0 1769439873 35250176 8418 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 8606 8418 145 145 0 8461 0 [pid=29735] vsize: 34424 Current children cumulated CPU time (s) 459.25 Current children cumulated vsize (Kb) 36548 [startup+470.052 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8876 0 2 0 46864 56 0 0 25 0 1 0 1769439873 37085184 8864 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9054 8864 145 145 0 8909 0 [pid=29735] vsize: 36216 Current children cumulated CPU time (s) 469.21 Current children cumulated vsize (Kb) 38340 [startup+480.052 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8876 0 2 0 47865 56 0 0 25 0 1 0 1769439873 37085184 8864 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9054 8864 145 145 0 8909 0 [pid=29735] vsize: 36216 Current children cumulated CPU time (s) 479.22 Current children cumulated vsize (Kb) 38340 [startup+490.054 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 8876 0 2 0 48865 56 0 0 25 0 1 0 1769439873 37085184 8864 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9054 8864 145 145 0 8909 0 [pid=29735] vsize: 36216 Current children cumulated CPU time (s) 489.22 Current children cumulated vsize (Kb) 38340 [startup+500.055 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9151 0 2 0 49862 58 0 0 25 0 1 0 1769439873 38211584 9139 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9329 9139 145 145 0 9184 0 [pid=29735] vsize: 37316 Current children cumulated CPU time (s) 499.21 Current children cumulated vsize (Kb) 39440 [startup+510.056 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9151 0 2 0 50862 58 0 0 25 0 1 0 1769439873 38211584 9139 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9329 9139 145 145 0 9184 0 [pid=29735] vsize: 37316 Current children cumulated CPU time (s) 509.21 Current children cumulated vsize (Kb) 39440 [startup+520.056 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9151 0 2 0 51862 58 0 0 25 0 1 0 1769439873 38211584 9139 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9329 9139 145 145 0 9184 0 [pid=29735] vsize: 37316 Current children cumulated CPU time (s) 519.21 Current children cumulated vsize (Kb) 39440 [startup+530.057 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9152 0 2 0 52862 58 0 0 25 0 1 0 1769439873 38211584 9140 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9329 9140 145 145 0 9184 0 [pid=29735] vsize: 37316 Current children cumulated CPU time (s) 529.21 Current children cumulated vsize (Kb) 39440 [startup+540.057 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9153 0 2 0 53862 58 0 0 25 0 1 0 1769439873 38211584 9141 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9329 9141 145 145 0 9184 0 [pid=29735] vsize: 37316 Current children cumulated CPU time (s) 539.21 Current children cumulated vsize (Kb) 39440 [startup+550.059 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9181 0 2 0 54862 58 0 0 25 0 1 0 1769439873 38395904 9169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9374 9169 145 145 0 9229 0 [pid=29735] vsize: 37496 Current children cumulated CPU time (s) 549.21 Current children cumulated vsize (Kb) 39620 [startup+560.059 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9181 0 2 0 55862 58 0 0 25 0 1 0 1769439873 38395904 9169 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9374 9169 145 145 0 9229 0 [pid=29735] vsize: 37496 Current children cumulated CPU time (s) 559.21 Current children cumulated vsize (Kb) 39620 [startup+570.059 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9181 0 2 0 56862 58 0 0 25 0 1 0 1769439873 38395904 9169 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9374 9169 145 145 0 9229 0 [pid=29735] vsize: 37496 Current children cumulated CPU time (s) 569.21 Current children cumulated vsize (Kb) 39620 [startup+580.06 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9181 0 2 0 57862 58 0 0 25 0 1 0 1769439873 38395904 9169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9374 9169 145 145 0 9229 0 [pid=29735] vsize: 37496 Current children cumulated CPU time (s) 579.21 Current children cumulated vsize (Kb) 39620 [startup+590.06 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9181 0 2 0 58863 58 0 0 25 0 1 0 1769439873 38395904 9169 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 9374 9169 145 145 0 9229 0 [pid=29735] vsize: 37496 Current children cumulated CPU time (s) 589.22 Current children cumulated vsize (Kb) 39620 [startup+600.061 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 9637 0 2 0 59856 61 0 0 25 0 1 0 1769439873 40263680 9625 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29735/statm): 9830 9625 145 145 0 9685 0 [pid=29735] vsize: 39320 Current children cumulated CPU time (s) 599.18 Current children cumulated vsize (Kb) 41444 [startup+610.062 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 10062 0 2 0 60849 64 0 0 25 0 1 0 1769439873 42008576 10050 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 10256 10050 145 145 0 10111 0 [pid=29735] vsize: 41024 Current children cumulated CPU time (s) 609.14 Current children cumulated vsize (Kb) 43148 [startup+620.062 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 10119 0 2 0 61848 64 0 0 25 0 1 0 1769439873 42242048 10107 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 10313 10107 145 145 0 10168 0 [pid=29735] vsize: 41252 Current children cumulated CPU time (s) 619.13 Current children cumulated vsize (Kb) 43376 [startup+630.063 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 11344 0 2 0 62830 72 0 0 25 0 1 0 1769439873 47280128 11332 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 11543 11332 145 145 0 11398 0 [pid=29735] vsize: 46172 Current children cumulated CPU time (s) 629.03 Current children cumulated vsize (Kb) 48296 [startup+640.063 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 11946 0 2 0 63822 75 0 0 25 0 1 0 1769439873 49770496 11934 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12151 11934 145 145 0 12006 0 [pid=29735] vsize: 48604 Current children cumulated CPU time (s) 638.98 Current children cumulated vsize (Kb) 50728 [startup+650.064 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 11947 0 2 0 64822 75 0 0 25 0 1 0 1769439873 49770496 11935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12151 11935 145 145 0 12006 0 [pid=29735] vsize: 48604 Current children cumulated CPU time (s) 648.98 Current children cumulated vsize (Kb) 50728 [startup+660.063 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 11947 0 2 0 65822 75 0 0 25 0 1 0 1769439873 49770496 11935 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12151 11935 145 145 0 12006 0 [pid=29735] vsize: 48604 Current children cumulated CPU time (s) 658.98 Current children cumulated vsize (Kb) 50728 [startup+670.065 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 11947 0 2 0 66822 75 0 0 25 0 1 0 1769439873 49770496 11935 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12151 11935 145 145 0 12006 0 [pid=29735] vsize: 48604 Current children cumulated CPU time (s) 668.98 Current children cumulated vsize (Kb) 50728 [startup+680.066 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 11947 0 2 0 67823 75 0 0 25 0 1 0 1769439873 49770496 11935 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12151 11935 145 145 0 12006 0 [pid=29735] vsize: 48604 Current children cumulated CPU time (s) 678.99 Current children cumulated vsize (Kb) 50728 [startup+690.067 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 12372 0 2 0 68816 78 0 0 25 0 1 0 1769439873 51511296 12360 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29735/statm): 12576 12360 145 145 0 12431 0 [pid=29735] vsize: 50304 Current children cumulated CPU time (s) 688.95 Current children cumulated vsize (Kb) 52428 [startup+700.068 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 12372 0 2 0 69815 78 0 0 25 0 1 0 1769439873 51511296 12360 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12576 12360 145 145 0 12431 0 [pid=29735] vsize: 50304 Current children cumulated CPU time (s) 698.94 Current children cumulated vsize (Kb) 52428 [startup+710.067 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 12372 0 2 0 70815 78 0 0 25 0 1 0 1769439873 51511296 12360 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12576 12360 145 145 0 12431 0 [pid=29735] vsize: 50304 Current children cumulated CPU time (s) 708.94 Current children cumulated vsize (Kb) 52428 [startup+720.068 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 12372 0 2 0 71816 78 0 0 25 0 1 0 1769439873 51511296 12360 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12576 12360 145 145 0 12431 0 [pid=29735] vsize: 50304 Current children cumulated CPU time (s) 718.95 Current children cumulated vsize (Kb) 52428 [startup+730.069 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 12372 0 2 0 72816 78 0 0 25 0 1 0 1769439873 51511296 12360 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12576 12360 145 145 0 12431 0 [pid=29735] vsize: 50304 Current children cumulated CPU time (s) 728.95 Current children cumulated vsize (Kb) 52428 [startup+740.069 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 12372 0 2 0 73816 78 0 0 25 0 1 0 1769439873 51511296 12360 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12576 12360 145 145 0 12431 0 [pid=29735] vsize: 50304 Current children cumulated CPU time (s) 738.95 Current children cumulated vsize (Kb) 52428 [startup+750.069 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 12372 0 2 0 74816 78 0 0 25 0 1 0 1769439873 51511296 12360 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12576 12360 145 145 0 12431 0 [pid=29735] vsize: 50304 Current children cumulated CPU time (s) 748.95 Current children cumulated vsize (Kb) 52428 [startup+760.07 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 12372 0 2 0 75816 78 0 0 25 0 1 0 1769439873 51511296 12360 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12576 12360 145 145 0 12431 0 [pid=29735] vsize: 50304 Current children cumulated CPU time (s) 758.95 Current children cumulated vsize (Kb) 52428 [startup+770.071 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 12372 0 2 0 76817 78 0 0 25 0 1 0 1769439873 51511296 12360 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 12576 12360 145 145 0 12431 0 [pid=29735] vsize: 50304 Current children cumulated CPU time (s) 768.96 Current children cumulated vsize (Kb) 52428 [startup+780.072 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 13052 0 2 0 77805 83 0 0 25 0 1 0 1769439873 54304768 13040 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 13258 13040 145 145 0 13113 0 [pid=29735] vsize: 53032 Current children cumulated CPU time (s) 778.89 Current children cumulated vsize (Kb) 55156 [startup+790.073 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 13407 0 2 0 78800 85 0 0 25 0 1 0 1769439873 55767040 13395 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 13615 13395 145 145 0 13470 0 [pid=29735] vsize: 54460 Current children cumulated CPU time (s) 788.86 Current children cumulated vsize (Kb) 56584 [startup+800.073 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 13407 0 2 0 79800 85 0 0 25 0 1 0 1769439873 55767040 13395 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 13615 13395 145 145 0 13470 0 [pid=29735] vsize: 54460 Current children cumulated CPU time (s) 798.86 Current children cumulated vsize (Kb) 56584 [startup+810.073 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 13407 0 2 0 80799 86 0 0 25 0 1 0 1769439873 55767040 13395 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 13615 13395 145 145 0 13470 0 [pid=29735] vsize: 54460 Current children cumulated CPU time (s) 808.86 Current children cumulated vsize (Kb) 56584 [startup+820.074 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 13408 0 2 0 81799 86 0 0 25 0 1 0 1769439873 55767040 13396 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 13615 13396 145 145 0 13470 0 [pid=29735] vsize: 54460 Current children cumulated CPU time (s) 818.86 Current children cumulated vsize (Kb) 56584 [startup+830.076 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 13696 0 2 0 82795 89 0 0 25 0 1 0 1769439873 56946688 13684 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 13903 13684 145 145 0 13758 0 [pid=29735] vsize: 55612 Current children cumulated CPU time (s) 828.85 Current children cumulated vsize (Kb) 57736 [startup+840.076 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 83781 95 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 838.77 Current children cumulated vsize (Kb) 61352 [startup+850.076 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 84781 95 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 848.77 Current children cumulated vsize (Kb) 61352 [startup+860.077 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 85781 95 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 858.77 Current children cumulated vsize (Kb) 61352 [startup+870.078 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 86782 95 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 868.78 Current children cumulated vsize (Kb) 61352 [startup+880.079 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 87782 95 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 878.78 Current children cumulated vsize (Kb) 61352 [startup+890.078 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 88782 95 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 888.78 Current children cumulated vsize (Kb) 61352 [startup+900.079 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 89782 95 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 898.78 Current children cumulated vsize (Kb) 61352 [startup+910.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 90782 95 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 908.78 Current children cumulated vsize (Kb) 61352 [startup+920.081 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 91782 96 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 918.79 Current children cumulated vsize (Kb) 61352 [startup+930.082 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 92783 96 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 928.8 Current children cumulated vsize (Kb) 61352 [startup+940.081 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14600 0 2 0 93782 96 0 0 25 0 1 0 1769439873 60649472 14588 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14588 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 938.79 Current children cumulated vsize (Kb) 61352 [startup+950.082 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 94782 96 0 0 25 0 1 0 1769439873 60649472 14590 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14590 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 948.79 Current children cumulated vsize (Kb) 61352 [startup+960.082 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 95782 96 0 0 25 0 1 0 1769439873 60649472 14590 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14590 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 958.79 Current children cumulated vsize (Kb) 61352 [startup+970.084 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 96782 96 0 0 25 0 1 0 1769439873 60649472 14590 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14807 14590 145 145 0 14662 0 [pid=29735] vsize: 59228 Current children cumulated CPU time (s) 968.79 Current children cumulated vsize (Kb) 61352 [startup+980.085 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 97783 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 978.8 Current children cumulated vsize (Kb) 61184 [startup+990.084 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 98783 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 988.8 Current children cumulated vsize (Kb) 61184 [startup+1000.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 99783 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 998.8 Current children cumulated vsize (Kb) 61184 [startup+1010.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 100783 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1008.8 Current children cumulated vsize (Kb) 61184 [startup+1020.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 101783 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1018.8 Current children cumulated vsize (Kb) 61184 [startup+1030.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 102783 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1028.8 Current children cumulated vsize (Kb) 61184 [startup+1040.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 103784 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1038.81 Current children cumulated vsize (Kb) 61184 [startup+1050.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 104784 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1048.81 Current children cumulated vsize (Kb) 61184 [startup+1060.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 105784 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1058.81 Current children cumulated vsize (Kb) 61184 [startup+1070.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 106784 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1068.81 Current children cumulated vsize (Kb) 61184 [startup+1080.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 107785 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1078.82 Current children cumulated vsize (Kb) 61184 [startup+1090.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 108785 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1088.82 Current children cumulated vsize (Kb) 61184 [startup+1100.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14602 0 2 0 109785 96 0 0 25 0 1 0 1769439873 60477440 14548 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14548 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1098.82 Current children cumulated vsize (Kb) 61184 [startup+1110.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14603 0 2 0 110785 96 0 0 25 0 1 0 1769439873 60477440 14549 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14549 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1108.82 Current children cumulated vsize (Kb) 61184 [startup+1120.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14603 0 2 0 111785 96 0 0 25 0 1 0 1769439873 60477440 14549 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14549 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1118.82 Current children cumulated vsize (Kb) 61184 [startup+1130.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14603 0 2 0 112786 96 0 0 25 0 1 0 1769439873 60477440 14549 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14549 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1128.83 Current children cumulated vsize (Kb) 61184 [startup+1140.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14603 0 2 0 113786 96 0 0 25 0 1 0 1769439873 60477440 14549 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14549 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1138.83 Current children cumulated vsize (Kb) 61184 [startup+1150.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14604 0 2 0 114786 97 0 0 25 0 1 0 1769439873 60477440 14550 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14550 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1148.84 Current children cumulated vsize (Kb) 61184 [startup+1160.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14604 0 2 0 115786 97 0 0 25 0 1 0 1769439873 60477440 14550 4294967295 134512640 135094434 3221224432 3221223024 134557363 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14550 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1158.84 Current children cumulated vsize (Kb) 61184 [startup+1170.1 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14604 0 2 0 116786 97 0 0 25 0 1 0 1769439873 60477440 14550 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14550 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1168.84 Current children cumulated vsize (Kb) 61184 [startup+1180.1 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14604 0 2 0 117787 97 0 0 25 0 1 0 1769439873 60477440 14550 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14550 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1178.85 Current children cumulated vsize (Kb) 61184 [startup+1190.1 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14604 0 2 0 118787 97 0 0 25 0 1 0 1769439873 60477440 14550 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14550 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1188.85 Current children cumulated vsize (Kb) 61184 [startup+1200.1 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14604 0 2 0 119787 97 0 0 25 0 1 0 1769439873 60477440 14550 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14550 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1198.85 Current children cumulated vsize (Kb) 61184 [startup+1210.1 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14604 0 2 0 120787 97 0 0 25 0 1 0 1769439873 60477440 14550 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14550 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1208.85 Current children cumulated vsize (Kb) 61184 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 29735 Raw data (/proc/29731/stat): 29731 (minisat+_script) S 29730 29731 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1769439868 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29731/statm): 531 226 485 147 0 384 0 [pid=29731] vsize: 2124 Raw data (/proc/29735/stat): 29735 (minisat+_64-bit) R 29731 29731 27660 0 -1 0 14604 0 2 0 120787 97 0 0 25 0 1 0 1769439873 60477440 14550 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29735/statm): 14765 14550 145 145 0 14620 0 [pid=29735] vsize: 59060 Current children cumulated CPU time (s) 1208.85 Current children cumulated vsize (Kb) 61184 Sending SIGTERM to -29731 Sleeping 2 seconds One traced child (pid=29731) ended because it received signal 15 (SIGTERM) One traced child (pid=29735) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1208.88 CPU user time (s): 1207.88 CPU system time (s): 0.996848 CPU usage (%): 99.8964 Max. virtual memory (cumulated for all children) (Kb): 61352
ERROR: no interpretation found !