Name | submitted/manquinho/primes-dimacs-cnf/normalized-f600.opb |
MD5SUM | 4fdec182582ed31d1ae371090f6cc5c1 |
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 | 1200 |
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 | 1200 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1200 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 1200 |
Total number of constraints | 3150 |
Number of constraints which are clauses | 3150 |
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 | 2 |
Maximum length of a constraint | 3 |
LAUNCH ON wulflinc26 THE 2005-09-18 15:08:58 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2468 boxname=wulflinc26 idbench=124 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4fdec182582ed31d1ae371090f6cc5c1 /oldhome/oroussel/tmp/wulflinc26/normalized-f600.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-f600.opb IDLAUNCH: 2468 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 922624 kB Buffers: 35236 kB Cached: 49644 kB SwapCached: 868 kB Active: 64656 kB Inactive: 22852 kB HighTotal: 131008 kB HighFree: 78624 kB LowTotal: 903652 kB LowFree: 844000 kB SwapTotal: 2097892 kB SwapFree: 2096540 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 18912 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 15:28:58 (client local time) WITH STATUS 0 IN 1200.09 SECONDS stats: 2468 7 1200.09 0
c Parsing PB file... c Converting 3150 PB-constraints to clauses... c -- Unit propagations: (none) 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 | 3150 8850 | 1050 0 0 nan | 0.000 % | c | 102 | 3150 8850 | 1155 102 3292 32.3 | 0.000 % | c | 253 | 3150 8850 | 1270 253 8611 34.0 | 0.000 % | c | 478 | 3150 8850 | 1397 478 15852 33.2 | 0.000 % | c | 817 | 3150 8850 | 1537 817 26836 32.8 | 0.000 % | c | 1324 | 3150 8850 | 1691 1324 41380 31.3 | 0.000 % | c | 2084 | 3150 8850 | 1860 1198 32243 26.9 | 0.000 % | c | 3224 | 3150 8850 | 2046 1363 35898 26.3 | 0.000 % | c | 4932 | 3150 8850 | 2250 2020 52177 25.8 | 0.000 % | c | 7495 | 3150 8850 | 2475 2231 61073 27.4 | 0.000 % | c | 11339 | 3150 8850 | 2723 2199 56842 25.8 | 0.000 % | c | 17106 | 3150 8850 | 2995 2299 59391 25.8 | 0.000 % | c | 25755 | 3150 8850 | 3295 1606 44453 27.7 | 0.000 % | c | 38729 | 3150 8850 | 3624 2649 77155 29.1 | 0.000 % | c | 58190 | 3150 8850 | 3987 3488 99761 28.6 | 0.000 % | c | 87383 | 3150 8850 | 4386 4024 109027 27.1 | 0.000 % | c | 131172 | 3150 8850 | 4824 2806 82033 29.2 | 0.000 % | c | 196857 | 3150 8850 | 5307 4322 119220 27.6 | 0.000 % | c | 295383 | 3150 8850 | 5837 4888 145414 29.7 | 0.000 % | c | 443173 | 3150 8850 | 6421 3557 104634 29.4 | 0.000 % | c | 664858 | 3150 8850 | 7063 5936 187586 31.6 | 0.000 % | c | 997383 | 3150 8850 | 7770 4394 120752 27.5 | 0.000 % | c | 1496174 | 3150 8850 | 8547 6921 191716 27.7 | 0.000 % | c | 2244356 | 3150 8850 | 9402 5643 161794 28.7 | 0.000 % |
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/22043/stat): 22043 (minisat+_script) R 22042 22043 16528 0 -1 0 19 0 0 0 0 0 0 0 20 0 1 0 1842230236 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/22043/statm): 174 3 169 147 0 27 0 [pid=22043] 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=22044 New process pid=22045 New process pid=22046 execve syscall for /bin/sed executable One traced child (pid=22045) 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=22046) exited with status: 0 One traced child (pid=22044) exited with status: 0 New process pid=22047 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-f600.opb [startup+10.0037 s] Raw data (loadavg): 0.83 0.95 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 460 0 0 0 989 3 0 0 25 0 1 0 1842230241 2158592 447 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22047/statm): 527 447 145 145 0 382 0 [pid=22047] vsize: 2108 Current children cumulated CPU time (s) 9.92 Current children cumulated vsize (Kb) 4232 [startup+20.0053 s] Raw data (loadavg): 0.85 0.95 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 513 0 0 0 1988 4 0 0 25 0 1 0 1842230241 2375680 500 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 580 500 145 145 0 435 0 [pid=22047] vsize: 2320 Current children cumulated CPU time (s) 19.92 Current children cumulated vsize (Kb) 4444 [startup+30.007 s] Raw data (loadavg): 0.87 0.95 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 565 0 0 0 2987 4 0 0 25 0 1 0 1842230241 2600960 552 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 635 552 145 145 0 490 0 [pid=22047] vsize: 2540 Current children cumulated CPU time (s) 29.91 Current children cumulated vsize (Kb) 4664 [startup+40.0077 s] Raw data (loadavg): 0.89 0.95 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 613 0 0 0 3987 4 0 0 25 0 1 0 1842230241 2797568 600 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 683 600 145 145 0 538 0 [pid=22047] vsize: 2732 Current children cumulated CPU time (s) 39.91 Current children cumulated vsize (Kb) 4856 [startup+50.0084 s] Raw data (loadavg): 0.91 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 655 0 0 0 4986 5 0 0 25 0 1 0 1842230241 2969600 642 4294967295 134512640 135094434 3221224448 3221223120 134555288 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 725 642 145 145 0 580 0 [pid=22047] vsize: 2900 Current children cumulated CPU time (s) 49.91 Current children cumulated vsize (Kb) 5024 [startup+60.0091 s] Raw data (loadavg): 0.92 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 694 0 0 0 5986 5 0 0 25 0 1 0 1842230241 3125248 681 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 763 681 145 145 0 618 0 [pid=22047] vsize: 3052 Current children cumulated CPU time (s) 59.91 Current children cumulated vsize (Kb) 5176 [startup+70.0097 s] Raw data (loadavg): 0.93 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 714 0 0 0 6985 5 0 0 25 0 1 0 1842230241 3207168 701 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 783 701 145 145 0 638 0 [pid=22047] vsize: 3132 Current children cumulated CPU time (s) 69.9 Current children cumulated vsize (Kb) 5256 [startup+80.0114 s] Raw data (loadavg): 0.94 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 753 0 0 0 7985 6 0 0 25 0 1 0 1842230241 3366912 740 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 822 740 145 145 0 677 0 [pid=22047] vsize: 3288 Current children cumulated CPU time (s) 79.91 Current children cumulated vsize (Kb) 5412 [startup+90.0121 s] Raw data (loadavg): 0.95 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 770 0 0 0 8985 6 0 0 25 0 1 0 1842230241 3436544 757 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 839 757 145 145 0 694 0 [pid=22047] vsize: 3356 Current children cumulated CPU time (s) 89.91 Current children cumulated vsize (Kb) 5480 [startup+100.012 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 776 0 0 0 9985 6 0 0 25 0 1 0 1842230241 3461120 763 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 845 763 145 145 0 700 0 [pid=22047] vsize: 3380 Current children cumulated CPU time (s) 99.91 Current children cumulated vsize (Kb) 5504 [startup+110.013 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 787 0 0 0 10985 6 0 0 25 0 1 0 1842230241 3506176 774 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 856 774 145 145 0 711 0 [pid=22047] vsize: 3424 Current children cumulated CPU time (s) 109.91 Current children cumulated vsize (Kb) 5548 [startup+120.014 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 843 0 0 0 11984 7 0 0 25 0 1 0 1842230241 3735552 830 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 912 830 145 145 0 767 0 [pid=22047] vsize: 3648 Current children cumulated CPU time (s) 119.91 Current children cumulated vsize (Kb) 5772 [startup+130.015 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 856 0 0 0 12984 7 0 0 25 0 1 0 1842230241 3788800 843 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 925 843 145 145 0 780 0 [pid=22047] vsize: 3700 Current children cumulated CPU time (s) 129.91 Current children cumulated vsize (Kb) 5824 [startup+140.016 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 878 0 0 0 13984 7 0 0 25 0 1 0 1842230241 3874816 865 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 946 865 145 145 0 801 0 [pid=22047] vsize: 3784 Current children cumulated CPU time (s) 139.91 Current children cumulated vsize (Kb) 5908 [startup+150.016 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 896 0 0 0 14984 7 0 0 25 0 1 0 1842230241 3948544 883 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 964 883 145 145 0 819 0 [pid=22047] vsize: 3856 Current children cumulated CPU time (s) 149.91 Current children cumulated vsize (Kb) 5980 [startup+160.017 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 909 0 0 0 15984 8 0 0 25 0 1 0 1842230241 4001792 896 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 977 896 145 145 0 832 0 [pid=22047] vsize: 3908 Current children cumulated CPU time (s) 159.92 Current children cumulated vsize (Kb) 6032 [startup+170.018 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 920 0 0 0 16984 8 0 0 25 0 1 0 1842230241 4050944 907 4294967295 134512640 135094434 3221224448 3221223040 134556715 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 989 907 145 145 0 844 0 [pid=22047] vsize: 3956 Current children cumulated CPU time (s) 169.92 Current children cumulated vsize (Kb) 6080 [startup+180.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 933 0 0 0 17984 8 0 0 25 0 1 0 1842230241 4104192 920 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1002 920 145 145 0 857 0 [pid=22047] vsize: 4008 Current children cumulated CPU time (s) 179.92 Current children cumulated vsize (Kb) 6132 [startup+190.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 978 0 0 0 18983 8 0 0 25 0 1 0 1842230241 4288512 965 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1047 965 145 145 0 902 0 [pid=22047] vsize: 4188 Current children cumulated CPU time (s) 189.91 Current children cumulated vsize (Kb) 6312 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 986 0 0 0 19983 8 0 0 25 0 1 0 1842230241 4321280 973 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1055 973 145 145 0 910 0 [pid=22047] vsize: 4220 Current children cumulated CPU time (s) 199.91 Current children cumulated vsize (Kb) 6344 [startup+210.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 996 0 0 0 20983 8 0 0 25 0 1 0 1842230241 4362240 983 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1065 983 145 145 0 920 0 [pid=22047] vsize: 4260 Current children cumulated CPU time (s) 209.91 Current children cumulated vsize (Kb) 6384 [startup+220.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1014 0 0 0 21983 8 0 0 25 0 1 0 1842230241 4440064 1001 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1084 1001 145 145 0 939 0 [pid=22047] vsize: 4336 Current children cumulated CPU time (s) 219.91 Current children cumulated vsize (Kb) 6460 [startup+230.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1022 0 0 0 22984 8 0 0 25 0 1 0 1842230241 4472832 1009 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1092 1009 145 145 0 947 0 [pid=22047] vsize: 4368 Current children cumulated CPU time (s) 229.92 Current children cumulated vsize (Kb) 6492 [startup+240.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1039 0 0 0 23984 9 0 0 25 0 1 0 1842230241 4546560 1026 4294967295 134512640 135094434 3221224448 3221223120 134556304 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1110 1026 145 145 0 965 0 [pid=22047] vsize: 4440 Current children cumulated CPU time (s) 239.93 Current children cumulated vsize (Kb) 6564 [startup+250.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1051 0 0 0 24984 9 0 0 25 0 1 0 1842230241 4595712 1038 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1122 1038 145 145 0 977 0 [pid=22047] vsize: 4488 Current children cumulated CPU time (s) 249.93 Current children cumulated vsize (Kb) 6612 [startup+260.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1065 0 0 0 25983 9 0 0 25 0 1 0 1842230241 4657152 1052 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1137 1052 145 145 0 992 0 [pid=22047] vsize: 4548 Current children cumulated CPU time (s) 259.92 Current children cumulated vsize (Kb) 6672 [startup+270.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1075 0 0 0 26983 9 0 0 25 0 1 0 1842230241 4698112 1062 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1147 1062 145 145 0 1002 0 [pid=22047] vsize: 4588 Current children cumulated CPU time (s) 269.92 Current children cumulated vsize (Kb) 6712 [startup+280.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1088 0 0 0 27984 9 0 0 25 0 1 0 1842230241 4755456 1075 4294967295 134512640 135094434 3221224448 3221223040 134557002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1161 1075 145 145 0 1016 0 [pid=22047] vsize: 4644 Current children cumulated CPU time (s) 279.93 Current children cumulated vsize (Kb) 6768 [startup+290.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1108 0 0 0 28982 10 0 0 25 0 1 0 1842230241 4837376 1095 4294967295 134512640 135094434 3221224448 3221223120 134555404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22047/statm): 1181 1095 145 145 0 1036 0 [pid=22047] vsize: 4724 Current children cumulated CPU time (s) 289.92 Current children cumulated vsize (Kb) 6848 [startup+300.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1119 0 0 0 29982 10 0 0 25 0 1 0 1842230241 4898816 1106 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1196 1106 145 145 0 1051 0 [pid=22047] vsize: 4784 Current children cumulated CPU time (s) 299.92 Current children cumulated vsize (Kb) 6908 [startup+310.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1131 0 0 0 30981 10 0 0 25 0 1 0 1842230241 4947968 1118 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1208 1118 145 145 0 1063 0 [pid=22047] vsize: 4832 Current children cumulated CPU time (s) 309.91 Current children cumulated vsize (Kb) 6956 [startup+320.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1150 0 0 0 31981 10 0 0 25 0 1 0 1842230241 5025792 1137 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1227 1137 145 145 0 1082 0 [pid=22047] vsize: 4908 Current children cumulated CPU time (s) 319.91 Current children cumulated vsize (Kb) 7032 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1152 0 0 0 32982 10 0 0 25 0 1 0 1842230241 5033984 1139 4294967295 134512640 135094434 3221224448 3221223120 134555940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1229 1139 145 145 0 1084 0 [pid=22047] vsize: 4916 Current children cumulated CPU time (s) 329.92 Current children cumulated vsize (Kb) 7040 [startup+340.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1160 0 0 0 33982 10 0 0 25 0 1 0 1842230241 5066752 1147 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1237 1147 145 145 0 1092 0 [pid=22047] vsize: 4948 Current children cumulated CPU time (s) 339.92 Current children cumulated vsize (Kb) 7072 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1160 0 0 0 34982 10 0 0 25 0 1 0 1842230241 5066752 1147 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1237 1147 145 145 0 1092 0 [pid=22047] vsize: 4948 Current children cumulated CPU time (s) 349.92 Current children cumulated vsize (Kb) 7072 [startup+360.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1166 0 0 0 35982 10 0 0 25 0 1 0 1842230241 5099520 1153 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1245 1153 145 145 0 1100 0 [pid=22047] vsize: 4980 Current children cumulated CPU time (s) 359.92 Current children cumulated vsize (Kb) 7104 [startup+370.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1172 0 0 0 36982 11 0 0 25 0 1 0 1842230241 5132288 1159 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1253 1159 145 145 0 1108 0 [pid=22047] vsize: 5012 Current children cumulated CPU time (s) 369.93 Current children cumulated vsize (Kb) 7136 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1185 0 0 0 37982 11 0 0 25 0 1 0 1842230241 5189632 1172 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1267 1172 145 145 0 1122 0 [pid=22047] vsize: 5068 Current children cumulated CPU time (s) 379.93 Current children cumulated vsize (Kb) 7192 [startup+390.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1185 0 0 0 38982 11 0 0 25 0 1 0 1842230241 5189632 1172 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1267 1172 145 145 0 1122 0 [pid=22047] vsize: 5068 Current children cumulated CPU time (s) 389.93 Current children cumulated vsize (Kb) 7192 [startup+400.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1196 0 0 0 39982 11 0 0 25 0 1 0 1842230241 5234688 1183 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1278 1183 145 145 0 1133 0 [pid=22047] vsize: 5112 Current children cumulated CPU time (s) 399.93 Current children cumulated vsize (Kb) 7236 [startup+410.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1200 0 0 0 40982 11 0 0 25 0 1 0 1842230241 5251072 1187 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1282 1187 145 145 0 1137 0 [pid=22047] vsize: 5128 Current children cumulated CPU time (s) 409.93 Current children cumulated vsize (Kb) 7252 [startup+420.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1203 0 0 0 41983 11 0 0 25 0 1 0 1842230241 5267456 1190 4294967295 134512640 135094434 3221224448 3221223072 134562122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1286 1190 145 145 0 1141 0 [pid=22047] vsize: 5144 Current children cumulated CPU time (s) 419.94 Current children cumulated vsize (Kb) 7268 [startup+430.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1215 0 0 0 42983 11 0 0 25 0 1 0 1842230241 5324800 1202 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1300 1202 145 145 0 1155 0 [pid=22047] vsize: 5200 Current children cumulated CPU time (s) 429.94 Current children cumulated vsize (Kb) 7324 [startup+440.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1244 0 0 0 43982 11 0 0 25 0 1 0 1842230241 5443584 1231 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1329 1231 145 145 0 1184 0 [pid=22047] vsize: 5316 Current children cumulated CPU time (s) 439.93 Current children cumulated vsize (Kb) 7440 [startup+450.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1262 0 0 0 44982 12 0 0 25 0 1 0 1842230241 5525504 1249 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1349 1249 145 145 0 1204 0 [pid=22047] vsize: 5396 Current children cumulated CPU time (s) 449.94 Current children cumulated vsize (Kb) 7520 [startup+460.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1280 0 0 0 45982 12 0 0 25 0 1 0 1842230241 5599232 1267 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1367 1267 145 145 0 1222 0 [pid=22047] vsize: 5468 Current children cumulated CPU time (s) 459.94 Current children cumulated vsize (Kb) 7592 [startup+470.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1292 0 0 0 46982 12 0 0 25 0 1 0 1842230241 5648384 1279 4294967295 134512640 135094434 3221224448 3221222912 134780733 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1379 1279 145 145 0 1234 0 [pid=22047] vsize: 5516 Current children cumulated CPU time (s) 469.94 Current children cumulated vsize (Kb) 7640 [startup+480.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1299 0 0 0 47982 12 0 0 25 0 1 0 1842230241 5681152 1286 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1387 1286 145 145 0 1242 0 [pid=22047] vsize: 5548 Current children cumulated CPU time (s) 479.94 Current children cumulated vsize (Kb) 7672 [startup+490.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1314 0 0 0 48982 12 0 0 25 0 1 0 1842230241 5738496 1301 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1401 1301 145 145 0 1256 0 [pid=22047] vsize: 5604 Current children cumulated CPU time (s) 489.94 Current children cumulated vsize (Kb) 7728 [startup+500.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1320 0 0 0 49982 12 0 0 25 0 1 0 1842230241 5763072 1307 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1407 1307 145 145 0 1262 0 [pid=22047] vsize: 5628 Current children cumulated CPU time (s) 499.94 Current children cumulated vsize (Kb) 7752 [startup+510.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1324 0 0 0 50982 12 0 0 25 0 1 0 1842230241 5779456 1311 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1411 1311 145 145 0 1266 0 [pid=22047] vsize: 5644 Current children cumulated CPU time (s) 509.94 Current children cumulated vsize (Kb) 7768 [startup+520.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1328 0 0 0 51982 12 0 0 25 0 1 0 1842230241 5795840 1315 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1415 1315 145 145 0 1270 0 [pid=22047] vsize: 5660 Current children cumulated CPU time (s) 519.94 Current children cumulated vsize (Kb) 7784 [startup+530.043 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1342 0 0 0 52983 12 0 0 25 0 1 0 1842230241 5857280 1329 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1430 1329 145 145 0 1285 0 [pid=22047] vsize: 5720 Current children cumulated CPU time (s) 529.95 Current children cumulated vsize (Kb) 7844 [startup+540.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1354 0 0 0 53982 13 0 0 25 0 1 0 1842230241 5906432 1341 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1442 1341 145 145 0 1297 0 [pid=22047] vsize: 5768 Current children cumulated CPU time (s) 539.95 Current children cumulated vsize (Kb) 7892 [startup+550.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1363 0 0 0 54982 13 0 0 25 0 1 0 1842230241 5947392 1350 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1452 1350 145 145 0 1307 0 [pid=22047] vsize: 5808 Current children cumulated CPU time (s) 549.95 Current children cumulated vsize (Kb) 7932 [startup+560.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1370 0 0 0 55983 13 0 0 25 0 1 0 1842230241 5980160 1357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1460 1357 145 145 0 1315 0 [pid=22047] vsize: 5840 Current children cumulated CPU time (s) 559.96 Current children cumulated vsize (Kb) 7964 [startup+570.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1377 0 0 0 56982 13 0 0 25 0 1 0 1842230241 6004736 1364 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1466 1364 145 145 0 1321 0 [pid=22047] vsize: 5864 Current children cumulated CPU time (s) 569.95 Current children cumulated vsize (Kb) 7988 [startup+580.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1377 0 0 0 57983 13 0 0 25 0 1 0 1842230241 6004736 1364 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1466 1364 145 145 0 1321 0 [pid=22047] vsize: 5864 Current children cumulated CPU time (s) 579.96 Current children cumulated vsize (Kb) 7988 [startup+590.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1387 0 0 0 58983 13 0 0 25 0 1 0 1842230241 6045696 1374 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1476 1374 145 145 0 1331 0 [pid=22047] vsize: 5904 Current children cumulated CPU time (s) 589.96 Current children cumulated vsize (Kb) 8028 [startup+600.047 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1401 0 0 0 59983 13 0 0 25 0 1 0 1842230241 6111232 1388 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1492 1388 145 145 0 1347 0 [pid=22047] vsize: 5968 Current children cumulated CPU time (s) 599.96 Current children cumulated vsize (Kb) 8092 [startup+610.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1407 0 0 0 60983 13 0 0 25 0 1 0 1842230241 6135808 1394 4294967295 134512640 135094434 3221224448 3221223120 134556329 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1498 1394 145 145 0 1353 0 [pid=22047] vsize: 5992 Current children cumulated CPU time (s) 609.96 Current children cumulated vsize (Kb) 8116 [startup+620.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1416 0 0 0 61983 14 0 0 25 0 1 0 1842230241 6176768 1403 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1508 1403 145 145 0 1363 0 [pid=22047] vsize: 6032 Current children cumulated CPU time (s) 619.97 Current children cumulated vsize (Kb) 8156 [startup+630.05 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1421 0 0 0 62983 14 0 0 25 0 1 0 1842230241 6201344 1408 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1514 1408 145 145 0 1369 0 [pid=22047] vsize: 6056 Current children cumulated CPU time (s) 629.97 Current children cumulated vsize (Kb) 8180 [startup+640.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1421 0 0 0 63984 14 0 0 25 0 1 0 1842230241 6201344 1408 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1514 1408 145 145 0 1369 0 [pid=22047] vsize: 6056 Current children cumulated CPU time (s) 639.98 Current children cumulated vsize (Kb) 8180 [startup+650.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1424 0 0 0 64984 14 0 0 25 0 1 0 1842230241 6217728 1411 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1518 1411 145 145 0 1373 0 [pid=22047] vsize: 6072 Current children cumulated CPU time (s) 649.98 Current children cumulated vsize (Kb) 8196 [startup+660.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1433 0 0 0 65984 14 0 0 25 0 1 0 1842230241 6250496 1420 4294967295 134512640 135094434 3221224448 3221222960 134781858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1526 1420 145 145 0 1381 0 [pid=22047] vsize: 6104 Current children cumulated CPU time (s) 659.98 Current children cumulated vsize (Kb) 8228 [startup+670.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1435 0 0 0 66984 14 0 0 25 0 1 0 1842230241 6258688 1422 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1528 1422 145 145 0 1383 0 [pid=22047] vsize: 6112 Current children cumulated CPU time (s) 669.98 Current children cumulated vsize (Kb) 8236 [startup+680.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1454 0 0 0 67983 14 0 0 25 0 1 0 1842230241 6365184 1441 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1554 1441 145 145 0 1409 0 [pid=22047] vsize: 6216 Current children cumulated CPU time (s) 679.97 Current children cumulated vsize (Kb) 8340 [startup+690.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1468 0 0 0 68983 15 0 0 25 0 1 0 1842230241 6430720 1455 4294967295 134512640 135094434 3221224448 3221223116 134562036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1570 1455 145 145 0 1425 0 [pid=22047] vsize: 6280 Current children cumulated CPU time (s) 689.98 Current children cumulated vsize (Kb) 8404 [startup+700.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1474 0 0 0 69983 15 0 0 25 0 1 0 1842230241 6463488 1461 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1578 1461 145 145 0 1433 0 [pid=22047] vsize: 6312 Current children cumulated CPU time (s) 699.98 Current children cumulated vsize (Kb) 8436 [startup+710.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1485 0 0 0 70984 15 0 0 25 0 1 0 1842230241 6512640 1472 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1590 1472 145 145 0 1445 0 [pid=22047] vsize: 6360 Current children cumulated CPU time (s) 709.99 Current children cumulated vsize (Kb) 8484 [startup+720.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1491 0 0 0 71984 15 0 0 25 0 1 0 1842230241 6541312 1478 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1597 1478 145 145 0 1452 0 [pid=22047] vsize: 6388 Current children cumulated CPU time (s) 719.99 Current children cumulated vsize (Kb) 8512 [startup+730.057 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1498 0 0 0 72984 15 0 0 25 0 1 0 1842230241 6569984 1485 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1604 1485 145 145 0 1459 0 [pid=22047] vsize: 6416 Current children cumulated CPU time (s) 729.99 Current children cumulated vsize (Kb) 8540 [startup+740.058 s] Raw data (loadavg): 1.07 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1503 0 0 0 73984 15 0 0 25 0 1 0 1842230241 6594560 1490 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1610 1490 145 145 0 1465 0 [pid=22047] vsize: 6440 Current children cumulated CPU time (s) 739.99 Current children cumulated vsize (Kb) 8564 [startup+750.058 s] Raw data (loadavg): 1.06 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1507 0 0 0 74984 15 0 0 25 0 1 0 1842230241 6610944 1494 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1614 1494 145 145 0 1469 0 [pid=22047] vsize: 6456 Current children cumulated CPU time (s) 749.99 Current children cumulated vsize (Kb) 8580 [startup+760.059 s] Raw data (loadavg): 1.05 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1523 0 0 0 75984 15 0 0 25 0 1 0 1842230241 6680576 1510 4294967295 134512640 135094434 3221224448 3221223040 134557210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1631 1510 145 145 0 1486 0 [pid=22047] vsize: 6524 Current children cumulated CPU time (s) 759.99 Current children cumulated vsize (Kb) 8648 [startup+770.06 s] Raw data (loadavg): 1.04 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1523 0 0 0 76984 15 0 0 25 0 1 0 1842230241 6680576 1510 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1631 1510 145 145 0 1486 0 [pid=22047] vsize: 6524 Current children cumulated CPU time (s) 769.99 Current children cumulated vsize (Kb) 8648 [startup+780.061 s] Raw data (loadavg): 1.04 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1528 0 0 0 77984 15 0 0 25 0 1 0 1842230241 6696960 1515 4294967295 134512640 135094434 3221224448 3221223060 134563061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1635 1515 145 145 0 1490 0 [pid=22047] vsize: 6540 Current children cumulated CPU time (s) 779.99 Current children cumulated vsize (Kb) 8664 [startup+790.062 s] Raw data (loadavg): 1.03 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1537 0 0 0 78984 15 0 0 25 0 1 0 1842230241 6742016 1524 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1646 1524 145 145 0 1501 0 [pid=22047] vsize: 6584 Current children cumulated CPU time (s) 789.99 Current children cumulated vsize (Kb) 8708 [startup+800.063 s] Raw data (loadavg): 1.03 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1548 0 0 0 79984 15 0 0 25 0 1 0 1842230241 6782976 1535 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1656 1535 145 145 0 1511 0 [pid=22047] vsize: 6624 Current children cumulated CPU time (s) 799.99 Current children cumulated vsize (Kb) 8748 [startup+810.063 s] Raw data (loadavg): 1.02 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1552 0 0 0 80984 16 0 0 25 0 1 0 1842230241 6799360 1539 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1660 1539 145 145 0 1515 0 [pid=22047] vsize: 6640 Current children cumulated CPU time (s) 810 Current children cumulated vsize (Kb) 8764 [startup+820.063 s] Raw data (loadavg): 1.02 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1553 0 0 0 81985 16 0 0 25 0 1 0 1842230241 6799360 1540 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1660 1540 145 145 0 1515 0 [pid=22047] vsize: 6640 Current children cumulated CPU time (s) 820.01 Current children cumulated vsize (Kb) 8764 [startup+830.065 s] Raw data (loadavg): 1.01 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1558 0 0 0 82985 16 0 0 25 0 1 0 1842230241 6823936 1545 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1666 1545 145 145 0 1521 0 [pid=22047] vsize: 6664 Current children cumulated CPU time (s) 830.01 Current children cumulated vsize (Kb) 8788 [startup+840.065 s] Raw data (loadavg): 1.01 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1562 0 0 0 83985 16 0 0 25 0 1 0 1842230241 6840320 1549 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1670 1549 145 145 0 1525 0 [pid=22047] vsize: 6680 Current children cumulated CPU time (s) 840.01 Current children cumulated vsize (Kb) 8804 [startup+850.065 s] Raw data (loadavg): 1.01 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1570 0 0 0 84985 16 0 0 25 0 1 0 1842230241 6873088 1557 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1678 1557 145 145 0 1533 0 [pid=22047] vsize: 6712 Current children cumulated CPU time (s) 850.01 Current children cumulated vsize (Kb) 8836 [startup+860.066 s] Raw data (loadavg): 1.01 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1570 0 0 0 85985 16 0 0 25 0 1 0 1842230241 6873088 1557 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1678 1557 145 145 0 1533 0 [pid=22047] vsize: 6712 Current children cumulated CPU time (s) 860.01 Current children cumulated vsize (Kb) 8836 [startup+870.067 s] Raw data (loadavg): 1.01 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1575 0 0 0 86985 16 0 0 25 0 1 0 1842230241 6897664 1562 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1684 1562 145 145 0 1539 0 [pid=22047] vsize: 6736 Current children cumulated CPU time (s) 870.01 Current children cumulated vsize (Kb) 8860 [startup+880.067 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1586 0 0 0 87986 16 0 0 25 0 1 0 1842230241 6946816 1573 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1696 1573 145 145 0 1551 0 [pid=22047] vsize: 6784 Current children cumulated CPU time (s) 880.02 Current children cumulated vsize (Kb) 8908 [startup+890.068 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1590 0 0 0 88986 16 0 0 25 0 1 0 1842230241 6963200 1577 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1700 1577 145 145 0 1555 0 [pid=22047] vsize: 6800 Current children cumulated CPU time (s) 890.02 Current children cumulated vsize (Kb) 8924 [startup+900.069 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1598 0 0 0 89986 16 0 0 25 0 1 0 1842230241 7004160 1585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1710 1585 145 145 0 1565 0 [pid=22047] vsize: 6840 Current children cumulated CPU time (s) 900.02 Current children cumulated vsize (Kb) 8964 [startup+910.069 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1611 0 0 0 90986 16 0 0 25 0 1 0 1842230241 7061504 1598 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1724 1598 145 145 0 1579 0 [pid=22047] vsize: 6896 Current children cumulated CPU time (s) 910.02 Current children cumulated vsize (Kb) 9020 [startup+920.07 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1625 0 0 0 91986 17 0 0 25 0 1 0 1842230241 7114752 1612 4294967295 134512640 135094434 3221224448 3221223040 134551448 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1737 1612 145 145 0 1592 0 [pid=22047] vsize: 6948 Current children cumulated CPU time (s) 920.03 Current children cumulated vsize (Kb) 9072 [startup+930.071 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1630 0 0 0 92986 17 0 0 25 0 1 0 1842230241 7131136 1617 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1741 1617 145 145 0 1596 0 [pid=22047] vsize: 6964 Current children cumulated CPU time (s) 930.03 Current children cumulated vsize (Kb) 9088 [startup+940.071 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1632 0 0 0 93986 17 0 0 25 0 1 0 1842230241 7139328 1619 4294967295 134512640 135094434 3221224448 3221223200 134559282 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1743 1619 145 145 0 1598 0 [pid=22047] vsize: 6972 Current children cumulated CPU time (s) 940.03 Current children cumulated vsize (Kb) 9096 [startup+950.072 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1634 0 0 0 94986 17 0 0 25 0 1 0 1842230241 7147520 1621 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1745 1621 145 145 0 1600 0 [pid=22047] vsize: 6980 Current children cumulated CPU time (s) 950.03 Current children cumulated vsize (Kb) 9104 [startup+960.073 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1634 0 0 0 95986 17 0 0 25 0 1 0 1842230241 7147520 1621 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1745 1621 145 145 0 1600 0 [pid=22047] vsize: 6980 Current children cumulated CPU time (s) 960.03 Current children cumulated vsize (Kb) 9104 [startup+970.073 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1639 0 0 0 96987 17 0 0 25 0 1 0 1842230241 7172096 1626 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1751 1626 145 145 0 1606 0 [pid=22047] vsize: 7004 Current children cumulated CPU time (s) 970.04 Current children cumulated vsize (Kb) 9128 [startup+980.075 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1639 0 0 0 97987 17 0 0 25 0 1 0 1842230241 7172096 1626 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1751 1626 145 145 0 1606 0 [pid=22047] vsize: 7004 Current children cumulated CPU time (s) 980.04 Current children cumulated vsize (Kb) 9128 [startup+990.076 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1644 0 0 0 98987 17 0 0 25 0 1 0 1842230241 7188480 1631 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1755 1631 145 145 0 1610 0 [pid=22047] vsize: 7020 Current children cumulated CPU time (s) 990.04 Current children cumulated vsize (Kb) 9144 [startup+1000.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1646 0 0 0 99987 17 0 0 25 0 1 0 1842230241 7196672 1633 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1757 1633 145 145 0 1612 0 [pid=22047] vsize: 7028 Current children cumulated CPU time (s) 1000.04 Current children cumulated vsize (Kb) 9152 [startup+1010.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1651 0 0 0 100987 17 0 0 25 0 1 0 1842230241 7221248 1638 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1763 1638 145 145 0 1618 0 [pid=22047] vsize: 7052 Current children cumulated CPU time (s) 1010.04 Current children cumulated vsize (Kb) 9176 [startup+1020.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1655 0 0 0 101987 17 0 0 25 0 1 0 1842230241 7237632 1642 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1767 1642 145 145 0 1622 0 [pid=22047] vsize: 7068 Current children cumulated CPU time (s) 1020.04 Current children cumulated vsize (Kb) 9192 [startup+1030.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1661 0 0 0 102988 17 0 0 25 0 1 0 1842230241 7262208 1648 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1773 1648 145 145 0 1628 0 [pid=22047] vsize: 7092 Current children cumulated CPU time (s) 1030.05 Current children cumulated vsize (Kb) 9216 [startup+1040.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1677 0 0 0 103987 18 0 0 25 0 1 0 1842230241 7327744 1664 4294967295 134512640 135094434 3221224448 3221223072 134557694 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1789 1664 145 145 0 1644 0 [pid=22047] vsize: 7156 Current children cumulated CPU time (s) 1040.05 Current children cumulated vsize (Kb) 9280 [startup+1050.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1680 0 0 0 104988 18 0 0 25 0 1 0 1842230241 7340032 1667 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1792 1667 145 145 0 1647 0 [pid=22047] vsize: 7168 Current children cumulated CPU time (s) 1050.06 Current children cumulated vsize (Kb) 9292 [startup+1060.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1705 0 0 0 105987 18 0 0 25 0 1 0 1842230241 7434240 1692 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1815 1692 145 145 0 1670 0 [pid=22047] vsize: 7260 Current children cumulated CPU time (s) 1060.05 Current children cumulated vsize (Kb) 9384 [startup+1070.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1714 0 0 0 106987 18 0 0 25 0 1 0 1842230241 7483392 1701 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1827 1701 145 145 0 1682 0 [pid=22047] vsize: 7308 Current children cumulated CPU time (s) 1070.05 Current children cumulated vsize (Kb) 9432 [startup+1080.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1719 0 0 0 107987 18 0 0 25 0 1 0 1842230241 7503872 1706 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1832 1706 145 145 0 1687 0 [pid=22047] vsize: 7328 Current children cumulated CPU time (s) 1080.05 Current children cumulated vsize (Kb) 9452 [startup+1090.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1721 0 0 0 108988 18 0 0 25 0 1 0 1842230241 7512064 1708 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1834 1708 145 145 0 1689 0 [pid=22047] vsize: 7336 Current children cumulated CPU time (s) 1090.06 Current children cumulated vsize (Kb) 9460 [startup+1100.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1724 0 0 0 109988 18 0 0 25 0 1 0 1842230241 7528448 1711 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1838 1711 145 145 0 1693 0 [pid=22047] vsize: 7352 Current children cumulated CPU time (s) 1100.06 Current children cumulated vsize (Kb) 9476 [startup+1110.08 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1730 0 0 0 110988 18 0 0 25 0 1 0 1842230241 7561216 1717 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1846 1717 145 145 0 1701 0 [pid=22047] vsize: 7384 Current children cumulated CPU time (s) 1110.06 Current children cumulated vsize (Kb) 9508 [startup+1120.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1736 0 0 0 111987 19 0 0 25 0 1 0 1842230241 7593984 1723 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1854 1723 145 145 0 1709 0 [pid=22047] vsize: 7416 Current children cumulated CPU time (s) 1120.06 Current children cumulated vsize (Kb) 9540 [startup+1130.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1737 0 0 0 112988 19 0 0 25 0 1 0 1842230241 7593984 1724 4294967295 134512640 135094434 3221224448 3221222992 134562155 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1854 1724 145 145 0 1709 0 [pid=22047] vsize: 7416 Current children cumulated CPU time (s) 1130.07 Current children cumulated vsize (Kb) 9540 [startup+1140.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1746 0 0 0 113988 19 0 0 25 0 1 0 1842230241 7643136 1733 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1866 1733 145 145 0 1721 0 [pid=22047] vsize: 7464 Current children cumulated CPU time (s) 1140.07 Current children cumulated vsize (Kb) 9588 [startup+1150.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1753 0 0 0 114988 19 0 0 25 0 1 0 1842230241 7675904 1740 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1874 1740 145 145 0 1729 0 [pid=22047] vsize: 7496 Current children cumulated CPU time (s) 1150.07 Current children cumulated vsize (Kb) 9620 [startup+1160.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1756 0 0 0 115988 19 0 0 25 0 1 0 1842230241 7692288 1743 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1878 1743 145 145 0 1733 0 [pid=22047] vsize: 7512 Current children cumulated CPU time (s) 1160.07 Current children cumulated vsize (Kb) 9636 [startup+1170.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1759 0 0 0 116988 19 0 0 25 0 1 0 1842230241 7708672 1746 4294967295 134512640 135094434 3221224448 3221223124 134552241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1882 1746 145 145 0 1737 0 [pid=22047] vsize: 7528 Current children cumulated CPU time (s) 1170.07 Current children cumulated vsize (Kb) 9652 [startup+1180.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1760 0 0 0 117989 19 0 0 25 0 1 0 1842230241 7708672 1747 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1882 1747 145 145 0 1737 0 [pid=22047] vsize: 7528 Current children cumulated CPU time (s) 1180.08 Current children cumulated vsize (Kb) 9652 [startup+1190.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1763 0 0 0 118989 19 0 0 25 0 1 0 1842230241 7725056 1750 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1886 1750 145 145 0 1741 0 [pid=22047] vsize: 7544 Current children cumulated CPU time (s) 1190.08 Current children cumulated vsize (Kb) 9668 [startup+1200.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1777 0 0 0 119989 19 0 0 25 0 1 0 1842230241 7786496 1764 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1901 1764 145 145 0 1756 0 [pid=22047] vsize: 7604 Current children cumulated CPU time (s) 1200.08 Current children cumulated vsize (Kb) 9728 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.09 s] Raw data (loadavg): 1.00 0.99 0.99 2/57 22047 Raw data (/proc/22043/stat): 22043 (minisat+_script) S 22042 22043 16528 0 -1 0 288 239 0 0 0 0 0 0 20 0 1 0 1842230236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22043/statm): 531 226 485 147 0 384 0 [pid=22043] vsize: 2124 Raw data (/proc/22047/stat): 22047 (minisat+_64-bit) R 22043 22043 16528 0 -1 0 1777 0 0 0 119989 19 0 0 25 0 1 0 1842230241 7786496 1764 4294967295 134512640 135094434 3221224448 3221223088 134562149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22047/statm): 1901 1764 145 145 0 1756 0 [pid=22047] vsize: 7604 Current children cumulated CPU time (s) 1200.08 Current children cumulated vsize (Kb) 9728 Sending SIGTERM to -22043 Sleeping 2 seconds One traced child (pid=22043) ended because it received signal 15 (SIGTERM) One traced child (pid=22047) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1200.1 CPU time (s): 1200.09 CPU user time (s): 1199.89 CPU system time (s): 0.199969 CPU usage (%): 99.9995 Max. virtual memory (cumulated for all children) (Kb): 9728
ERROR: no interpretation found !