Name | submitted/manquinho/primes-dimacs-cnf/normalized-par32-1.opb |
MD5SUM | 64e81a7b23abbb8a6da4e2377ea69dee |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 6352 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 6352 |
Number of bits of the sum of numbers in the objective function | 13 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 6352 |
Number of bits of the biggest sum of numbers | 13 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 6352 |
Total number of constraints | 13453 |
Number of constraints which are clauses | 13453 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 3 |
LAUNCH ON wulflinc8 THE 2005-09-18 15:30:13 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2535 boxname=wulflinc8 idbench=191 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 64e81a7b23abbb8a6da4e2377ea69dee /oldhome/oroussel/tmp/wulflinc8/normalized-par32-1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-par32-1.opb IDLAUNCH: 2535 /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: 921720 kB Buffers: 34260 kB Cached: 53824 kB SwapCached: 792 kB Active: 63848 kB Inactive: 26880 kB HighTotal: 131008 kB HighFree: 73388 kB LowTotal: 903652 kB LowFree: 848332 kB SwapTotal: 2097136 kB SwapFree: 2095876 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5752 kB Slab: 16600 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 15:50:14 (client local time) WITH STATUS 0 IN 1200.17 SECONDS stats: 2535 7 1200.17 0
c Parsing PB file... c Converting 13039 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 9878 24638 | 3292 0 0 nan | 0.000 % | c | 101 | 9878 24638 | 3621 101 1231 12.2 | 23.867 % | c | 251 | 9878 24638 | 3983 251 5277 21.0 | 23.867 % | c | 476 | 9878 24638 | 4381 476 8655 18.2 | 23.867 % | c | 814 | 9878 24638 | 4819 814 19600 24.1 | 23.867 % | c | 1320 | 9878 24638 | 5301 1320 27899 21.1 | 23.867 % | c | 2082 | 9878 24638 | 5831 2082 57645 27.7 | 23.867 % | c | 3221 | 9878 24638 | 6415 3221 93388 29.0 | 23.867 % | c | 4931 | 9878 24638 | 7056 4931 143848 29.2 | 23.867 % | c | 7493 | 9878 24638 | 7762 7493 210661 28.1 | 23.867 % | c | 11338 | 9878 24638 | 8538 6644 169658 25.5 | 23.867 % | c | 17105 | 9878 24638 | 9392 7285 177959 24.4 | 23.867 % | c | 25754 | 9878 24638 | 10331 10409 254945 24.5 | 23.867 % | c | 38729 | 9878 24638 | 11364 11455 286759 25.0 | 23.867 % | c | 58191 | 9878 24638 | 12501 11386 282530 24.8 | 23.867 % | c | 87384 | 9878 24638 | 13751 12309 296202 24.1 | 23.867 % | c | 131173 | 9868 24616 | 15126 10027 237728 23.7 | 23.929 % | c | 196858 | 9868 24616 | 16639 8659 223250 25.8 | 23.929 % | c | 295384 | 9868 24616 | 18303 16056 367503 22.9 | 23.929 % | c | 443174 | 9868 24616 | 20133 14387 321561 22.4 | 23.929 % |
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/1456/stat): 1456 (minisat+_script) R 1455 1456 27660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1770554224 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/1456/statm): 174 3 169 147 0 27 0 [pid=1456] 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=1457 New process pid=1458 New process pid=1459 execve syscall for /bin/sed executable One traced child (pid=1458) 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=1459) exited with status: 0 One traced child (pid=1457) exited with status: 0 New process pid=1460 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-par32-1.opb [startup+10.0037 s] Raw data (loadavg): 0.80 0.90 0.89 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 986 5 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 9.91 Current children cumulated vsize (Kb) 7628 [startup+20.0055 s] Raw data (loadavg): 0.83 0.91 0.89 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 1986 5 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 19.91 Current children cumulated vsize (Kb) 7628 [startup+30.0073 s] Raw data (loadavg): 0.85 0.91 0.89 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 2985 5 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223040 134556999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 29.9 Current children cumulated vsize (Kb) 7628 [startup+40.008 s] Raw data (loadavg): 0.88 0.91 0.89 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 3985 5 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 39.9 Current children cumulated vsize (Kb) 7628 [startup+50.0098 s] Raw data (loadavg): 0.89 0.91 0.89 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 4985 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 49.91 Current children cumulated vsize (Kb) 7628 [startup+60.0106 s] Raw data (loadavg): 0.91 0.92 0.89 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 5985 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 59.91 Current children cumulated vsize (Kb) 7628 [startup+70.0124 s] Raw data (loadavg): 0.92 0.92 0.89 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 6986 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 69.92 Current children cumulated vsize (Kb) 7628 [startup+80.0142 s] Raw data (loadavg): 0.93 0.92 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 7986 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 79.92 Current children cumulated vsize (Kb) 7628 [startup+90.0149 s] Raw data (loadavg): 0.94 0.92 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 8986 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 89.92 Current children cumulated vsize (Kb) 7628 [startup+100.016 s] Raw data (loadavg): 0.95 0.92 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 9986 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 99.92 Current children cumulated vsize (Kb) 7628 [startup+110.017 s] Raw data (loadavg): 0.96 0.93 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 10987 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 109.93 Current children cumulated vsize (Kb) 7628 [startup+120.017 s] Raw data (loadavg): 0.97 0.93 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 11987 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 119.93 Current children cumulated vsize (Kb) 7628 [startup+130.018 s] Raw data (loadavg): 0.97 0.93 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 12987 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 129.93 Current children cumulated vsize (Kb) 7628 [startup+140.019 s] Raw data (loadavg): 0.97 0.93 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 13987 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 139.93 Current children cumulated vsize (Kb) 7628 [startup+150.02 s] Raw data (loadavg): 0.98 0.93 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 14988 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223040 134557232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 149.94 Current children cumulated vsize (Kb) 7628 [startup+160.02 s] Raw data (loadavg): 0.98 0.93 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 15988 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 159.94 Current children cumulated vsize (Kb) 7628 [startup+170.021 s] Raw data (loadavg): 0.98 0.94 0.90 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1327 0 0 0 16988 6 0 0 25 0 1 0 1770554229 5636096 1276 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1376 1276 145 145 0 1231 0 [pid=1460] vsize: 5504 Current children cumulated CPU time (s) 169.94 Current children cumulated vsize (Kb) 7628 [startup+180.022 s] Raw data (loadavg): 0.98 0.94 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1335 0 0 0 17988 6 0 0 25 0 1 0 1770554229 5668864 1284 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1384 1284 145 145 0 1239 0 [pid=1460] vsize: 5536 Current children cumulated CPU time (s) 179.94 Current children cumulated vsize (Kb) 7660 [startup+190.023 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1342 0 0 0 18989 6 0 0 25 0 1 0 1770554229 5701632 1291 4294967295 134512640 135094434 3221224448 3221223072 134562131 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1392 1291 145 145 0 1247 0 [pid=1460] vsize: 5568 Current children cumulated CPU time (s) 189.95 Current children cumulated vsize (Kb) 7692 [startup+200.024 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1370 0 0 0 19988 6 0 0 25 0 1 0 1770554229 5832704 1319 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1424 1319 145 145 0 1279 0 [pid=1460] vsize: 5696 Current children cumulated CPU time (s) 199.94 Current children cumulated vsize (Kb) 7820 [startup+210.023 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1374 0 0 0 20989 6 0 0 25 0 1 0 1770554229 5849088 1323 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1428 1323 145 145 0 1283 0 [pid=1460] vsize: 5712 Current children cumulated CPU time (s) 209.95 Current children cumulated vsize (Kb) 7836 [startup+220.025 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1381 0 0 0 21989 6 0 0 25 0 1 0 1770554229 5898240 1330 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1440 1330 145 145 0 1295 0 [pid=1460] vsize: 5760 Current children cumulated CPU time (s) 219.95 Current children cumulated vsize (Kb) 7884 [startup+230.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1387 0 0 0 22989 6 0 0 25 0 1 0 1770554229 5931008 1336 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1448 1336 145 145 0 1303 0 [pid=1460] vsize: 5792 Current children cumulated CPU time (s) 229.95 Current children cumulated vsize (Kb) 7916 [startup+240.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1405 0 0 0 23989 6 0 0 25 0 1 0 1770554229 5992448 1354 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1463 1354 145 145 0 1318 0 [pid=1460] vsize: 5852 Current children cumulated CPU time (s) 239.95 Current children cumulated vsize (Kb) 7976 [startup+250.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1414 0 0 0 24989 6 0 0 25 0 1 0 1770554229 6057984 1363 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1479 1363 145 145 0 1334 0 [pid=1460] vsize: 5916 Current children cumulated CPU time (s) 249.95 Current children cumulated vsize (Kb) 8040 [startup+260.027 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1419 0 0 0 25989 6 0 0 25 0 1 0 1770554229 6074368 1368 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1483 1368 145 145 0 1338 0 [pid=1460] vsize: 5932 Current children cumulated CPU time (s) 259.95 Current children cumulated vsize (Kb) 8056 [startup+270.028 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1420 0 0 0 26989 6 0 0 25 0 1 0 1770554229 6074368 1369 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1483 1369 145 145 0 1338 0 [pid=1460] vsize: 5932 Current children cumulated CPU time (s) 269.95 Current children cumulated vsize (Kb) 8056 [startup+280.029 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1423 0 0 0 27989 6 0 0 25 0 1 0 1770554229 6090752 1372 4294967295 134512640 135094434 3221224448 3221223072 134562101 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1487 1372 145 145 0 1342 0 [pid=1460] vsize: 5948 Current children cumulated CPU time (s) 279.95 Current children cumulated vsize (Kb) 8072 [startup+290.03 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1500 0 0 0 28988 7 0 0 25 0 1 0 1770554229 6463488 1449 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1578 1449 145 145 0 1433 0 [pid=1460] vsize: 6312 Current children cumulated CPU time (s) 289.95 Current children cumulated vsize (Kb) 8436 [startup+300.03 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1510 0 0 0 29988 7 0 0 25 0 1 0 1770554229 6512640 1459 4294967295 134512640 135094434 3221224448 3221223040 134556993 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1590 1459 145 145 0 1445 0 [pid=1460] vsize: 6360 Current children cumulated CPU time (s) 299.95 Current children cumulated vsize (Kb) 8484 [startup+310.031 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1544 0 0 0 30988 7 0 0 25 0 1 0 1770554229 6660096 1493 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1626 1493 145 145 0 1481 0 [pid=1460] vsize: 6504 Current children cumulated CPU time (s) 309.95 Current children cumulated vsize (Kb) 8628 [startup+320.033 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1551 0 0 0 31988 7 0 0 25 0 1 0 1770554229 6692864 1500 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1634 1500 145 145 0 1489 0 [pid=1460] vsize: 6536 Current children cumulated CPU time (s) 319.95 Current children cumulated vsize (Kb) 8660 [startup+330.034 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1560 0 0 0 32988 7 0 0 25 0 1 0 1770554229 6729728 1509 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1509 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 329.95 Current children cumulated vsize (Kb) 8696 [startup+340.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1560 0 0 0 33989 7 0 0 25 0 1 0 1770554229 6729728 1509 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1509 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 339.96 Current children cumulated vsize (Kb) 8696 [startup+350.035 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1560 0 0 0 34989 7 0 0 25 0 1 0 1770554229 6729728 1509 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1509 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 349.96 Current children cumulated vsize (Kb) 8696 [startup+360.036 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1560 0 0 0 35989 7 0 0 25 0 1 0 1770554229 6729728 1509 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1509 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 359.96 Current children cumulated vsize (Kb) 8696 [startup+370.037 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1560 0 0 0 36989 7 0 0 25 0 1 0 1770554229 6729728 1509 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1509 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 369.96 Current children cumulated vsize (Kb) 8696 [startup+380.038 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1560 0 0 0 37989 7 0 0 25 0 1 0 1770554229 6729728 1509 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1509 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 379.96 Current children cumulated vsize (Kb) 8696 [startup+390.038 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1560 0 0 0 38990 7 0 0 25 0 1 0 1770554229 6729728 1509 4294967295 134512640 135094434 3221224448 3221223072 134557645 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1509 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 389.97 Current children cumulated vsize (Kb) 8696 [startup+400.039 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1561 0 0 0 39990 7 0 0 25 0 1 0 1770554229 6729728 1510 4294967295 134512640 135094434 3221224448 3221223120 134555323 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1510 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 399.97 Current children cumulated vsize (Kb) 8696 [startup+410.04 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1561 0 0 0 40990 7 0 0 25 0 1 0 1770554229 6729728 1510 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1510 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 409.97 Current children cumulated vsize (Kb) 8696 [startup+420.041 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1562 0 0 0 41990 7 0 0 25 0 1 0 1770554229 6729728 1511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1511 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 419.97 Current children cumulated vsize (Kb) 8696 [startup+430.042 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1563 0 0 0 42990 8 0 0 25 0 1 0 1770554229 6729728 1512 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1512 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 429.98 Current children cumulated vsize (Kb) 8696 [startup+440.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1563 0 0 0 43990 8 0 0 25 0 1 0 1770554229 6729728 1512 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1643 1512 145 145 0 1498 0 [pid=1460] vsize: 6572 Current children cumulated CPU time (s) 439.98 Current children cumulated vsize (Kb) 8696 [startup+450.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1580 0 0 0 44991 8 0 0 25 0 1 0 1770554229 6795264 1529 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1659 1529 145 145 0 1514 0 [pid=1460] vsize: 6636 Current children cumulated CPU time (s) 449.99 Current children cumulated vsize (Kb) 8760 [startup+460.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1586 0 0 0 45990 9 0 0 25 0 1 0 1770554229 6844416 1535 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1671 1535 145 145 0 1526 0 [pid=1460] vsize: 6684 Current children cumulated CPU time (s) 459.99 Current children cumulated vsize (Kb) 8808 [startup+470.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1591 0 0 0 46990 9 0 0 25 0 1 0 1770554229 6860800 1540 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1675 1540 145 145 0 1530 0 [pid=1460] vsize: 6700 Current children cumulated CPU time (s) 469.99 Current children cumulated vsize (Kb) 8824 [startup+480.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1591 0 0 0 47990 9 0 0 25 0 1 0 1770554229 6860800 1540 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1675 1540 145 145 0 1530 0 [pid=1460] vsize: 6700 Current children cumulated CPU time (s) 479.99 Current children cumulated vsize (Kb) 8824 [startup+490.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1592 0 0 0 48990 9 0 0 25 0 1 0 1770554229 6860800 1541 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1675 1541 145 145 0 1530 0 [pid=1460] vsize: 6700 Current children cumulated CPU time (s) 489.99 Current children cumulated vsize (Kb) 8824 [startup+500.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1604 0 0 0 49991 9 0 0 25 0 1 0 1770554229 6926336 1553 4294967295 134512640 135094434 3221224448 3221223120 134556327 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1691 1553 145 145 0 1546 0 [pid=1460] vsize: 6764 Current children cumulated CPU time (s) 500 Current children cumulated vsize (Kb) 8888 [startup+510.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1605 0 0 0 50991 9 0 0 25 0 1 0 1770554229 6926336 1554 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1691 1554 145 145 0 1546 0 [pid=1460] vsize: 6764 Current children cumulated CPU time (s) 510 Current children cumulated vsize (Kb) 8888 [startup+520.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1605 0 0 0 51991 9 0 0 25 0 1 0 1770554229 6926336 1554 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1691 1554 145 145 0 1546 0 [pid=1460] vsize: 6764 Current children cumulated CPU time (s) 520 Current children cumulated vsize (Kb) 8888 [startup+530.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1611 0 0 0 52991 9 0 0 25 0 1 0 1770554229 6959104 1560 4294967295 134512640 135094434 3221224448 3221223040 134556791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1699 1560 145 145 0 1554 0 [pid=1460] vsize: 6796 Current children cumulated CPU time (s) 530 Current children cumulated vsize (Kb) 8920 [startup+540.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1612 0 0 0 53991 9 0 0 25 0 1 0 1770554229 6959104 1561 4294967295 134512640 135094434 3221224448 3221223060 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1699 1561 145 145 0 1554 0 [pid=1460] vsize: 6796 Current children cumulated CPU time (s) 540 Current children cumulated vsize (Kb) 8920 [startup+550.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1613 0 0 0 54991 9 0 0 25 0 1 0 1770554229 6959104 1562 4294967295 134512640 135094434 3221224448 3221223120 134555570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1699 1562 145 145 0 1554 0 [pid=1460] vsize: 6796 Current children cumulated CPU time (s) 550 Current children cumulated vsize (Kb) 8920 [startup+560.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1613 0 0 0 55991 9 0 0 25 0 1 0 1770554229 6959104 1562 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1699 1562 145 145 0 1554 0 [pid=1460] vsize: 6796 Current children cumulated CPU time (s) 560 Current children cumulated vsize (Kb) 8920 [startup+570.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1613 0 0 0 56992 9 0 0 25 0 1 0 1770554229 6959104 1562 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1699 1562 145 145 0 1554 0 [pid=1460] vsize: 6796 Current children cumulated CPU time (s) 570.01 Current children cumulated vsize (Kb) 8920 [startup+580.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1613 0 0 0 57992 9 0 0 25 0 1 0 1770554229 6959104 1562 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1699 1562 145 145 0 1554 0 [pid=1460] vsize: 6796 Current children cumulated CPU time (s) 580.01 Current children cumulated vsize (Kb) 8920 [startup+590.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1613 0 0 0 58992 9 0 0 25 0 1 0 1770554229 6959104 1562 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1699 1562 145 145 0 1554 0 [pid=1460] vsize: 6796 Current children cumulated CPU time (s) 590.01 Current children cumulated vsize (Kb) 8920 [startup+600.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1618 0 0 0 59993 9 0 0 25 0 1 0 1770554229 6991872 1567 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1707 1567 145 145 0 1562 0 [pid=1460] vsize: 6828 Current children cumulated CPU time (s) 600.02 Current children cumulated vsize (Kb) 8952 [startup+610.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1619 0 0 0 60993 9 0 0 25 0 1 0 1770554229 6991872 1568 4294967295 134512640 135094434 3221224448 3221223120 134555579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1707 1568 145 145 0 1562 0 [pid=1460] vsize: 6828 Current children cumulated CPU time (s) 610.02 Current children cumulated vsize (Kb) 8952 [startup+620.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1619 0 0 0 61993 9 0 0 25 0 1 0 1770554229 6991872 1568 4294967295 134512640 135094434 3221224448 3221223040 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1707 1568 145 145 0 1562 0 [pid=1460] vsize: 6828 Current children cumulated CPU time (s) 620.02 Current children cumulated vsize (Kb) 8952 [startup+630.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1619 0 0 0 62993 9 0 0 25 0 1 0 1770554229 6991872 1568 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1707 1568 145 145 0 1562 0 [pid=1460] vsize: 6828 Current children cumulated CPU time (s) 630.02 Current children cumulated vsize (Kb) 8952 [startup+640.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1620 0 0 0 63993 9 0 0 25 0 1 0 1770554229 6991872 1569 4294967295 134512640 135094434 3221224448 3221223136 134554715 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1707 1569 145 145 0 1562 0 [pid=1460] vsize: 6828 Current children cumulated CPU time (s) 640.02 Current children cumulated vsize (Kb) 8952 [startup+650.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1622 0 0 0 64993 9 0 0 25 0 1 0 1770554229 6991872 1571 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1707 1571 145 145 0 1562 0 [pid=1460] vsize: 6828 Current children cumulated CPU time (s) 650.02 Current children cumulated vsize (Kb) 8952 [startup+660.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1622 0 0 0 65993 9 0 0 25 0 1 0 1770554229 6991872 1571 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1707 1571 145 145 0 1562 0 [pid=1460] vsize: 6828 Current children cumulated CPU time (s) 660.02 Current children cumulated vsize (Kb) 8952 [startup+670.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1622 0 0 0 66994 9 0 0 25 0 1 0 1770554229 6991872 1571 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1707 1571 145 145 0 1562 0 [pid=1460] vsize: 6828 Current children cumulated CPU time (s) 670.03 Current children cumulated vsize (Kb) 8952 [startup+680.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1622 0 0 0 67994 9 0 0 25 0 1 0 1770554229 6991872 1571 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1707 1571 145 145 0 1562 0 [pid=1460] vsize: 6828 Current children cumulated CPU time (s) 680.03 Current children cumulated vsize (Kb) 8952 [startup+690.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1632 0 0 0 68994 9 0 0 25 0 1 0 1770554229 7057408 1581 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1723 1581 145 145 0 1578 0 [pid=1460] vsize: 6892 Current children cumulated CPU time (s) 690.03 Current children cumulated vsize (Kb) 9016 [startup+700.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1632 0 0 0 69994 9 0 0 25 0 1 0 1770554229 7057408 1581 4294967295 134512640 135094434 3221224448 3221223088 134562076 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1723 1581 145 145 0 1578 0 [pid=1460] vsize: 6892 Current children cumulated CPU time (s) 700.03 Current children cumulated vsize (Kb) 9016 [startup+710.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1634 0 0 0 70994 9 0 0 25 0 1 0 1770554229 7057408 1583 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1723 1583 145 145 0 1578 0 [pid=1460] vsize: 6892 Current children cumulated CPU time (s) 710.03 Current children cumulated vsize (Kb) 9016 [startup+720.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1644 0 0 0 71994 9 0 0 25 0 1 0 1770554229 7122944 1593 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1739 1593 145 145 0 1594 0 [pid=1460] vsize: 6956 Current children cumulated CPU time (s) 720.03 Current children cumulated vsize (Kb) 9080 [startup+730.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1644 0 0 0 72994 9 0 0 25 0 1 0 1770554229 7122944 1593 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1739 1593 145 145 0 1594 0 [pid=1460] vsize: 6956 Current children cumulated CPU time (s) 730.03 Current children cumulated vsize (Kb) 9080 [startup+740.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1644 0 0 0 73995 9 0 0 25 0 1 0 1770554229 7122944 1593 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1739 1593 145 145 0 1594 0 [pid=1460] vsize: 6956 Current children cumulated CPU time (s) 740.04 Current children cumulated vsize (Kb) 9080 [startup+750.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1644 0 0 0 74995 9 0 0 25 0 1 0 1770554229 7122944 1593 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1739 1593 145 145 0 1594 0 [pid=1460] vsize: 6956 Current children cumulated CPU time (s) 750.04 Current children cumulated vsize (Kb) 9080 [startup+760.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1644 0 0 0 75995 9 0 0 25 0 1 0 1770554229 7122944 1593 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1739 1593 145 145 0 1594 0 [pid=1460] vsize: 6956 Current children cumulated CPU time (s) 760.04 Current children cumulated vsize (Kb) 9080 [startup+770.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1644 0 0 0 76995 9 0 0 25 0 1 0 1770554229 7122944 1593 4294967295 134512640 135094434 3221224448 3221223040 134557391 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1739 1593 145 145 0 1594 0 [pid=1460] vsize: 6956 Current children cumulated CPU time (s) 770.04 Current children cumulated vsize (Kb) 9080 [startup+780.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1645 0 0 0 77996 9 0 0 25 0 1 0 1770554229 7122944 1594 4294967295 134512640 135094434 3221224448 3221223120 134556473 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1739 1594 145 145 0 1594 0 [pid=1460] vsize: 6956 Current children cumulated CPU time (s) 780.05 Current children cumulated vsize (Kb) 9080 [startup+790.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1645 0 0 0 78996 9 0 0 25 0 1 0 1770554229 7122944 1594 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1739 1594 145 145 0 1594 0 [pid=1460] vsize: 6956 Current children cumulated CPU time (s) 790.05 Current children cumulated vsize (Kb) 9080 [startup+800.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1645 0 0 0 79996 9 0 0 25 0 1 0 1770554229 7122944 1594 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1739 1594 145 145 0 1594 0 [pid=1460] vsize: 6956 Current children cumulated CPU time (s) 800.05 Current children cumulated vsize (Kb) 9080 [startup+810.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1655 0 0 0 80996 9 0 0 25 0 1 0 1770554229 7188480 1604 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1755 1604 145 145 0 1610 0 [pid=1460] vsize: 7020 Current children cumulated CPU time (s) 810.05 Current children cumulated vsize (Kb) 9144 [startup+820.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1655 0 0 0 81997 9 0 0 25 0 1 0 1770554229 7188480 1604 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1755 1604 145 145 0 1610 0 [pid=1460] vsize: 7020 Current children cumulated CPU time (s) 820.06 Current children cumulated vsize (Kb) 9144 [startup+830.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1655 0 0 0 82997 9 0 0 25 0 1 0 1770554229 7188480 1604 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1755 1604 145 145 0 1610 0 [pid=1460] vsize: 7020 Current children cumulated CPU time (s) 830.06 Current children cumulated vsize (Kb) 9144 [startup+840.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1655 0 0 0 83997 9 0 0 25 0 1 0 1770554229 7188480 1604 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1755 1604 145 145 0 1610 0 [pid=1460] vsize: 7020 Current children cumulated CPU time (s) 840.06 Current children cumulated vsize (Kb) 9144 [startup+850.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1655 0 0 0 84998 9 0 0 25 0 1 0 1770554229 7188480 1604 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1755 1604 145 145 0 1610 0 [pid=1460] vsize: 7020 Current children cumulated CPU time (s) 850.07 Current children cumulated vsize (Kb) 9144 [startup+860.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1655 0 0 0 85998 9 0 0 25 0 1 0 1770554229 7188480 1604 4294967295 134512640 135094434 3221224448 3221223136 134554728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1755 1604 145 145 0 1610 0 [pid=1460] vsize: 7020 Current children cumulated CPU time (s) 860.07 Current children cumulated vsize (Kb) 9144 [startup+870.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1662 0 0 0 86998 9 0 0 25 0 1 0 1770554229 7221248 1611 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1763 1611 145 145 0 1618 0 [pid=1460] vsize: 7052 Current children cumulated CPU time (s) 870.07 Current children cumulated vsize (Kb) 9176 [startup+880.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1663 0 0 0 87998 9 0 0 25 0 1 0 1770554229 7221248 1612 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1763 1612 145 145 0 1618 0 [pid=1460] vsize: 7052 Current children cumulated CPU time (s) 880.07 Current children cumulated vsize (Kb) 9176 [startup+890.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1663 0 0 0 88999 9 0 0 25 0 1 0 1770554229 7221248 1612 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1763 1612 145 145 0 1618 0 [pid=1460] vsize: 7052 Current children cumulated CPU time (s) 890.08 Current children cumulated vsize (Kb) 9176 [startup+900.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1663 0 0 0 89999 9 0 0 25 0 1 0 1770554229 7221248 1612 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1763 1612 145 145 0 1618 0 [pid=1460] vsize: 7052 Current children cumulated CPU time (s) 900.08 Current children cumulated vsize (Kb) 9176 [startup+910.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1669 0 0 0 90999 9 0 0 25 0 1 0 1770554229 7254016 1618 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1771 1618 145 145 0 1626 0 [pid=1460] vsize: 7084 Current children cumulated CPU time (s) 910.08 Current children cumulated vsize (Kb) 9208 [startup+920.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1670 0 0 0 91999 9 0 0 25 0 1 0 1770554229 7254016 1619 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1771 1619 145 145 0 1626 0 [pid=1460] vsize: 7084 Current children cumulated CPU time (s) 920.08 Current children cumulated vsize (Kb) 9208 [startup+930.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1670 0 0 0 93000 9 0 0 25 0 1 0 1770554229 7254016 1619 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1771 1619 145 145 0 1626 0 [pid=1460] vsize: 7084 Current children cumulated CPU time (s) 930.09 Current children cumulated vsize (Kb) 9208 [startup+940.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1672 0 0 0 94000 9 0 0 25 0 1 0 1770554229 7254016 1621 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1771 1621 145 145 0 1626 0 [pid=1460] vsize: 7084 Current children cumulated CPU time (s) 940.09 Current children cumulated vsize (Kb) 9208 [startup+950.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1682 0 0 0 95000 9 0 0 25 0 1 0 1770554229 7319552 1631 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1787 1631 145 145 0 1642 0 [pid=1460] vsize: 7148 Current children cumulated CPU time (s) 950.09 Current children cumulated vsize (Kb) 9272 [startup+960.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1683 0 0 0 96000 9 0 0 25 0 1 0 1770554229 7319552 1632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1787 1632 145 145 0 1642 0 [pid=1460] vsize: 7148 Current children cumulated CPU time (s) 960.09 Current children cumulated vsize (Kb) 9272 [startup+970.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1692 0 0 0 97001 9 0 0 25 0 1 0 1770554229 7385088 1641 4294967295 134512640 135094434 3221224448 3221223072 134557577 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1803 1641 145 145 0 1658 0 [pid=1460] vsize: 7212 Current children cumulated CPU time (s) 970.1 Current children cumulated vsize (Kb) 9336 [startup+980.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1692 0 0 0 98001 9 0 0 25 0 1 0 1770554229 7385088 1641 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1803 1641 145 145 0 1658 0 [pid=1460] vsize: 7212 Current children cumulated CPU time (s) 980.1 Current children cumulated vsize (Kb) 9336 [startup+990.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1700 0 0 0 99001 9 0 0 25 0 1 0 1770554229 7417856 1649 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1811 1649 145 145 0 1666 0 [pid=1460] vsize: 7244 Current children cumulated CPU time (s) 990.1 Current children cumulated vsize (Kb) 9368 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1752 0 0 0 100000 10 0 0 25 0 1 0 1770554229 7622656 1701 4294967295 134512640 135094434 3221224448 3221223120 134555991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1861 1701 145 145 0 1716 0 [pid=1460] vsize: 7444 Current children cumulated CPU time (s) 1000.1 Current children cumulated vsize (Kb) 9568 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1758 0 0 0 101001 10 0 0 25 0 1 0 1770554229 7655424 1707 4294967295 134512640 135094434 3221224448 3221223096 134562167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1869 1707 145 145 0 1724 0 [pid=1460] vsize: 7476 Current children cumulated CPU time (s) 1010.11 Current children cumulated vsize (Kb) 9600 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1770 0 0 0 102001 10 0 0 25 0 1 0 1770554229 7704576 1719 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1881 1719 145 145 0 1736 0 [pid=1460] vsize: 7524 Current children cumulated CPU time (s) 1020.11 Current children cumulated vsize (Kb) 9648 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1773 0 0 0 103001 10 0 0 25 0 1 0 1770554229 7712768 1722 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1883 1722 145 145 0 1738 0 [pid=1460] vsize: 7532 Current children cumulated CPU time (s) 1030.11 Current children cumulated vsize (Kb) 9656 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1773 0 0 0 104001 10 0 0 25 0 1 0 1770554229 7712768 1722 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1883 1722 145 145 0 1738 0 [pid=1460] vsize: 7532 Current children cumulated CPU time (s) 1040.11 Current children cumulated vsize (Kb) 9656 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1779 0 0 0 105001 10 0 0 25 0 1 0 1770554229 7745536 1728 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1891 1728 145 145 0 1746 0 [pid=1460] vsize: 7564 Current children cumulated CPU time (s) 1050.11 Current children cumulated vsize (Kb) 9688 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1779 0 0 0 106001 10 0 0 25 0 1 0 1770554229 7745536 1728 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1891 1728 145 145 0 1746 0 [pid=1460] vsize: 7564 Current children cumulated CPU time (s) 1060.11 Current children cumulated vsize (Kb) 9688 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1779 0 0 0 107002 10 0 0 25 0 1 0 1770554229 7745536 1728 4294967295 134512640 135094434 3221224448 3221223120 134555440 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1891 1728 145 145 0 1746 0 [pid=1460] vsize: 7564 Current children cumulated CPU time (s) 1070.12 Current children cumulated vsize (Kb) 9688 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1784 0 0 0 108002 10 0 0 25 0 1 0 1770554229 7778304 1733 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1899 1733 145 145 0 1754 0 [pid=1460] vsize: 7596 Current children cumulated CPU time (s) 1080.12 Current children cumulated vsize (Kb) 9720 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1784 0 0 0 109002 10 0 0 25 0 1 0 1770554229 7778304 1733 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1899 1733 145 145 0 1754 0 [pid=1460] vsize: 7596 Current children cumulated CPU time (s) 1090.12 Current children cumulated vsize (Kb) 9720 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1784 0 0 0 110002 10 0 0 25 0 1 0 1770554229 7778304 1733 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1899 1733 145 145 0 1754 0 [pid=1460] vsize: 7596 Current children cumulated CPU time (s) 1100.12 Current children cumulated vsize (Kb) 9720 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1789 0 0 0 111003 10 0 0 25 0 1 0 1770554229 7811072 1738 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1907 1738 145 145 0 1762 0 [pid=1460] vsize: 7628 Current children cumulated CPU time (s) 1110.13 Current children cumulated vsize (Kb) 9752 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1790 0 0 0 112003 10 0 0 25 0 1 0 1770554229 7811072 1739 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1907 1739 145 145 0 1762 0 [pid=1460] vsize: 7628 Current children cumulated CPU time (s) 1120.13 Current children cumulated vsize (Kb) 9752 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1790 0 0 0 113003 10 0 0 25 0 1 0 1770554229 7811072 1739 4294967295 134512640 135094434 3221224448 3221223072 134557666 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1907 1739 145 145 0 1762 0 [pid=1460] vsize: 7628 Current children cumulated CPU time (s) 1130.13 Current children cumulated vsize (Kb) 9752 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1791 0 0 0 114003 10 0 0 25 0 1 0 1770554229 7811072 1740 4294967295 134512640 135094434 3221224448 3221223120 134555437 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1907 1740 145 145 0 1762 0 [pid=1460] vsize: 7628 Current children cumulated CPU time (s) 1140.13 Current children cumulated vsize (Kb) 9752 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1791 0 0 0 115004 10 0 0 25 0 1 0 1770554229 7811072 1740 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1907 1740 145 145 0 1762 0 [pid=1460] vsize: 7628 Current children cumulated CPU time (s) 1150.14 Current children cumulated vsize (Kb) 9752 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1801 0 0 0 116004 10 0 0 25 0 1 0 1770554229 7876608 1750 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1923 1750 145 145 0 1778 0 [pid=1460] vsize: 7692 Current children cumulated CPU time (s) 1160.14 Current children cumulated vsize (Kb) 9816 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1801 0 0 0 117004 10 0 0 25 0 1 0 1770554229 7876608 1750 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1923 1750 145 145 0 1778 0 [pid=1460] vsize: 7692 Current children cumulated CPU time (s) 1170.14 Current children cumulated vsize (Kb) 9816 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1801 0 0 0 118004 10 0 0 25 0 1 0 1770554229 7876608 1750 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1923 1750 145 145 0 1778 0 [pid=1460] vsize: 7692 Current children cumulated CPU time (s) 1180.14 Current children cumulated vsize (Kb) 9816 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1801 0 0 0 119005 10 0 0 25 0 1 0 1770554229 7876608 1750 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1923 1750 145 145 0 1778 0 [pid=1460] vsize: 7692 Current children cumulated CPU time (s) 1190.15 Current children cumulated vsize (Kb) 9816 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1801 0 0 0 120005 10 0 0 25 0 1 0 1770554229 7876608 1750 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1923 1750 145 145 0 1778 0 [pid=1460] vsize: 7692 Current children cumulated CPU time (s) 1200.15 Current children cumulated vsize (Kb) 9816 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1460 Raw data (/proc/1456/stat): 1456 (minisat+_script) S 1455 1456 27660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1770554224 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1456/statm): 531 226 485 147 0 384 0 [pid=1456] vsize: 2124 Raw data (/proc/1460/stat): 1460 (minisat+_64-bit) R 1456 1456 27660 0 -1 0 1801 0 0 0 120005 10 0 0 25 0 1 0 1770554229 7876608 1750 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1460/statm): 1923 1750 145 145 0 1778 0 [pid=1460] vsize: 7692 Current children cumulated CPU time (s) 1200.15 Current children cumulated vsize (Kb) 9816 Sending SIGTERM to -1456 Sleeping 2 seconds One traced child (pid=1456) ended because it received signal 15 (SIGTERM) One traced child (pid=1460) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1200.12 CPU time (s): 1200.17 CPU user time (s): 1200.06 CPU system time (s): 0.109983 CPU usage (%): 100.004 Max. virtual memory (cumulated for all children) (Kb): 9816
ERROR: no interpretation found !