Name | submitted/manquinho/primes-dimacs-cnf/normalized-ii8a3.opb |
MD5SUM | a430664a9b4f203a5896b33ca2b0e0e5 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 191 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 528 |
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 | 528 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 528 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.01 |
Number of variables | 528 |
Total number of constraints | 1816 |
Number of constraints which are clauses | 1816 |
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 | 8 |
LAUNCH ON wulflinc5 THE 2005-09-18 18:04:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2567 boxname=wulflinc5 idbench=223 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a430664a9b4f203a5896b33ca2b0e0e5 /oldhome/oroussel/tmp/wulflinc5/normalized-ii8a3.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-ii8a3.opb IDLAUNCH: 2567 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 917328 kB Buffers: 33876 kB Cached: 59456 kB SwapCached: 780 kB Active: 58704 kB Inactive: 37348 kB HighTotal: 131008 kB HighFree: 67900 kB LowTotal: 903652 kB LowFree: 849428 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5804 kB Slab: 15576 kB Committed_AS: 64300 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 18:25:02 (client local time) WITH STATUS 10 IN 1209.7 SECONDS stats: 2567 7 1209.7 10
c Parsing PB file... c Converting 1816 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 | 1816 4536 | 605 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 232[0m c ---[ 0]---> Sorter-cost:23592 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3 | 29165 68520 | 9721 3 16 5.3 | 0.000 % | c ============================================================================== c [1mFound solution: 210[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 59 | 29396 69141 | 9798 58 792 13.7 | 0.000 % | c | 159 | 29373 69094 | 10777 157 5757 36.7 | 0.383 % | c | 309 | 29326 68997 | 11855 305 12018 39.4 | 0.516 % | c | 534 | 28837 67952 | 13041 517 17976 34.8 | 1.995 % | c ============================================================================== c [1mFound solution: 204[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 621 | 28880 68089 | 9626 588 18176 30.9 | 1.995 % | c | 721 | 28880 68089 | 10588 688 22308 32.4 | 2.200 % | c | 871 | 28524 67303 | 11647 827 25164 30.4 | 3.340 % | c | 1097 | 28524 67303 | 12812 1053 42619 40.5 | 3.340 % | c | 1435 | 28524 67303 | 14093 1391 53572 38.5 | 3.340 % | c ============================================================================== c [1mFound solution: 199[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1910 | 28602 67526 | 9534 1866 63598 34.1 | 3.340 % | c | 2010 | 28318 66912 | 10487 1959 66161 33.8 | 4.209 % | c | 2161 | 28233 66721 | 11536 2108 68666 32.6 | 4.489 % | c | 2387 | 28233 66721 | 12689 2334 80278 34.4 | 4.489 % | c | 2726 | 28092 66412 | 13958 2670 97944 36.7 | 4.933 % | c | 3232 | 27650 65426 | 15354 3164 139189 44.0 | 6.371 % | c | 3992 | 27650 65426 | 16890 3924 180674 46.0 | 6.371 % | c | 5136 | 27551 65211 | 18579 5065 211969 41.8 | 6.673 % | c ============================================================================== c [1mFound solution: 192[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6518 | 27558 65253 | 9186 6436 265899 41.3 | 6.673 % | c | 6619 | 27519 65166 | 10104 6536 269336 41.2 | 7.104 % | c | 6769 | 27415 64938 | 11115 6684 274644 41.1 | 7.431 % | c | 6994 | 27379 64854 | 12226 6897 277613 40.3 | 7.557 % | c | 7331 | 27379 64854 | 13449 7234 295109 40.8 | 7.557 % | c | 7838 | 27325 64734 | 14794 7535 302474 40.1 | 7.721 % | c | 8597 | 27274 64621 | 16273 8293 341703 41.2 | 7.884 % | c | 9736 | 27274 64621 | 17900 9432 369370 39.2 | 7.884 % | c | 11444 | 27232 64533 | 19691 11138 486622 43.7 | 8.005 % | c | 14007 | 27151 64356 | 21660 13694 628930 45.9 | 8.253 % | c | 17851 | 27151 64356 | 23826 17538 912902 52.1 | 8.253 % | c | 23619 | 27118 64281 | 26208 23271 1310002 56.3 | 8.364 % | c | 32268 | 27118 64281 | 28829 16325 870814 53.3 | 8.364 % | c | 45244 | 27118 64281 | 31712 29301 1724772 58.9 | 8.364 % | c | 64705 | 27024 64061 | 34883 29562 1535665 51.9 | 8.696 % | c | 93897 | 27024 64061 | 38372 36552 1736312 47.5 | 8.696 % | c | 137686 | 27024 64061 | 42209 32006 1723902 53.9 | 8.696 % | c | 203370 | 26915 63818 | 46430 41295 2182791 52.9 | 9.043 % | c | 301896 | 26810 63575 | 51073 47594 2455983 51.6 | 9.407 % |
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/12117/stat): 12117 (minisat+_script) R 12116 12117 824 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785052591 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/12117/statm): 174 3 169 147 0 27 0 [pid=12117] 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=12118 New process pid=12119 New process pid=12120 execve syscall for /bin/sed executable One traced child (pid=12119) 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=12120) exited with status: 0 One traced child (pid=12118) exited with status: 0 New process pid=12121 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-ii8a3.opb [startup+10.004 s] Raw data (loadavg): 0.46 0.63 0.82 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 2019 0 0 0 978 8 0 0 25 0 1 0 1785052596 9273344 1953 4294967295 134512640 135094434 3221224448 3221222000 134518742 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 2264 1953 145 145 0 2119 0 [pid=12121] vsize: 9056 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 11180 [startup+20.0048 s] Raw data (loadavg): 0.54 0.64 0.82 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 2278 0 0 0 1972 10 0 0 25 0 1 0 1785052596 10350592 2212 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 2527 2212 145 145 0 2382 0 [pid=12121] vsize: 10108 Current children cumulated CPU time (s) 19.83 Current children cumulated vsize (Kb) 12232 [startup+30.0065 s] Raw data (loadavg): 0.61 0.65 0.82 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 2537 0 0 0 2966 13 0 0 25 0 1 0 1785052596 11395072 2471 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 2782 2471 145 145 0 2637 0 [pid=12121] vsize: 11128 Current children cumulated CPU time (s) 29.8 Current children cumulated vsize (Kb) 13252 [startup+40.0072 s] Raw data (loadavg): 0.67 0.66 0.82 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 2848 0 0 0 3960 16 0 0 25 0 1 0 1785052596 12722176 2782 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 3106 2782 145 145 0 2961 0 [pid=12121] vsize: 12424 Current children cumulated CPU time (s) 39.77 Current children cumulated vsize (Kb) 14548 [startup+50.008 s] Raw data (loadavg): 0.72 0.67 0.82 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3130 0 0 0 4953 19 0 0 25 0 1 0 1785052596 13860864 3064 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 3384 3064 145 145 0 3239 0 [pid=12121] vsize: 13536 Current children cumulated CPU time (s) 49.73 Current children cumulated vsize (Kb) 15660 [startup+60.0097 s] Raw data (loadavg): 0.76 0.68 0.82 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3348 0 0 0 5949 21 0 0 25 0 1 0 1785052596 14741504 3282 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 3599 3282 145 145 0 3454 0 [pid=12121] vsize: 14396 Current children cumulated CPU time (s) 59.71 Current children cumulated vsize (Kb) 16520 [startup+70.0105 s] Raw data (loadavg): 0.80 0.69 0.82 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3546 0 0 0 6944 24 0 0 25 0 1 0 1785052596 15540224 3480 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 3794 3480 145 145 0 3649 0 [pid=12121] vsize: 15176 Current children cumulated CPU time (s) 69.69 Current children cumulated vsize (Kb) 17300 [startup+80.0132 s] Raw data (loadavg): 0.83 0.70 0.82 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3708 0 0 0 7939 27 0 0 25 0 1 0 1785052596 16195584 3642 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 3954 3642 145 145 0 3809 0 [pid=12121] vsize: 15816 Current children cumulated CPU time (s) 79.67 Current children cumulated vsize (Kb) 17940 [startup+90.0139 s] Raw data (loadavg): 0.86 0.71 0.82 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3711 0 0 0 8938 27 0 0 25 0 1 0 1785052596 16211968 3645 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 3958 3645 145 145 0 3813 0 [pid=12121] vsize: 15832 Current children cumulated CPU time (s) 89.66 Current children cumulated vsize (Kb) 17956 [startup+100.015 s] Raw data (loadavg): 0.88 0.72 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3714 0 0 0 9938 28 0 0 25 0 1 0 1785052596 16228352 3648 4294967295 134512640 135094434 3221224448 3221223136 134554748 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 3962 3648 145 145 0 3817 0 [pid=12121] vsize: 15848 Current children cumulated CPU time (s) 99.67 Current children cumulated vsize (Kb) 17972 [startup+110.016 s] Raw data (loadavg): 0.90 0.73 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3714 0 0 0 10937 29 0 0 25 0 1 0 1785052596 16228352 3648 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 3962 3648 145 145 0 3817 0 [pid=12121] vsize: 15848 Current children cumulated CPU time (s) 109.67 Current children cumulated vsize (Kb) 17972 [startup+120.018 s] Raw data (loadavg): 0.91 0.74 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3724 0 0 0 11937 29 0 0 25 0 1 0 1785052596 16293888 3658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 3978 3658 145 145 0 3833 0 [pid=12121] vsize: 15912 Current children cumulated CPU time (s) 119.67 Current children cumulated vsize (Kb) 18036 [startup+130.019 s] Raw data (loadavg): 0.92 0.75 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 3857 0 0 0 12934 30 0 0 25 0 1 0 1785052596 16834560 3791 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 4110 3791 145 145 0 3965 0 [pid=12121] vsize: 16440 Current children cumulated CPU time (s) 129.65 Current children cumulated vsize (Kb) 18564 [startup+140.021 s] Raw data (loadavg): 0.94 0.75 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4016 0 0 0 13931 32 0 0 25 0 1 0 1785052596 17494016 3950 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 4271 3950 145 145 0 4126 0 [pid=12121] vsize: 17084 Current children cumulated CPU time (s) 139.64 Current children cumulated vsize (Kb) 19208 [startup+150.021 s] Raw data (loadavg): 0.95 0.76 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4185 0 0 0 14928 33 0 0 25 0 1 0 1785052596 18305024 4119 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4469 4119 145 145 0 4324 0 [pid=12121] vsize: 17876 Current children cumulated CPU time (s) 149.62 Current children cumulated vsize (Kb) 20000 [startup+160.022 s] Raw data (loadavg): 0.95 0.77 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4269 0 0 0 15926 34 0 0 25 0 1 0 1785052596 18661376 4203 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4556 4203 145 145 0 4411 0 [pid=12121] vsize: 18224 Current children cumulated CPU time (s) 159.61 Current children cumulated vsize (Kb) 20348 [startup+170.023 s] Raw data (loadavg): 0.96 0.78 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4271 0 0 0 16927 34 0 0 25 0 1 0 1785052596 18661376 4205 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4556 4205 145 145 0 4411 0 [pid=12121] vsize: 18224 Current children cumulated CPU time (s) 169.62 Current children cumulated vsize (Kb) 20348 [startup+180.024 s] Raw data (loadavg): 0.97 0.78 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4271 0 0 0 17927 34 0 0 25 0 1 0 1785052596 18661376 4205 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4556 4205 145 145 0 4411 0 [pid=12121] vsize: 18224 Current children cumulated CPU time (s) 179.62 Current children cumulated vsize (Kb) 20348 [startup+190.024 s] Raw data (loadavg): 0.97 0.79 0.83 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4282 0 0 0 18927 34 0 0 25 0 1 0 1785052596 18710528 4216 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4568 4216 145 145 0 4423 0 [pid=12121] vsize: 18272 Current children cumulated CPU time (s) 189.62 Current children cumulated vsize (Kb) 20396 [startup+200.025 s] Raw data (loadavg): 0.97 0.80 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4289 0 0 0 19927 34 0 0 25 0 1 0 1785052596 18743296 4223 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4576 4223 145 145 0 4431 0 [pid=12121] vsize: 18304 Current children cumulated CPU time (s) 199.62 Current children cumulated vsize (Kb) 20428 [startup+210.026 s] Raw data (loadavg): 0.98 0.80 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4298 0 0 0 20927 34 0 0 25 0 1 0 1785052596 18776064 4232 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4584 4232 145 145 0 4439 0 [pid=12121] vsize: 18336 Current children cumulated CPU time (s) 209.62 Current children cumulated vsize (Kb) 20460 [startup+220.026 s] Raw data (loadavg): 0.98 0.81 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4306 0 0 0 21927 34 0 0 25 0 1 0 1785052596 18825216 4240 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4596 4240 145 145 0 4451 0 [pid=12121] vsize: 18384 Current children cumulated CPU time (s) 219.62 Current children cumulated vsize (Kb) 20508 [startup+230.027 s] Raw data (loadavg): 0.98 0.81 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4321 0 0 0 22928 34 0 0 25 0 1 0 1785052596 18890752 4255 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4612 4255 145 145 0 4467 0 [pid=12121] vsize: 18448 Current children cumulated CPU time (s) 229.63 Current children cumulated vsize (Kb) 20572 [startup+240.028 s] Raw data (loadavg): 0.99 0.82 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 23928 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0 [pid=12121] vsize: 18448 Current children cumulated CPU time (s) 239.63 Current children cumulated vsize (Kb) 20572 [startup+250.029 s] Raw data (loadavg): 0.99 0.83 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 24928 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0 [pid=12121] vsize: 18448 Current children cumulated CPU time (s) 249.63 Current children cumulated vsize (Kb) 20572 [startup+260.029 s] Raw data (loadavg): 0.99 0.83 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 25928 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0 [pid=12121] vsize: 18448 Current children cumulated CPU time (s) 259.63 Current children cumulated vsize (Kb) 20572 [startup+270.03 s] Raw data (loadavg): 0.99 0.84 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 26929 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0 [pid=12121] vsize: 18448 Current children cumulated CPU time (s) 269.64 Current children cumulated vsize (Kb) 20572 [startup+280.031 s] Raw data (loadavg): 0.99 0.84 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 27929 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0 [pid=12121] vsize: 18448 Current children cumulated CPU time (s) 279.64 Current children cumulated vsize (Kb) 20572 [startup+290.032 s] Raw data (loadavg): 0.99 0.85 0.84 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4322 0 0 0 28929 34 0 0 25 0 1 0 1785052596 18890752 4256 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4612 4256 145 145 0 4467 0 [pid=12121] vsize: 18448 Current children cumulated CPU time (s) 289.64 Current children cumulated vsize (Kb) 20572 [startup+300.032 s] Raw data (loadavg): 0.99 0.85 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4327 0 0 0 29929 34 0 0 25 0 1 0 1785052596 18923520 4261 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4620 4261 145 145 0 4475 0 [pid=12121] vsize: 18480 Current children cumulated CPU time (s) 299.64 Current children cumulated vsize (Kb) 20604 [startup+310.033 s] Raw data (loadavg): 0.99 0.85 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4333 0 0 0 30930 34 0 0 25 0 1 0 1785052596 18956288 4267 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4628 4267 145 145 0 4483 0 [pid=12121] vsize: 18512 Current children cumulated CPU time (s) 309.65 Current children cumulated vsize (Kb) 20636 [startup+320.034 s] Raw data (loadavg): 0.99 0.86 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4399 0 0 0 31929 34 0 0 25 0 1 0 1785052596 19218432 4333 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4692 4333 145 145 0 4547 0 [pid=12121] vsize: 18768 Current children cumulated CPU time (s) 319.64 Current children cumulated vsize (Kb) 20892 [startup+330.035 s] Raw data (loadavg): 0.99 0.86 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4502 0 0 0 32926 35 0 0 25 0 1 0 1785052596 19632128 4436 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4793 4436 145 145 0 4648 0 [pid=12121] vsize: 19172 Current children cumulated CPU time (s) 329.62 Current children cumulated vsize (Kb) 21296 [startup+340.035 s] Raw data (loadavg): 0.99 0.87 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4505 0 0 0 33926 35 0 0 25 0 1 0 1785052596 19644416 4439 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4796 4439 145 145 0 4651 0 [pid=12121] vsize: 19184 Current children cumulated CPU time (s) 339.62 Current children cumulated vsize (Kb) 21308 [startup+350.036 s] Raw data (loadavg): 0.99 0.87 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4507 0 0 0 34926 35 0 0 25 0 1 0 1785052596 19660800 4441 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4800 4441 145 145 0 4655 0 [pid=12121] vsize: 19200 Current children cumulated CPU time (s) 349.62 Current children cumulated vsize (Kb) 21324 [startup+360.038 s] Raw data (loadavg): 0.99 0.87 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4516 0 0 0 35927 35 0 0 25 0 1 0 1785052596 19701760 4450 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4810 4450 145 145 0 4665 0 [pid=12121] vsize: 19240 Current children cumulated CPU time (s) 359.63 Current children cumulated vsize (Kb) 21364 [startup+370.039 s] Raw data (loadavg): 0.99 0.88 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4532 0 0 0 36927 35 0 0 25 0 1 0 1785052596 19775488 4466 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4828 4466 145 145 0 4683 0 [pid=12121] vsize: 19312 Current children cumulated CPU time (s) 369.63 Current children cumulated vsize (Kb) 21436 [startup+380.04 s] Raw data (loadavg): 0.99 0.88 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4536 0 0 0 37927 35 0 0 25 0 1 0 1785052596 19791872 4470 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4832 4470 145 145 0 4687 0 [pid=12121] vsize: 19328 Current children cumulated CPU time (s) 379.63 Current children cumulated vsize (Kb) 21452 [startup+390.041 s] Raw data (loadavg): 0.99 0.89 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4553 0 0 0 38927 35 0 0 25 0 1 0 1785052596 19873792 4487 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4852 4487 145 145 0 4707 0 [pid=12121] vsize: 19408 Current children cumulated CPU time (s) 389.63 Current children cumulated vsize (Kb) 21532 [startup+400.041 s] Raw data (loadavg): 0.99 0.89 0.85 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4565 0 0 0 39927 35 0 0 25 0 1 0 1785052596 19939328 4499 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4868 4499 145 145 0 4723 0 [pid=12121] vsize: 19472 Current children cumulated CPU time (s) 399.63 Current children cumulated vsize (Kb) 21596 [startup+410.042 s] Raw data (loadavg): 0.99 0.89 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4589 0 0 0 40927 36 0 0 25 0 1 0 1785052596 20029440 4523 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 4890 4523 145 145 0 4745 0 [pid=12121] vsize: 19560 Current children cumulated CPU time (s) 409.64 Current children cumulated vsize (Kb) 21684 [startup+420.042 s] Raw data (loadavg): 0.99 0.89 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4741 0 0 0 41923 37 0 0 25 0 1 0 1785052596 20652032 4675 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5042 4675 145 145 0 4897 0 [pid=12121] vsize: 20168 Current children cumulated CPU time (s) 419.61 Current children cumulated vsize (Kb) 22292 [startup+430.043 s] Raw data (loadavg): 0.99 0.90 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4741 0 0 0 42924 37 0 0 25 0 1 0 1785052596 20652032 4675 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5042 4675 145 145 0 4897 0 [pid=12121] vsize: 20168 Current children cumulated CPU time (s) 429.62 Current children cumulated vsize (Kb) 22292 [startup+440.044 s] Raw data (loadavg): 0.99 0.90 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4744 0 0 0 43924 37 0 0 25 0 1 0 1785052596 20668416 4678 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5046 4678 145 145 0 4901 0 [pid=12121] vsize: 20184 Current children cumulated CPU time (s) 439.62 Current children cumulated vsize (Kb) 22308 [startup+450.044 s] Raw data (loadavg): 0.99 0.90 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4744 0 0 0 44924 37 0 0 25 0 1 0 1785052596 20668416 4678 4294967295 134512640 135094434 3221224448 3221223040 134557488 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5046 4678 145 145 0 4901 0 [pid=12121] vsize: 20184 Current children cumulated CPU time (s) 449.62 Current children cumulated vsize (Kb) 22308 [startup+460.045 s] Raw data (loadavg): 0.99 0.91 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4744 0 0 0 45924 37 0 0 25 0 1 0 1785052596 20668416 4678 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5046 4678 145 145 0 4901 0 [pid=12121] vsize: 20184 Current children cumulated CPU time (s) 459.62 Current children cumulated vsize (Kb) 22308 [startup+470.046 s] Raw data (loadavg): 0.99 0.91 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4755 0 0 0 46924 37 0 0 25 0 1 0 1785052596 20733952 4689 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 5062 4689 145 145 0 4917 0 [pid=12121] vsize: 20248 Current children cumulated CPU time (s) 469.62 Current children cumulated vsize (Kb) 22372 [startup+480.048 s] Raw data (loadavg): 0.99 0.91 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4755 0 0 0 47924 38 0 0 25 0 1 0 1785052596 20733952 4689 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5062 4689 145 145 0 4917 0 [pid=12121] vsize: 20248 Current children cumulated CPU time (s) 479.63 Current children cumulated vsize (Kb) 22372 [startup+490.048 s] Raw data (loadavg): 0.99 0.91 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4755 0 0 0 48924 38 0 0 25 0 1 0 1785052596 20733952 4689 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5062 4689 145 145 0 4917 0 [pid=12121] vsize: 20248 Current children cumulated CPU time (s) 489.63 Current children cumulated vsize (Kb) 22372 [startup+500.049 s] Raw data (loadavg): 0.99 0.92 0.86 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 4883 0 0 0 49922 39 0 0 25 0 1 0 1785052596 21258240 4817 4294967295 134512640 135094434 3221224448 3221222992 134562113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5190 4817 145 145 0 5045 0 [pid=12121] vsize: 20760 Current children cumulated CPU time (s) 499.62 Current children cumulated vsize (Kb) 22884 [startup+510.05 s] Raw data (loadavg): 0.99 0.92 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5044 0 0 0 50918 40 0 0 25 0 1 0 1785052596 21929984 4978 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5354 4978 145 145 0 5209 0 [pid=12121] vsize: 21416 Current children cumulated CPU time (s) 509.59 Current children cumulated vsize (Kb) 23540 [startup+520.051 s] Raw data (loadavg): 0.99 0.92 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5216 0 0 0 51916 41 0 0 25 0 1 0 1785052596 22622208 5150 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 5523 5150 145 145 0 5378 0 [pid=12121] vsize: 22092 Current children cumulated CPU time (s) 519.58 Current children cumulated vsize (Kb) 24216 [startup+530.052 s] Raw data (loadavg): 0.99 0.92 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5245 0 0 0 52914 42 0 0 25 0 1 0 1785052596 22740992 5179 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5552 5179 145 145 0 5407 0 [pid=12121] vsize: 22208 Current children cumulated CPU time (s) 529.57 Current children cumulated vsize (Kb) 24332 [startup+540.053 s] Raw data (loadavg): 0.99 0.92 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5245 0 0 0 53915 42 0 0 25 0 1 0 1785052596 22740992 5179 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5552 5179 145 145 0 5407 0 [pid=12121] vsize: 22208 Current children cumulated CPU time (s) 539.58 Current children cumulated vsize (Kb) 24332 [startup+550.053 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5247 0 0 0 54915 42 0 0 25 0 1 0 1785052596 22753280 5181 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5555 5181 145 145 0 5410 0 [pid=12121] vsize: 22220 Current children cumulated CPU time (s) 549.58 Current children cumulated vsize (Kb) 24344 [startup+560.055 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5255 0 0 0 55914 42 0 0 25 0 1 0 1785052596 22786048 5189 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5563 5189 145 145 0 5418 0 [pid=12121] vsize: 22252 Current children cumulated CPU time (s) 559.57 Current children cumulated vsize (Kb) 24376 [startup+570.055 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5255 0 0 0 56914 42 0 0 25 0 1 0 1785052596 22786048 5189 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5563 5189 145 145 0 5418 0 [pid=12121] vsize: 22252 Current children cumulated CPU time (s) 569.57 Current children cumulated vsize (Kb) 24376 [startup+580.056 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5259 0 0 0 57915 42 0 0 25 0 1 0 1785052596 22802432 5193 4294967295 134512640 135094434 3221224448 3221223040 134557168 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5567 5193 145 145 0 5422 0 [pid=12121] vsize: 22268 Current children cumulated CPU time (s) 579.58 Current children cumulated vsize (Kb) 24392 [startup+590.057 s] Raw data (loadavg): 0.99 0.93 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5262 0 0 0 58915 42 0 0 25 0 1 0 1785052596 22818816 5196 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5571 5196 145 145 0 5426 0 [pid=12121] vsize: 22284 Current children cumulated CPU time (s) 589.58 Current children cumulated vsize (Kb) 24408 [startup+600.058 s] Raw data (loadavg): 0.99 0.94 0.87 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5272 0 0 0 59915 42 0 0 25 0 1 0 1785052596 22867968 5206 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5583 5206 145 145 0 5438 0 [pid=12121] vsize: 22332 Current children cumulated CPU time (s) 599.58 Current children cumulated vsize (Kb) 24456 [startup+610.058 s] Raw data (loadavg): 0.99 0.94 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5281 0 0 0 60915 42 0 0 25 0 1 0 1785052596 22917120 5215 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5595 5215 145 145 0 5450 0 [pid=12121] vsize: 22380 Current children cumulated CPU time (s) 609.58 Current children cumulated vsize (Kb) 24504 [startup+620.059 s] Raw data (loadavg): 0.99 0.94 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5288 0 0 0 61916 42 0 0 25 0 1 0 1785052596 22949888 5222 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5603 5222 145 145 0 5458 0 [pid=12121] vsize: 22412 Current children cumulated CPU time (s) 619.59 Current children cumulated vsize (Kb) 24536 [startup+630.06 s] Raw data (loadavg): 0.99 0.94 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5440 0 0 0 62913 43 0 0 25 0 1 0 1785052596 23572480 5374 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5755 5374 145 145 0 5610 0 [pid=12121] vsize: 23020 Current children cumulated CPU time (s) 629.57 Current children cumulated vsize (Kb) 25144 [startup+640.061 s] Raw data (loadavg): 0.99 0.94 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5486 0 0 0 63913 43 0 0 25 0 1 0 1785052596 23760896 5420 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5801 5420 145 145 0 5656 0 [pid=12121] vsize: 23204 Current children cumulated CPU time (s) 639.57 Current children cumulated vsize (Kb) 25328 [startup+650.061 s] Raw data (loadavg): 0.99 0.94 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5492 0 0 0 64913 43 0 0 25 0 1 0 1785052596 23793664 5426 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5809 5426 145 145 0 5664 0 [pid=12121] vsize: 23236 Current children cumulated CPU time (s) 649.57 Current children cumulated vsize (Kb) 25360 [startup+660.062 s] Raw data (loadavg): 0.99 0.94 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5492 0 0 0 65913 43 0 0 25 0 1 0 1785052596 23793664 5426 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5809 5426 145 145 0 5664 0 [pid=12121] vsize: 23236 Current children cumulated CPU time (s) 659.57 Current children cumulated vsize (Kb) 25360 [startup+670.063 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5492 0 0 0 66914 43 0 0 25 0 1 0 1785052596 23793664 5426 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5809 5426 145 145 0 5664 0 [pid=12121] vsize: 23236 Current children cumulated CPU time (s) 669.58 Current children cumulated vsize (Kb) 25360 [startup+680.064 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5493 0 0 0 67914 43 0 0 25 0 1 0 1785052596 23793664 5427 4294967295 134512640 135094434 3221224448 3221223104 134558292 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5809 5427 145 145 0 5664 0 [pid=12121] vsize: 23236 Current children cumulated CPU time (s) 679.58 Current children cumulated vsize (Kb) 25360 [startup+690.065 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5493 0 0 0 68914 43 0 0 25 0 1 0 1785052596 23793664 5427 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5809 5427 145 145 0 5664 0 [pid=12121] vsize: 23236 Current children cumulated CPU time (s) 689.58 Current children cumulated vsize (Kb) 25360 [startup+700.065 s] Raw data (loadavg): 0.99 0.95 0.88 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5493 0 0 0 69914 43 0 0 25 0 1 0 1785052596 23793664 5427 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5809 5427 145 145 0 5664 0 [pid=12121] vsize: 23236 Current children cumulated CPU time (s) 699.58 Current children cumulated vsize (Kb) 25360 [startup+710.067 s] Raw data (loadavg): 0.99 0.95 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5499 0 0 0 70915 43 0 0 25 0 1 0 1785052596 23826432 5433 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5817 5433 145 145 0 5672 0 [pid=12121] vsize: 23268 Current children cumulated CPU time (s) 709.59 Current children cumulated vsize (Kb) 25392 [startup+720.067 s] Raw data (loadavg): 0.99 0.95 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5499 0 0 0 71914 44 0 0 25 0 1 0 1785052596 23826432 5433 4294967295 134512640 135094434 3221224448 3221223120 134556222 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5817 5433 145 145 0 5672 0 [pid=12121] vsize: 23268 Current children cumulated CPU time (s) 719.59 Current children cumulated vsize (Kb) 25392 [startup+730.068 s] Raw data (loadavg): 0.99 0.95 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5506 0 0 0 72915 44 0 0 25 0 1 0 1785052596 23859200 5440 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5825 5440 145 145 0 5680 0 [pid=12121] vsize: 23300 Current children cumulated CPU time (s) 729.6 Current children cumulated vsize (Kb) 25424 [startup+740.07 s] Raw data (loadavg): 0.99 0.95 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5508 0 0 0 73915 44 0 0 25 0 1 0 1785052596 23859200 5442 4294967295 134512640 135094434 3221224448 3221223104 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5825 5442 145 145 0 5680 0 [pid=12121] vsize: 23300 Current children cumulated CPU time (s) 739.6 Current children cumulated vsize (Kb) 25424 [startup+750.071 s] Raw data (loadavg): 0.99 0.95 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5509 0 0 0 74915 44 0 0 25 0 1 0 1785052596 23859200 5443 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5825 5443 145 145 0 5680 0 [pid=12121] vsize: 23300 Current children cumulated CPU time (s) 749.6 Current children cumulated vsize (Kb) 25424 [startup+760.071 s] Raw data (loadavg): 0.99 0.95 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5559 0 0 0 75915 44 0 0 25 0 1 0 1785052596 24055808 5493 4294967295 134512640 135094434 3221224448 3221223040 134551457 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5873 5493 145 145 0 5728 0 [pid=12121] vsize: 23492 Current children cumulated CPU time (s) 759.6 Current children cumulated vsize (Kb) 25616 [startup+770.072 s] Raw data (loadavg): 0.99 0.95 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5559 0 0 0 76915 44 0 0 25 0 1 0 1785052596 24055808 5493 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5873 5493 145 145 0 5728 0 [pid=12121] vsize: 23492 Current children cumulated CPU time (s) 769.6 Current children cumulated vsize (Kb) 25616 [startup+780.073 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5559 0 0 0 77915 44 0 0 25 0 1 0 1785052596 24055808 5493 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5873 5493 145 145 0 5728 0 [pid=12121] vsize: 23492 Current children cumulated CPU time (s) 779.6 Current children cumulated vsize (Kb) 25616 [startup+790.074 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5561 0 0 0 78915 44 0 0 25 0 1 0 1785052596 24055808 5495 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5873 5495 145 145 0 5728 0 [pid=12121] vsize: 23492 Current children cumulated CPU time (s) 789.6 Current children cumulated vsize (Kb) 25616 [startup+800.074 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5572 0 0 0 79916 44 0 0 25 0 1 0 1785052596 24117248 5506 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5888 5506 145 145 0 5743 0 [pid=12121] vsize: 23552 Current children cumulated CPU time (s) 799.61 Current children cumulated vsize (Kb) 25676 [startup+810.076 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5585 0 0 0 80916 44 0 0 25 0 1 0 1785052596 24182784 5519 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5904 5519 145 145 0 5759 0 [pid=12121] vsize: 23616 Current children cumulated CPU time (s) 809.61 Current children cumulated vsize (Kb) 25740 [startup+820.077 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5585 0 0 0 81916 44 0 0 25 0 1 0 1785052596 24182784 5519 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5904 5519 145 145 0 5759 0 [pid=12121] vsize: 23616 Current children cumulated CPU time (s) 819.61 Current children cumulated vsize (Kb) 25740 [startup+830.078 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5585 0 0 0 82916 44 0 0 25 0 1 0 1785052596 24182784 5519 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 5904 5519 145 145 0 5759 0 [pid=12121] vsize: 23616 Current children cumulated CPU time (s) 829.61 Current children cumulated vsize (Kb) 25740 [startup+840.079 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5585 0 0 0 83915 45 0 0 25 0 1 0 1785052596 24182784 5519 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5904 5519 145 145 0 5759 0 [pid=12121] vsize: 23616 Current children cumulated CPU time (s) 839.61 Current children cumulated vsize (Kb) 25740 [startup+850.079 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5586 0 0 0 84915 45 0 0 25 0 1 0 1785052596 24182784 5520 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5904 5520 145 145 0 5759 0 [pid=12121] vsize: 23616 Current children cumulated CPU time (s) 849.61 Current children cumulated vsize (Kb) 25740 [startup+860.081 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5604 0 0 0 85916 45 0 0 25 0 1 0 1785052596 24281088 5538 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5928 5538 145 145 0 5783 0 [pid=12121] vsize: 23712 Current children cumulated CPU time (s) 859.62 Current children cumulated vsize (Kb) 25836 [startup+870.082 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5613 0 0 0 86916 45 0 0 25 0 1 0 1785052596 24313856 5547 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5936 5547 145 145 0 5791 0 [pid=12121] vsize: 23744 Current children cumulated CPU time (s) 869.62 Current children cumulated vsize (Kb) 25868 [startup+880.083 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5641 0 0 0 87916 45 0 0 25 0 1 0 1785052596 24453120 5575 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5970 5575 145 145 0 5825 0 [pid=12121] vsize: 23880 Current children cumulated CPU time (s) 879.62 Current children cumulated vsize (Kb) 26004 [startup+890.084 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5647 0 0 0 88916 45 0 0 25 0 1 0 1785052596 24485888 5581 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5978 5581 145 145 0 5833 0 [pid=12121] vsize: 23912 Current children cumulated CPU time (s) 889.62 Current children cumulated vsize (Kb) 26036 [startup+900.085 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5652 0 0 0 89916 45 0 0 25 0 1 0 1785052596 24518656 5586 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5986 5586 145 145 0 5841 0 [pid=12121] vsize: 23944 Current children cumulated CPU time (s) 899.62 Current children cumulated vsize (Kb) 26068 [startup+910.086 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5654 0 0 0 90916 45 0 0 25 0 1 0 1785052596 24518656 5588 4294967295 134512640 135094434 3221224448 3221223120 134556244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5986 5588 145 145 0 5841 0 [pid=12121] vsize: 23944 Current children cumulated CPU time (s) 909.62 Current children cumulated vsize (Kb) 26068 [startup+920.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5656 0 0 0 91917 45 0 0 25 0 1 0 1785052596 24518656 5590 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5986 5590 145 145 0 5841 0 [pid=12121] vsize: 23944 Current children cumulated CPU time (s) 919.63 Current children cumulated vsize (Kb) 26068 [startup+930.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5661 0 0 0 92917 45 0 0 25 0 1 0 1785052596 24551424 5595 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5994 5595 145 145 0 5849 0 [pid=12121] vsize: 23976 Current children cumulated CPU time (s) 929.63 Current children cumulated vsize (Kb) 26100 [startup+940.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5661 0 0 0 93917 45 0 0 25 0 1 0 1785052596 24551424 5595 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5994 5595 145 145 0 5849 0 [pid=12121] vsize: 23976 Current children cumulated CPU time (s) 939.63 Current children cumulated vsize (Kb) 26100 [startup+950.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5663 0 0 0 94917 45 0 0 25 0 1 0 1785052596 24551424 5597 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5994 5597 145 145 0 5849 0 [pid=12121] vsize: 23976 Current children cumulated CPU time (s) 949.63 Current children cumulated vsize (Kb) 26100 [startup+960.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5663 0 0 0 95918 45 0 0 25 0 1 0 1785052596 24551424 5597 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5994 5597 145 145 0 5849 0 [pid=12121] vsize: 23976 Current children cumulated CPU time (s) 959.64 Current children cumulated vsize (Kb) 26100 [startup+970.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5664 0 0 0 96918 45 0 0 25 0 1 0 1785052596 24551424 5598 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5994 5598 145 145 0 5849 0 [pid=12121] vsize: 23976 Current children cumulated CPU time (s) 969.64 Current children cumulated vsize (Kb) 26100 [startup+980.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5664 0 0 0 97918 45 0 0 25 0 1 0 1785052596 24551424 5598 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 5994 5598 145 145 0 5849 0 [pid=12121] vsize: 23976 Current children cumulated CPU time (s) 979.64 Current children cumulated vsize (Kb) 26100 [startup+990.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5669 0 0 0 98918 45 0 0 25 0 1 0 1785052596 24584192 5603 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6002 5603 145 145 0 5857 0 [pid=12121] vsize: 24008 Current children cumulated CPU time (s) 989.64 Current children cumulated vsize (Kb) 26132 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5678 0 0 0 99919 45 0 0 25 0 1 0 1785052596 24649728 5612 4294967295 134512640 135094434 3221224448 3221223120 134555260 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6018 5612 145 145 0 5873 0 [pid=12121] vsize: 24072 Current children cumulated CPU time (s) 999.65 Current children cumulated vsize (Kb) 26196 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5723 0 0 0 100918 45 0 0 25 0 1 0 1785052596 24834048 5657 4294967295 134512640 135094434 3221224448 3221223120 134556239 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6063 5657 145 145 0 5918 0 [pid=12121] vsize: 24252 Current children cumulated CPU time (s) 1009.64 Current children cumulated vsize (Kb) 26376 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 101919 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0 [pid=12121] vsize: 24252 Current children cumulated CPU time (s) 1019.65 Current children cumulated vsize (Kb) 26376 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 102919 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0 [pid=12121] vsize: 24252 Current children cumulated CPU time (s) 1029.65 Current children cumulated vsize (Kb) 26376 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 103919 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0 [pid=12121] vsize: 24252 Current children cumulated CPU time (s) 1039.65 Current children cumulated vsize (Kb) 26376 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 104919 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223120 134555855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0 [pid=12121] vsize: 24252 Current children cumulated CPU time (s) 1049.65 Current children cumulated vsize (Kb) 26376 [startup+1060.1 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5724 0 0 0 105920 45 0 0 25 0 1 0 1785052596 24834048 5658 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6063 5658 145 145 0 5918 0 [pid=12121] vsize: 24252 Current children cumulated CPU time (s) 1059.66 Current children cumulated vsize (Kb) 26376 [startup+1070.1 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5731 0 0 0 106920 45 0 0 25 0 1 0 1785052596 24866816 5665 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6071 5665 145 145 0 5926 0 [pid=12121] vsize: 24284 Current children cumulated CPU time (s) 1069.66 Current children cumulated vsize (Kb) 26408 [startup+1080.1 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5732 0 0 0 107920 45 0 0 25 0 1 0 1785052596 24866816 5666 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6071 5666 145 145 0 5926 0 [pid=12121] vsize: 24284 Current children cumulated CPU time (s) 1079.66 Current children cumulated vsize (Kb) 26408 [startup+1090.1 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5735 0 0 0 108920 45 0 0 25 0 1 0 1785052596 24932352 5669 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6087 5669 145 145 0 5942 0 [pid=12121] vsize: 24348 Current children cumulated CPU time (s) 1089.66 Current children cumulated vsize (Kb) 26472 [startup+1100.1 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5736 0 0 0 109920 45 0 0 25 0 1 0 1785052596 24932352 5670 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6087 5670 145 145 0 5942 0 [pid=12121] vsize: 24348 Current children cumulated CPU time (s) 1099.66 Current children cumulated vsize (Kb) 26472 [startup+1110.1 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5736 0 0 0 110921 45 0 0 25 0 1 0 1785052596 24932352 5670 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6087 5670 145 145 0 5942 0 [pid=12121] vsize: 24348 Current children cumulated CPU time (s) 1109.67 Current children cumulated vsize (Kb) 26472 [startup+1120.1 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5752 0 0 0 111921 46 0 0 25 0 1 0 1785052596 25014272 5686 4294967295 134512640 135094434 3221224448 3221223104 134557976 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12121/statm): 6107 5686 145 145 0 5962 0 [pid=12121] vsize: 24428 Current children cumulated CPU time (s) 1119.68 Current children cumulated vsize (Kb) 26552 [startup+1130.1 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5764 0 0 0 112920 46 0 0 25 0 1 0 1785052596 25047040 5698 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6115 5698 145 145 0 5970 0 [pid=12121] vsize: 24460 Current children cumulated CPU time (s) 1129.67 Current children cumulated vsize (Kb) 26584 [startup+1140.1 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5768 0 0 0 113920 46 0 0 25 0 1 0 1785052596 25047040 5702 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6115 5702 145 145 0 5970 0 [pid=12121] vsize: 24460 Current children cumulated CPU time (s) 1139.67 Current children cumulated vsize (Kb) 26584 [startup+1150.1 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5817 0 0 0 114919 46 0 0 25 0 1 0 1785052596 25235456 5751 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6161 5751 145 145 0 6016 0 [pid=12121] vsize: 24644 Current children cumulated CPU time (s) 1149.66 Current children cumulated vsize (Kb) 26768 [startup+1160.11 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5817 0 0 0 115919 46 0 0 25 0 1 0 1785052596 25235456 5751 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6161 5751 145 145 0 6016 0 [pid=12121] vsize: 24644 Current children cumulated CPU time (s) 1159.66 Current children cumulated vsize (Kb) 26768 [startup+1170.11 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5817 0 0 0 116920 46 0 0 25 0 1 0 1785052596 25235456 5751 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6161 5751 145 145 0 6016 0 [pid=12121] vsize: 24644 Current children cumulated CPU time (s) 1169.67 Current children cumulated vsize (Kb) 26768 [startup+1180.11 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5822 0 0 0 117920 46 0 0 25 0 1 0 1785052596 25268224 5756 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6169 5756 145 145 0 6024 0 [pid=12121] vsize: 24676 Current children cumulated CPU time (s) 1179.67 Current children cumulated vsize (Kb) 26800 [startup+1190.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5822 0 0 0 118920 46 0 0 25 0 1 0 1785052596 25268224 5756 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6169 5756 145 145 0 6024 0 [pid=12121] vsize: 24676 Current children cumulated CPU time (s) 1189.67 Current children cumulated vsize (Kb) 26800 [startup+1200.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5822 0 0 0 119920 46 0 0 25 0 1 0 1785052596 25268224 5756 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6169 5756 145 145 0 6024 0 [pid=12121] vsize: 24676 Current children cumulated CPU time (s) 1199.67 Current children cumulated vsize (Kb) 26800 [startup+1210.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5828 0 0 0 120921 46 0 0 25 0 1 0 1785052596 25300992 5762 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6177 5762 145 145 0 6032 0 [pid=12121] vsize: 24708 Current children cumulated CPU time (s) 1209.68 Current children cumulated vsize (Kb) 26832 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 12121 Raw data (/proc/12117/stat): 12117 (minisat+_script) S 12116 12117 824 0 -1 0 288 239 0 0 0 0 0 1 21 0 1 0 1785052591 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12117/statm): 531 226 485 147 0 384 0 [pid=12117] vsize: 2124 Raw data (/proc/12121/stat): 12121 (minisat+_64-bit) R 12117 12117 824 0 -1 0 5828 0 0 0 120921 46 0 0 25 0 1 0 1785052596 25300992 5762 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12121/statm): 6177 5762 145 145 0 6032 0 [pid=12121] vsize: 24708 Current children cumulated CPU time (s) 1209.68 Current children cumulated vsize (Kb) 26832 Sending SIGTERM to -12117 Sleeping 2 seconds One traced child (pid=12117) ended because it received signal 15 (SIGTERM) One traced child (pid=12121) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.13 CPU time (s): 1209.7 CPU user time (s): 1209.21 CPU system time (s): 0.481926 CPU usage (%): 99.9645 Max. virtual memory (cumulated for all children) (Kb): 26832
ERROR: no interpretation found !