Name | submitted/manquinho/primes-dimacs-cnf/normalized-par32-4-c.opb |
MD5SUM | 3d2c3109962e8068c6ff1a393a02942b |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 2666 |
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 | 2666 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 2666 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 2666 |
Total number of constraints | 6659 |
Number of constraints which are clauses | 6659 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 3 |
LAUNCH ON wulflinc4 THE 2005-09-18 15:31:21 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2539 boxname=wulflinc4 idbench=195 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3d2c3109962e8068c6ff1a393a02942b /oldhome/oroussel/tmp/wulflinc4/normalized-par32-4-c.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-par32-4-c.opb IDLAUNCH: 2539 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 923872 kB Buffers: 34500 kB Cached: 52600 kB SwapCached: 960 kB Active: 64436 kB Inactive: 25316 kB HighTotal: 131008 kB HighFree: 76076 kB LowTotal: 903652 kB LowFree: 847796 kB SwapTotal: 2097136 kB SwapFree: 2095628 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5692 kB Slab: 15540 kB Committed_AS: 72324 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 15:51:21 (client local time) WITH STATUS 0 IN 1200.16 SECONDS stats: 2539 7 1200.16 0
c Parsing PB file... c Converting 6659 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 | 6659 18272 | 2219 0 0 nan | 0.000 % | c | 102 | 6659 18272 | 2440 102 4036 39.6 | 0.003 % | c | 252 | 6659 18272 | 2684 252 9977 39.6 | 0.000 % | c | 478 | 6659 18272 | 2953 478 18267 38.2 | 0.000 % | c | 817 | 6659 18272 | 3248 817 33443 40.9 | 0.000 % | c | 1324 | 6659 18272 | 3573 1324 50708 38.3 | 0.000 % | c | 2085 | 6659 18272 | 3931 2085 75530 36.2 | 0.000 % | c | 3224 | 6659 18272 | 4324 3224 113144 35.1 | 0.000 % | c | 4934 | 6659 18272 | 4756 2697 80855 30.0 | 0.000 % | c | 7496 | 6659 18272 | 5232 2741 76314 27.8 | 0.000 % | c | 11342 | 6659 18272 | 5755 3932 98780 25.1 | 0.000 % | c | 17108 | 6659 18272 | 6331 3848 85273 22.2 | 0.000 % | c | 25757 | 6659 18272 | 6964 6011 141979 23.6 | 0.000 % | c | 38731 | 6659 18272 | 7660 4835 104809 21.7 | 0.000 % | c | 58192 | 6659 18272 | 8426 4891 115405 23.6 | 0.000 % | c | 87384 | 6659 18272 | 9269 8363 183816 22.0 | 0.000 % | c | 131173 | 6652 18256 | 10196 5291 107425 20.3 | 0.075 % | c | 196857 | 6652 18256 | 11215 9133 189013 20.7 | 0.075 % | c | 295384 | 6652 18256 | 12337 5895 132460 22.5 | 0.075 % | c | 443174 | 6652 18256 | 13571 10715 243644 22.7 | 0.075 % | c | 664857 | 6652 18256 | 14928 6866 130708 19.0 | 0.075 % | c | 997383 | 6652 18256 | 16421 8655 160498 18.5 | 0.075 % |
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/14271/stat): 14271 (minisat+_script) R 14270 14271 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1784112042 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/14271/statm): 174 3 169 147 0 27 0 [pid=14271] 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=14272 New process pid=14273 New process pid=14274 execve syscall for /bin/sed executable One traced child (pid=14273) 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=14274) exited with status: 0 One traced child (pid=14272) exited with status: 0 New process pid=14275 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-par32-4-c.opb [startup+10.0034 s] Raw data (loadavg): 0.93 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 989 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223072 134562048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14275/statm): 819 733 145 145 0 674 0 [pid=14275] vsize: 3276 Current children cumulated CPU time (s) 9.93 Current children cumulated vsize (Kb) 5400 [startup+20.0052 s] Raw data (loadavg): 0.94 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 1989 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 819 733 145 145 0 674 0 [pid=14275] vsize: 3276 Current children cumulated CPU time (s) 19.93 Current children cumulated vsize (Kb) 5400 [startup+30.0061 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 2988 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 819 733 145 145 0 674 0 [pid=14275] vsize: 3276 Current children cumulated CPU time (s) 29.92 Current children cumulated vsize (Kb) 5400 [startup+40.0069 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 3989 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 819 733 145 145 0 674 0 [pid=14275] vsize: 3276 Current children cumulated CPU time (s) 39.93 Current children cumulated vsize (Kb) 5400 [startup+50.0078 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 4989 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 819 733 145 145 0 674 0 [pid=14275] vsize: 3276 Current children cumulated CPU time (s) 49.93 Current children cumulated vsize (Kb) 5400 [startup+60.0087 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 772 0 0 0 5989 4 0 0 25 0 1 0 1784112047 3485696 759 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 851 759 145 145 0 706 0 [pid=14275] vsize: 3404 Current children cumulated CPU time (s) 59.94 Current children cumulated vsize (Kb) 5528 [startup+70.0105 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 776 0 0 0 6989 4 0 0 25 0 1 0 1784112047 3502080 763 4294967295 134512640 135094434 3221224448 3221223040 134557372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 855 763 145 145 0 710 0 [pid=14275] vsize: 3420 Current children cumulated CPU time (s) 69.94 Current children cumulated vsize (Kb) 5544 [startup+80.0114 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 782 0 0 0 7989 4 0 0 25 0 1 0 1784112047 3551232 769 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 867 769 145 145 0 722 0 [pid=14275] vsize: 3468 Current children cumulated CPU time (s) 79.94 Current children cumulated vsize (Kb) 5592 [startup+90.0112 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 799 0 0 0 8989 4 0 0 25 0 1 0 1784112047 3608576 786 4294967295 134512640 135094434 3221224448 3221223120 134556257 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 881 786 145 145 0 736 0 [pid=14275] vsize: 3524 Current children cumulated CPU time (s) 89.94 Current children cumulated vsize (Kb) 5648 [startup+100.012 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 817 0 0 0 9989 4 0 0 25 0 1 0 1784112047 3686400 804 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 900 804 145 145 0 755 0 [pid=14275] vsize: 3600 Current children cumulated CPU time (s) 99.94 Current children cumulated vsize (Kb) 5724 [startup+110.013 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 821 0 0 0 10990 4 0 0 25 0 1 0 1784112047 3702784 808 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 904 808 145 145 0 759 0 [pid=14275] vsize: 3616 Current children cumulated CPU time (s) 109.95 Current children cumulated vsize (Kb) 5740 [startup+120.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 825 0 0 0 11990 4 0 0 25 0 1 0 1784112047 3719168 812 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 908 812 145 145 0 763 0 [pid=14275] vsize: 3632 Current children cumulated CPU time (s) 119.95 Current children cumulated vsize (Kb) 5756 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 825 0 0 0 12990 4 0 0 25 0 1 0 1784112047 3719168 812 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 908 812 145 145 0 763 0 [pid=14275] vsize: 3632 Current children cumulated CPU time (s) 129.95 Current children cumulated vsize (Kb) 5756 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 851 0 0 0 13989 4 0 0 25 0 1 0 1784112047 3829760 838 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 935 838 145 145 0 790 0 [pid=14275] vsize: 3740 Current children cumulated CPU time (s) 139.94 Current children cumulated vsize (Kb) 5864 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 855 0 0 0 14989 4 0 0 25 0 1 0 1784112047 3846144 842 4294967295 134512640 135094434 3221224448 3221223120 134555583 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 939 842 145 145 0 794 0 [pid=14275] vsize: 3756 Current children cumulated CPU time (s) 149.94 Current children cumulated vsize (Kb) 5880 [startup+160.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 858 0 0 0 15990 4 0 0 25 0 1 0 1784112047 3878912 845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 947 845 145 145 0 802 0 [pid=14275] vsize: 3788 Current children cumulated CPU time (s) 159.95 Current children cumulated vsize (Kb) 5912 [startup+170.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 867 0 0 0 16990 4 0 0 25 0 1 0 1784112047 3911680 854 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 955 854 145 145 0 810 0 [pid=14275] vsize: 3820 Current children cumulated CPU time (s) 169.95 Current children cumulated vsize (Kb) 5944 [startup+180.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 874 0 0 0 17990 4 0 0 25 0 1 0 1784112047 3944448 861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 963 861 145 145 0 818 0 [pid=14275] vsize: 3852 Current children cumulated CPU time (s) 179.95 Current children cumulated vsize (Kb) 5976 [startup+190.019 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 884 0 0 0 18990 4 0 0 25 0 1 0 1784112047 3993600 871 4294967295 134512640 135094434 3221224448 3221223012 134562166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 975 871 145 145 0 830 0 [pid=14275] vsize: 3900 Current children cumulated CPU time (s) 189.95 Current children cumulated vsize (Kb) 6024 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 884 0 0 0 19990 4 0 0 25 0 1 0 1784112047 3993600 871 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 975 871 145 145 0 830 0 [pid=14275] vsize: 3900 Current children cumulated CPU time (s) 199.95 Current children cumulated vsize (Kb) 6024 [startup+210.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 891 0 0 0 20991 4 0 0 25 0 1 0 1784112047 4018176 878 4294967295 134512640 135094434 3221224448 3221222976 134783130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 981 878 145 145 0 836 0 [pid=14275] vsize: 3924 Current children cumulated CPU time (s) 209.96 Current children cumulated vsize (Kb) 6048 [startup+220.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 937 0 0 0 21990 5 0 0 25 0 1 0 1784112047 4198400 924 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1025 924 145 145 0 880 0 [pid=14275] vsize: 4100 Current children cumulated CPU time (s) 219.96 Current children cumulated vsize (Kb) 6224 [startup+230.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 22990 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0 [pid=14275] vsize: 4132 Current children cumulated CPU time (s) 229.96 Current children cumulated vsize (Kb) 6256 [startup+240.023 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 23990 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223120 134556415 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0 [pid=14275] vsize: 4132 Current children cumulated CPU time (s) 239.96 Current children cumulated vsize (Kb) 6256 [startup+250.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 24990 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0 [pid=14275] vsize: 4132 Current children cumulated CPU time (s) 249.96 Current children cumulated vsize (Kb) 6256 [startup+260.025 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 25991 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0 [pid=14275] vsize: 4132 Current children cumulated CPU time (s) 259.97 Current children cumulated vsize (Kb) 6256 [startup+270.026 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 26990 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223104 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0 [pid=14275] vsize: 4132 Current children cumulated CPU time (s) 269.96 Current children cumulated vsize (Kb) 6256 [startup+280.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 943 0 0 0 27990 5 0 0 25 0 1 0 1784112047 4235264 930 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1034 930 145 145 0 889 0 [pid=14275] vsize: 4136 Current children cumulated CPU time (s) 279.96 Current children cumulated vsize (Kb) 6260 [startup+290.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 951 0 0 0 28991 5 0 0 25 0 1 0 1784112047 4280320 938 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1045 938 145 145 0 900 0 [pid=14275] vsize: 4180 Current children cumulated CPU time (s) 289.97 Current children cumulated vsize (Kb) 6304 [startup+300.028 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 951 0 0 0 29991 5 0 0 25 0 1 0 1784112047 4280320 938 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1045 938 145 145 0 900 0 [pid=14275] vsize: 4180 Current children cumulated CPU time (s) 299.97 Current children cumulated vsize (Kb) 6304 [startup+310.029 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 954 0 0 0 30991 5 0 0 25 0 1 0 1784112047 4296704 941 4294967295 134512640 135094434 3221224448 3221223112 134562037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1049 941 145 145 0 904 0 [pid=14275] vsize: 4196 Current children cumulated CPU time (s) 309.97 Current children cumulated vsize (Kb) 6320 [startup+320.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 955 0 0 0 31991 5 0 0 25 0 1 0 1784112047 4296704 942 4294967295 134512640 135094434 3221224448 3221223104 134558240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1049 942 145 145 0 904 0 [pid=14275] vsize: 4196 Current children cumulated CPU time (s) 319.97 Current children cumulated vsize (Kb) 6320 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 993 0 0 0 32990 6 0 0 25 0 1 0 1784112047 4452352 980 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1087 980 145 145 0 942 0 [pid=14275] vsize: 4348 Current children cumulated CPU time (s) 329.97 Current children cumulated vsize (Kb) 6472 [startup+340.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1006 0 0 0 33990 6 0 0 25 0 1 0 1784112047 4501504 993 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1099 993 145 145 0 954 0 [pid=14275] vsize: 4396 Current children cumulated CPU time (s) 339.97 Current children cumulated vsize (Kb) 6520 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1029 0 0 0 34990 6 0 0 25 0 1 0 1784112047 4608000 1016 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1125 1016 145 145 0 980 0 [pid=14275] vsize: 4500 Current children cumulated CPU time (s) 349.97 Current children cumulated vsize (Kb) 6624 [startup+360.032 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1036 0 0 0 35990 6 0 0 25 0 1 0 1784112047 4648960 1023 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1135 1023 145 145 0 990 0 [pid=14275] vsize: 4540 Current children cumulated CPU time (s) 359.97 Current children cumulated vsize (Kb) 6664 [startup+370.033 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1037 0 0 0 36991 6 0 0 25 0 1 0 1784112047 4648960 1024 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1135 1024 145 145 0 990 0 [pid=14275] vsize: 4540 Current children cumulated CPU time (s) 369.98 Current children cumulated vsize (Kb) 6664 [startup+380.034 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1043 0 0 0 37991 6 0 0 25 0 1 0 1784112047 4681728 1030 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1143 1030 145 145 0 998 0 [pid=14275] vsize: 4572 Current children cumulated CPU time (s) 379.98 Current children cumulated vsize (Kb) 6696 [startup+390.035 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1044 0 0 0 38991 6 0 0 25 0 1 0 1784112047 4681728 1031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1143 1031 145 145 0 998 0 [pid=14275] vsize: 4572 Current children cumulated CPU time (s) 389.98 Current children cumulated vsize (Kb) 6696 [startup+400.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1044 0 0 0 39991 6 0 0 25 0 1 0 1784112047 4681728 1031 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1143 1031 145 145 0 998 0 [pid=14275] vsize: 4572 Current children cumulated CPU time (s) 399.98 Current children cumulated vsize (Kb) 6696 [startup+410.037 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1045 0 0 0 40992 6 0 0 25 0 1 0 1784112047 4681728 1032 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1143 1032 145 145 0 998 0 [pid=14275] vsize: 4572 Current children cumulated CPU time (s) 409.99 Current children cumulated vsize (Kb) 6696 [startup+420.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1051 0 0 0 41992 6 0 0 25 0 1 0 1784112047 4714496 1038 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1151 1038 145 145 0 1006 0 [pid=14275] vsize: 4604 Current children cumulated CPU time (s) 419.99 Current children cumulated vsize (Kb) 6728 [startup+430.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1051 0 0 0 42992 6 0 0 25 0 1 0 1784112047 4714496 1038 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1151 1038 145 145 0 1006 0 [pid=14275] vsize: 4604 Current children cumulated CPU time (s) 429.99 Current children cumulated vsize (Kb) 6728 [startup+440.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1051 0 0 0 43992 6 0 0 25 0 1 0 1784112047 4714496 1038 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1151 1038 145 145 0 1006 0 [pid=14275] vsize: 4604 Current children cumulated CPU time (s) 439.99 Current children cumulated vsize (Kb) 6728 [startup+450.039 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1051 0 0 0 44992 6 0 0 25 0 1 0 1784112047 4714496 1038 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1151 1038 145 145 0 1006 0 [pid=14275] vsize: 4604 Current children cumulated CPU time (s) 449.99 Current children cumulated vsize (Kb) 6728 [startup+460.04 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1057 0 0 0 45992 6 0 0 25 0 1 0 1784112047 4747264 1044 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1159 1044 145 145 0 1014 0 [pid=14275] vsize: 4636 Current children cumulated CPU time (s) 459.99 Current children cumulated vsize (Kb) 6760 [startup+470.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1064 0 0 0 46992 6 0 0 25 0 1 0 1784112047 4780032 1051 4294967295 134512640 135094434 3221224448 3221223120 134556033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1167 1051 145 145 0 1022 0 [pid=14275] vsize: 4668 Current children cumulated CPU time (s) 469.99 Current children cumulated vsize (Kb) 6792 [startup+480.042 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1064 0 0 0 47992 6 0 0 25 0 1 0 1784112047 4780032 1051 4294967295 134512640 135094434 3221224448 3221222976 134780546 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1167 1051 145 145 0 1022 0 [pid=14275] vsize: 4668 Current children cumulated CPU time (s) 479.99 Current children cumulated vsize (Kb) 6792 [startup+490.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1065 0 0 0 48992 6 0 0 25 0 1 0 1784112047 4780032 1052 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1167 1052 145 145 0 1022 0 [pid=14275] vsize: 4668 Current children cumulated CPU time (s) 489.99 Current children cumulated vsize (Kb) 6792 [startup+500.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1065 0 0 0 49992 6 0 0 25 0 1 0 1784112047 4780032 1052 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1167 1052 145 145 0 1022 0 [pid=14275] vsize: 4668 Current children cumulated CPU time (s) 499.99 Current children cumulated vsize (Kb) 6792 [startup+510.044 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1065 0 0 0 50993 6 0 0 25 0 1 0 1784112047 4780032 1052 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1167 1052 145 145 0 1022 0 [pid=14275] vsize: 4668 Current children cumulated CPU time (s) 510 Current children cumulated vsize (Kb) 6792 [startup+520.045 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1066 0 0 0 51993 6 0 0 25 0 1 0 1784112047 4780032 1053 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1167 1053 145 145 0 1022 0 [pid=14275] vsize: 4668 Current children cumulated CPU time (s) 520 Current children cumulated vsize (Kb) 6792 [startup+530.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1067 0 0 0 52993 6 0 0 25 0 1 0 1784112047 4780032 1054 4294967295 134512640 135094434 3221224448 3221223120 134556275 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1167 1054 145 145 0 1022 0 [pid=14275] vsize: 4668 Current children cumulated CPU time (s) 530 Current children cumulated vsize (Kb) 6792 [startup+540.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1067 0 0 0 53993 6 0 0 25 0 1 0 1784112047 4780032 1054 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1167 1054 145 145 0 1022 0 [pid=14275] vsize: 4668 Current children cumulated CPU time (s) 540 Current children cumulated vsize (Kb) 6792 [startup+550.047 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1073 0 0 0 54994 6 0 0 25 0 1 0 1784112047 4812800 1060 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1175 1060 145 145 0 1030 0 [pid=14275] vsize: 4700 Current children cumulated CPU time (s) 550.01 Current children cumulated vsize (Kb) 6824 [startup+560.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1073 0 0 0 55994 6 0 0 25 0 1 0 1784112047 4812800 1060 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1175 1060 145 145 0 1030 0 [pid=14275] vsize: 4700 Current children cumulated CPU time (s) 560.01 Current children cumulated vsize (Kb) 6824 [startup+570.049 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1079 0 0 0 56994 6 0 0 25 0 1 0 1784112047 4845568 1066 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1183 1066 145 145 0 1038 0 [pid=14275] vsize: 4732 Current children cumulated CPU time (s) 570.01 Current children cumulated vsize (Kb) 6856 [startup+580.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1079 0 0 0 57994 6 0 0 25 0 1 0 1784112047 4845568 1066 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1183 1066 145 145 0 1038 0 [pid=14275] vsize: 4732 Current children cumulated CPU time (s) 580.01 Current children cumulated vsize (Kb) 6856 [startup+590.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1086 0 0 0 58994 6 0 0 25 0 1 0 1784112047 4878336 1073 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1191 1073 145 145 0 1046 0 [pid=14275] vsize: 4764 Current children cumulated CPU time (s) 590.01 Current children cumulated vsize (Kb) 6888 [startup+600.051 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1086 0 0 0 59995 6 0 0 25 0 1 0 1784112047 4878336 1073 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1191 1073 145 145 0 1046 0 [pid=14275] vsize: 4764 Current children cumulated CPU time (s) 600.02 Current children cumulated vsize (Kb) 6888 [startup+610.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1092 0 0 0 60995 6 0 0 25 0 1 0 1784112047 4911104 1079 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1199 1079 145 145 0 1054 0 [pid=14275] vsize: 4796 Current children cumulated CPU time (s) 610.02 Current children cumulated vsize (Kb) 6920 [startup+620.053 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1093 0 0 0 61995 6 0 0 25 0 1 0 1784112047 4911104 1080 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1199 1080 145 145 0 1054 0 [pid=14275] vsize: 4796 Current children cumulated CPU time (s) 620.02 Current children cumulated vsize (Kb) 6920 [startup+630.054 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1093 0 0 0 62995 6 0 0 25 0 1 0 1784112047 4911104 1080 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1199 1080 145 145 0 1054 0 [pid=14275] vsize: 4796 Current children cumulated CPU time (s) 630.02 Current children cumulated vsize (Kb) 6920 [startup+640.054 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1093 0 0 0 63995 7 0 0 25 0 1 0 1784112047 4911104 1080 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1199 1080 145 145 0 1054 0 [pid=14275] vsize: 4796 Current children cumulated CPU time (s) 640.03 Current children cumulated vsize (Kb) 6920 [startup+650.055 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1093 0 0 0 64996 7 0 0 25 0 1 0 1784112047 4911104 1080 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1199 1080 145 145 0 1054 0 [pid=14275] vsize: 4796 Current children cumulated CPU time (s) 650.04 Current children cumulated vsize (Kb) 6920 [startup+660.056 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1100 0 0 0 65996 7 0 0 25 0 1 0 1784112047 4943872 1087 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1207 1087 145 145 0 1062 0 [pid=14275] vsize: 4828 Current children cumulated CPU time (s) 660.04 Current children cumulated vsize (Kb) 6952 [startup+670.058 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1100 0 0 0 66996 7 0 0 25 0 1 0 1784112047 4943872 1087 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1207 1087 145 145 0 1062 0 [pid=14275] vsize: 4828 Current children cumulated CPU time (s) 670.04 Current children cumulated vsize (Kb) 6952 [startup+680.059 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 67997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0 [pid=14275] vsize: 4860 Current children cumulated CPU time (s) 680.05 Current children cumulated vsize (Kb) 6984 [startup+690.059 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 68997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0 [pid=14275] vsize: 4860 Current children cumulated CPU time (s) 690.05 Current children cumulated vsize (Kb) 6984 [startup+700.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 69997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0 [pid=14275] vsize: 4860 Current children cumulated CPU time (s) 700.05 Current children cumulated vsize (Kb) 6984 [startup+710.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 70997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0 [pid=14275] vsize: 4860 Current children cumulated CPU time (s) 710.05 Current children cumulated vsize (Kb) 6984 [startup+720.061 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 71997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0 [pid=14275] vsize: 4860 Current children cumulated CPU time (s) 720.05 Current children cumulated vsize (Kb) 6984 [startup+730.062 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 72998 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0 [pid=14275] vsize: 4860 Current children cumulated CPU time (s) 730.06 Current children cumulated vsize (Kb) 6984 [startup+740.063 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 73998 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0 [pid=14275] vsize: 4860 Current children cumulated CPU time (s) 740.06 Current children cumulated vsize (Kb) 6984 [startup+750.064 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1109 0 0 0 74998 7 0 0 25 0 1 0 1784112047 4976640 1096 4294967295 134512640 135094434 3221224448 3221223040 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1215 1096 145 145 0 1070 0 [pid=14275] vsize: 4860 Current children cumulated CPU time (s) 750.06 Current children cumulated vsize (Kb) 6984 [startup+760.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1136 0 0 0 75997 7 0 0 25 0 1 0 1784112047 5091328 1123 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1243 1123 145 145 0 1098 0 [pid=14275] vsize: 4972 Current children cumulated CPU time (s) 760.05 Current children cumulated vsize (Kb) 7096 [startup+770.066 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1136 0 0 0 76998 7 0 0 25 0 1 0 1784112047 5091328 1123 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1243 1123 145 145 0 1098 0 [pid=14275] vsize: 4972 Current children cumulated CPU time (s) 770.06 Current children cumulated vsize (Kb) 7096 [startup+780.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1136 0 0 0 77998 7 0 0 25 0 1 0 1784112047 5091328 1123 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1243 1123 145 145 0 1098 0 [pid=14275] vsize: 4972 Current children cumulated CPU time (s) 780.06 Current children cumulated vsize (Kb) 7096 [startup+790.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1136 0 0 0 78998 7 0 0 25 0 1 0 1784112047 5091328 1123 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1243 1123 145 145 0 1098 0 [pid=14275] vsize: 4972 Current children cumulated CPU time (s) 790.06 Current children cumulated vsize (Kb) 7096 [startup+800.068 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1142 0 0 0 79998 7 0 0 25 0 1 0 1784112047 5124096 1129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1251 1129 145 145 0 1106 0 [pid=14275] vsize: 5004 Current children cumulated CPU time (s) 800.06 Current children cumulated vsize (Kb) 7128 [startup+810.069 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1147 0 0 0 80999 7 0 0 25 0 1 0 1784112047 5156864 1134 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1259 1134 145 145 0 1114 0 [pid=14275] vsize: 5036 Current children cumulated CPU time (s) 810.07 Current children cumulated vsize (Kb) 7160 [startup+820.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1147 0 0 0 81999 7 0 0 25 0 1 0 1784112047 5156864 1134 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1259 1134 145 145 0 1114 0 [pid=14275] vsize: 5036 Current children cumulated CPU time (s) 820.07 Current children cumulated vsize (Kb) 7160 [startup+830.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1147 0 0 0 82999 7 0 0 25 0 1 0 1784112047 5156864 1134 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1259 1134 145 145 0 1114 0 [pid=14275] vsize: 5036 Current children cumulated CPU time (s) 830.07 Current children cumulated vsize (Kb) 7160 [startup+840.072 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1147 0 0 0 83999 7 0 0 25 0 1 0 1784112047 5156864 1134 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1259 1134 145 145 0 1114 0 [pid=14275] vsize: 5036 Current children cumulated CPU time (s) 840.07 Current children cumulated vsize (Kb) 7160 [startup+850.073 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1148 0 0 0 85000 7 0 0 25 0 1 0 1784112047 5156864 1135 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1259 1135 145 145 0 1114 0 [pid=14275] vsize: 5036 Current children cumulated CPU time (s) 850.08 Current children cumulated vsize (Kb) 7160 [startup+860.074 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1149 0 0 0 86000 7 0 0 25 0 1 0 1784112047 5156864 1136 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1259 1136 145 145 0 1114 0 [pid=14275] vsize: 5036 Current children cumulated CPU time (s) 860.08 Current children cumulated vsize (Kb) 7160 [startup+870.075 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1155 0 0 0 87000 7 0 0 25 0 1 0 1784112047 5189632 1142 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1267 1142 145 145 0 1122 0 [pid=14275] vsize: 5068 Current children cumulated CPU time (s) 870.08 Current children cumulated vsize (Kb) 7192 [startup+880.076 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1160 0 0 0 88000 7 0 0 25 0 1 0 1784112047 5222400 1147 4294967295 134512640 135094434 3221224448 3221223060 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1275 1147 145 145 0 1130 0 [pid=14275] vsize: 5100 Current children cumulated CPU time (s) 880.08 Current children cumulated vsize (Kb) 7224 [startup+890.077 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1162 0 0 0 89000 7 0 0 25 0 1 0 1784112047 5222400 1149 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1275 1149 145 145 0 1130 0 [pid=14275] vsize: 5100 Current children cumulated CPU time (s) 890.08 Current children cumulated vsize (Kb) 7224 [startup+900.078 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1163 0 0 0 90001 7 0 0 25 0 1 0 1784112047 5222400 1150 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1275 1150 145 145 0 1130 0 [pid=14275] vsize: 5100 Current children cumulated CPU time (s) 900.09 Current children cumulated vsize (Kb) 7224 [startup+910.079 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1163 0 0 0 91001 7 0 0 25 0 1 0 1784112047 5222400 1150 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1275 1150 145 145 0 1130 0 [pid=14275] vsize: 5100 Current children cumulated CPU time (s) 910.09 Current children cumulated vsize (Kb) 7224 [startup+920.081 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1163 0 0 0 92001 7 0 0 25 0 1 0 1784112047 5222400 1150 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1275 1150 145 145 0 1130 0 [pid=14275] vsize: 5100 Current children cumulated CPU time (s) 920.09 Current children cumulated vsize (Kb) 7224 [startup+930.081 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1163 0 0 0 93002 7 0 0 25 0 1 0 1784112047 5222400 1150 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1275 1150 145 145 0 1130 0 [pid=14275] vsize: 5100 Current children cumulated CPU time (s) 930.1 Current children cumulated vsize (Kb) 7224 [startup+940.082 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1168 0 0 0 94002 7 0 0 25 0 1 0 1784112047 5255168 1155 4294967295 134512640 135094434 3221224448 3221223040 134551469 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1283 1155 145 145 0 1138 0 [pid=14275] vsize: 5132 Current children cumulated CPU time (s) 940.1 Current children cumulated vsize (Kb) 7256 [startup+950.083 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1168 0 0 0 95002 7 0 0 25 0 1 0 1784112047 5255168 1155 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1283 1155 145 145 0 1138 0 [pid=14275] vsize: 5132 Current children cumulated CPU time (s) 950.1 Current children cumulated vsize (Kb) 7256 [startup+960.084 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1168 0 0 0 96002 7 0 0 25 0 1 0 1784112047 5255168 1155 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1283 1155 145 145 0 1138 0 [pid=14275] vsize: 5132 Current children cumulated CPU time (s) 960.1 Current children cumulated vsize (Kb) 7256 [startup+970.086 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1169 0 0 0 97003 7 0 0 25 0 1 0 1784112047 5255168 1156 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1283 1156 145 145 0 1138 0 [pid=14275] vsize: 5132 Current children cumulated CPU time (s) 970.11 Current children cumulated vsize (Kb) 7256 [startup+980.087 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1170 0 0 0 98003 7 0 0 25 0 1 0 1784112047 5255168 1157 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1283 1157 145 145 0 1138 0 [pid=14275] vsize: 5132 Current children cumulated CPU time (s) 980.11 Current children cumulated vsize (Kb) 7256 [startup+990.087 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1170 0 0 0 99003 7 0 0 25 0 1 0 1784112047 5255168 1157 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1283 1157 145 145 0 1138 0 [pid=14275] vsize: 5132 Current children cumulated CPU time (s) 990.11 Current children cumulated vsize (Kb) 7256 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1175 0 0 0 100003 7 0 0 25 0 1 0 1784112047 5287936 1162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1291 1162 145 145 0 1146 0 [pid=14275] vsize: 5164 Current children cumulated CPU time (s) 1000.11 Current children cumulated vsize (Kb) 7288 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1177 0 0 0 101003 7 0 0 25 0 1 0 1784112047 5287936 1164 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1291 1164 145 145 0 1146 0 [pid=14275] vsize: 5164 Current children cumulated CPU time (s) 1010.11 Current children cumulated vsize (Kb) 7288 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1182 0 0 0 102004 7 0 0 25 0 1 0 1784112047 5320704 1169 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1299 1169 145 145 0 1154 0 [pid=14275] vsize: 5196 Current children cumulated CPU time (s) 1020.12 Current children cumulated vsize (Kb) 7320 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1183 0 0 0 103004 7 0 0 25 0 1 0 1784112047 5320704 1170 4294967295 134512640 135094434 3221224448 3221223120 134554867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1299 1170 145 145 0 1154 0 [pid=14275] vsize: 5196 Current children cumulated CPU time (s) 1030.12 Current children cumulated vsize (Kb) 7320 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1184 0 0 0 104004 7 0 0 25 0 1 0 1784112047 5320704 1171 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1299 1171 145 145 0 1154 0 [pid=14275] vsize: 5196 Current children cumulated CPU time (s) 1040.12 Current children cumulated vsize (Kb) 7320 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1184 0 0 0 105005 7 0 0 25 0 1 0 1784112047 5320704 1171 4294967295 134512640 135094434 3221224448 3221222992 134562048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1299 1171 145 145 0 1154 0 [pid=14275] vsize: 5196 Current children cumulated CPU time (s) 1050.13 Current children cumulated vsize (Kb) 7320 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1197 0 0 0 106005 7 0 0 25 0 1 0 1784112047 5386240 1184 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1315 1184 145 145 0 1170 0 [pid=14275] vsize: 5260 Current children cumulated CPU time (s) 1060.13 Current children cumulated vsize (Kb) 7384 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1205 0 0 0 107005 7 0 0 25 0 1 0 1784112047 5414912 1192 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1322 1192 145 145 0 1177 0 [pid=14275] vsize: 5288 Current children cumulated CPU time (s) 1070.13 Current children cumulated vsize (Kb) 7412 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1205 0 0 0 108005 7 0 0 25 0 1 0 1784112047 5414912 1192 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1322 1192 145 145 0 1177 0 [pid=14275] vsize: 5288 Current children cumulated CPU time (s) 1080.13 Current children cumulated vsize (Kb) 7412 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1205 0 0 0 109005 7 0 0 25 0 1 0 1784112047 5414912 1192 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1322 1192 145 145 0 1177 0 [pid=14275] vsize: 5288 Current children cumulated CPU time (s) 1090.13 Current children cumulated vsize (Kb) 7412 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1205 0 0 0 110005 7 0 0 25 0 1 0 1784112047 5414912 1192 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1322 1192 145 145 0 1177 0 [pid=14275] vsize: 5288 Current children cumulated CPU time (s) 1100.13 Current children cumulated vsize (Kb) 7412 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1206 0 0 0 111006 7 0 0 25 0 1 0 1784112047 5414912 1193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1322 1193 145 145 0 1177 0 [pid=14275] vsize: 5288 Current children cumulated CPU time (s) 1110.14 Current children cumulated vsize (Kb) 7412 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1206 0 0 0 112006 7 0 0 25 0 1 0 1784112047 5414912 1193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1322 1193 145 145 0 1177 0 [pid=14275] vsize: 5288 Current children cumulated CPU time (s) 1120.14 Current children cumulated vsize (Kb) 7412 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1206 0 0 0 113006 7 0 0 25 0 1 0 1784112047 5414912 1193 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1322 1193 145 145 0 1177 0 [pid=14275] vsize: 5288 Current children cumulated CPU time (s) 1130.14 Current children cumulated vsize (Kb) 7412 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1206 0 0 0 114006 7 0 0 25 0 1 0 1784112047 5414912 1193 4294967295 134512640 135094434 3221224448 3221223072 134562092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1322 1193 145 145 0 1177 0 [pid=14275] vsize: 5288 Current children cumulated CPU time (s) 1140.14 Current children cumulated vsize (Kb) 7412 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1213 0 0 0 115007 7 0 0 25 0 1 0 1784112047 5447680 1200 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1330 1200 145 145 0 1185 0 [pid=14275] vsize: 5320 Current children cumulated CPU time (s) 1150.15 Current children cumulated vsize (Kb) 7444 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1213 0 0 0 116006 8 0 0 25 0 1 0 1784112047 5447680 1200 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14275/statm): 1330 1200 145 145 0 1185 0 [pid=14275] vsize: 5320 Current children cumulated CPU time (s) 1160.15 Current children cumulated vsize (Kb) 7444 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1231 0 0 0 117006 8 0 0 25 0 1 0 1784112047 5578752 1218 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1362 1218 145 145 0 1217 0 [pid=14275] vsize: 5448 Current children cumulated CPU time (s) 1170.15 Current children cumulated vsize (Kb) 7572 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1235 0 0 0 118006 8 0 0 25 0 1 0 1784112047 5595136 1222 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1366 1222 145 145 0 1221 0 [pid=14275] vsize: 5464 Current children cumulated CPU time (s) 1180.15 Current children cumulated vsize (Kb) 7588 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1235 0 0 0 119006 8 0 0 25 0 1 0 1784112047 5595136 1222 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1366 1222 145 145 0 1221 0 [pid=14275] vsize: 5464 Current children cumulated CPU time (s) 1190.15 Current children cumulated vsize (Kb) 7588 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1240 0 0 0 120006 8 0 0 25 0 1 0 1784112047 5623808 1227 4294967295 134512640 135094434 3221224448 3221223072 134557694 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1373 1227 145 145 0 1228 0 [pid=14275] vsize: 5492 Current children cumulated CPU time (s) 1200.15 Current children cumulated vsize (Kb) 7616 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 14275 Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14271/statm): 531 226 485 147 0 384 0 [pid=14271] vsize: 2124 Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1240 0 0 0 120006 8 0 0 25 0 1 0 1784112047 5623808 1227 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14275/statm): 1373 1227 145 145 0 1228 0 [pid=14275] vsize: 5492 Current children cumulated CPU time (s) 1200.15 Current children cumulated vsize (Kb) 7616 Sending SIGTERM to -14271 Sleeping 2 seconds One traced child (pid=14271) ended because it received signal 15 (SIGTERM) One traced child (pid=14275) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1200.12 CPU time (s): 1200.16 CPU user time (s): 1200.07 CPU system time (s): 0.088986 CPU usage (%): 100.003 Max. virtual memory (cumulated for all children) (Kb): 7616
ERROR: no interpretation found !