Name | submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-mux.opb |
MD5SUM | fa7153262db792d01bec14f5a651af5b |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 872 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 232 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 9597 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 9597 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 18.0453 |
Number of variables | 232 |
Total number of constraints | 527 |
Number of constraints which are clauses | 527 |
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 | 27 |
LAUNCH ON wulflinc13 THE 2005-09-18 18:10:58 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2597 boxname=wulflinc13 idbench=253 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fa7153262db792d01bec14f5a651af5b /oldhome/oroussel/tmp/wulflinc13/normalized-mux.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mux.opb IDLAUNCH: 2597 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 882840 kB Buffers: 34096 kB Cached: 91472 kB SwapCached: 708 kB Active: 65260 kB Inactive: 62876 kB HighTotal: 131008 kB HighFree: 66556 kB LowTotal: 903652 kB LowFree: 816284 kB SwapTotal: 2097136 kB SwapFree: 2095936 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5740 kB Slab: 18048 kB Committed_AS: 64128 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 18:31:09 (client local time) WITH STATUS 10 IN 1209.28 SECONDS stats: 2597 7 1209.28 10
c Parsing PB file... c Converting 527 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 | 527 2331 | 175 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 1330[0m c ---[ 0]---> Sorter-cost:29793 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 71948 169106 | 23982 0 0 nan | 0.000 % | c | 100 | 71806 168786 | 26380 99 2955 29.8 | 0.129 % | c | 251 | 71806 168786 | 29018 250 6809 27.2 | 0.129 % | c | 477 | 71373 167811 | 31920 472 10592 22.4 | 0.579 % | c ============================================================================== c [1mFound solution: 1234[0m c ---[ 0]---> Sorter-cost:24283 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 513 | 131893 309118 | 43964 507 11929 23.5 | 0.579 % | c | 614 | 131893 309118 | 48360 608 14630 24.1 | 0.337 % | c | 765 | 131893 309118 | 53196 759 16948 22.3 | 0.337 % | c | 990 | 131893 309118 | 58516 984 20452 20.8 | 0.337 % | c | 1327 | 131793 308891 | 64367 1316 29130 22.1 | 0.398 % | c | 1833 | 131793 308891 | 70804 1822 42478 23.3 | 0.398 % | c | 2592 | 131771 308841 | 77884 2580 60031 23.3 | 0.409 % | c | 3733 | 131637 308542 | 85673 3717 88874 23.9 | 0.482 % | c ============================================================================== c [1mFound solution: 1233[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4682 | 131826 309294 | 43942 4666 147647 31.6 | 0.482 % | c | 4783 | 131826 309294 | 48336 4767 149006 31.3 | 0.483 % | c ============================================================================== c [1mFound solution: 1199[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4810 | 132099 309958 | 44033 4794 152722 31.9 | 0.483 % | c | 4910 | 132099 309958 | 48436 4894 157309 32.1 | 0.484 % | c | 5060 | 132099 309958 | 53279 5044 166454 33.0 | 0.484 % | c | 5285 | 132099 309958 | 58607 5269 177805 33.7 | 0.484 % | c | 5622 | 132099 309958 | 64468 5606 190601 34.0 | 0.484 % | c | 6128 | 131993 309729 | 70915 6108 202232 33.1 | 0.557 % | c | 6889 | 131993 309729 | 78007 6869 218880 31.9 | 0.557 % | c | 8029 | 131989 309720 | 85807 8008 393024 49.1 | 0.559 % | c | 9737 | 131989 309720 | 94388 9716 464106 47.8 | 0.559 % | c | 12300 | 131949 309629 | 103827 12275 614249 50.0 | 0.586 % | c ============================================================================== c [1mFound solution: 1196[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15838 | 132219 310293 | 44073 15813 1409395 89.1 | 0.586 % | c | 15939 | 132219 310293 | 48480 15914 1410776 88.6 | 0.588 % | c | 16089 | 132219 310293 | 53328 16064 1413959 88.0 | 0.588 % | c | 16316 | 132219 310293 | 58661 16291 1420583 87.2 | 0.588 % | c | 16653 | 132219 310293 | 64527 16628 1424998 85.7 | 0.588 % | c | 17160 | 132219 310293 | 70980 17135 1431067 83.5 | 0.588 % | c | 17920 | 132219 310293 | 78078 17895 1444512 80.7 | 0.588 % | c | 19059 | 132219 310293 | 85885 19034 1508888 79.3 | 0.588 % | c | 20768 | 132219 310293 | 94474 20743 1585879 76.5 | 0.588 % | c | 23330 | 132219 310293 | 103921 23305 1683334 72.2 | 0.588 % | c | 27176 | 132219 310293 | 114314 27151 1841999 67.8 | 0.588 % | c | 32944 | 132219 310293 | 125745 32919 2133960 64.8 | 0.588 % | c | 41593 | 132219 310293 | 138319 41568 2548271 61.3 | 0.588 % | c | 54567 | 132219 310293 | 152151 54542 3221898 59.1 | 0.588 % | c | 74029 | 132219 310293 | 167367 74004 4058574 54.8 | 0.588 % | c | 103224 | 132219 310293 | 184103 103199 5283147 51.2 | 0.588 % |
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/5568/stat): 5568 (minisat+_script) R 5567 5568 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785103563 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/5568/statm): 174 3 169 147 0 27 0 [pid=5568] 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=5569 New process pid=5570 New process pid=5571 execve syscall for /bin/sed executable One traced child (pid=5570) 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=5571) exited with status: 0 One traced child (pid=5569) exited with status: 0 New process pid=5572 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mux.opb [startup+10.0033 s] Raw data (loadavg): 0.92 0.95 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4197 0 0 0 964 18 0 0 25 0 1 0 1785103568 18714624 3999 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 4569 3999 145 145 0 4424 0 [pid=5572] vsize: 18276 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 20400 [startup+20.0049 s] Raw data (loadavg): 0.93 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4289 0 0 0 1962 19 0 0 25 0 1 0 1785103568 19083264 4091 4294967295 134512640 135094434 3221224448 3221223104 134558295 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 4659 4091 145 145 0 4514 0 [pid=5572] vsize: 18636 Current children cumulated CPU time (s) 19.82 Current children cumulated vsize (Kb) 20760 [startup+30.0056 s] Raw data (loadavg): 0.94 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4492 0 0 0 2960 20 0 0 25 0 1 0 1785103568 19902464 4290 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 4859 4290 145 145 0 4714 0 [pid=5572] vsize: 19436 Current children cumulated CPU time (s) 29.81 Current children cumulated vsize (Kb) 21560 [startup+40.0062 s] Raw data (loadavg): 0.95 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4503 0 0 0 3960 20 0 0 25 0 1 0 1785103568 19943424 4301 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 4869 4301 145 145 0 4724 0 [pid=5572] vsize: 19476 Current children cumulated CPU time (s) 39.81 Current children cumulated vsize (Kb) 21600 [startup+50.0079 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4694 0 0 0 4957 22 0 0 25 0 1 0 1785103568 20721664 4492 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 5059 4492 145 145 0 4914 0 [pid=5572] vsize: 20236 Current children cumulated CPU time (s) 49.8 Current children cumulated vsize (Kb) 22360 [startup+60.0085 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4768 0 0 0 5955 23 0 0 25 0 1 0 1785103568 21045248 4566 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 5138 4566 145 145 0 4993 0 [pid=5572] vsize: 20552 Current children cumulated CPU time (s) 59.79 Current children cumulated vsize (Kb) 22676 [startup+70.0102 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4890 0 0 0 6953 24 0 0 25 0 1 0 1785103568 21553152 4688 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 5262 4688 145 145 0 5117 0 [pid=5572] vsize: 21048 Current children cumulated CPU time (s) 69.78 Current children cumulated vsize (Kb) 23172 [startup+80.0118 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5000 0 0 0 7951 25 0 0 25 0 1 0 1785103568 21995520 4798 4294967295 134512640 135094434 3221224448 3221223040 134556975 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 5370 4798 145 145 0 5225 0 [pid=5572] vsize: 21480 Current children cumulated CPU time (s) 79.77 Current children cumulated vsize (Kb) 23604 [startup+90.0125 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5278 0 0 0 8945 27 0 0 25 0 1 0 1785103568 23130112 5076 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 5647 5076 145 145 0 5502 0 [pid=5572] vsize: 22588 Current children cumulated CPU time (s) 89.73 Current children cumulated vsize (Kb) 24712 [startup+100.013 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5557 0 0 0 9940 29 0 0 25 0 1 0 1785103568 24268800 5355 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 5925 5355 145 145 0 5780 0 [pid=5572] vsize: 23700 Current children cumulated CPU time (s) 99.7 Current children cumulated vsize (Kb) 25824 [startup+110.014 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5829 0 0 0 10937 31 0 0 25 0 1 0 1785103568 25382912 5627 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6197 5627 145 145 0 6052 0 [pid=5572] vsize: 24788 Current children cumulated CPU time (s) 109.69 Current children cumulated vsize (Kb) 26912 [startup+120.015 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5874 0 0 0 11936 31 0 0 25 0 1 0 1785103568 25567232 5672 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6242 5672 145 145 0 6097 0 [pid=5572] vsize: 24968 Current children cumulated CPU time (s) 119.68 Current children cumulated vsize (Kb) 27092 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5939 0 0 0 12935 32 0 0 25 0 1 0 1785103568 25833472 5737 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6307 5737 145 145 0 6162 0 [pid=5572] vsize: 25228 Current children cumulated CPU time (s) 129.68 Current children cumulated vsize (Kb) 27352 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6021 0 0 0 13933 33 0 0 25 0 1 0 1785103568 26169344 5819 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6389 5819 145 145 0 6244 0 [pid=5572] vsize: 25556 Current children cumulated CPU time (s) 139.67 Current children cumulated vsize (Kb) 27680 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6084 0 0 0 14931 34 0 0 25 0 1 0 1785103568 26427392 5882 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6452 5882 145 145 0 6307 0 [pid=5572] vsize: 25808 Current children cumulated CPU time (s) 149.66 Current children cumulated vsize (Kb) 27932 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6152 0 0 0 15929 36 0 0 25 0 1 0 1785103568 26705920 5950 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6520 5950 145 145 0 6375 0 [pid=5572] vsize: 26080 Current children cumulated CPU time (s) 159.66 Current children cumulated vsize (Kb) 28204 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6226 0 0 0 16927 37 0 0 25 0 1 0 1785103568 27009024 6024 4294967295 134512640 135094434 3221224448 3221223088 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6594 6024 145 145 0 6449 0 [pid=5572] vsize: 26376 Current children cumulated CPU time (s) 169.65 Current children cumulated vsize (Kb) 28500 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6308 0 0 0 17925 38 0 0 25 0 1 0 1785103568 27344896 6106 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6676 6106 145 145 0 6531 0 [pid=5572] vsize: 26704 Current children cumulated CPU time (s) 179.64 Current children cumulated vsize (Kb) 28828 [startup+190.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6374 0 0 0 18924 39 0 0 25 0 1 0 1785103568 27615232 6172 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6742 6172 145 145 0 6597 0 [pid=5572] vsize: 26968 Current children cumulated CPU time (s) 189.64 Current children cumulated vsize (Kb) 29092 [startup+200.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6439 0 0 0 19923 40 0 0 25 0 1 0 1785103568 27881472 6237 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6807 6237 145 145 0 6662 0 [pid=5572] vsize: 27228 Current children cumulated CPU time (s) 199.64 Current children cumulated vsize (Kb) 29352 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6501 0 0 0 20922 40 0 0 25 0 1 0 1785103568 28135424 6299 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6869 6299 145 145 0 6724 0 [pid=5572] vsize: 27476 Current children cumulated CPU time (s) 209.63 Current children cumulated vsize (Kb) 29600 [startup+220.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6571 0 0 0 21920 41 0 0 25 0 1 0 1785103568 28422144 6369 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 6939 6369 145 145 0 6794 0 [pid=5572] vsize: 27756 Current children cumulated CPU time (s) 219.62 Current children cumulated vsize (Kb) 29880 [startup+230.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6647 0 0 0 22919 42 0 0 25 0 1 0 1785103568 28733440 6445 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7015 6445 145 145 0 6870 0 [pid=5572] vsize: 28060 Current children cumulated CPU time (s) 229.62 Current children cumulated vsize (Kb) 30184 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6696 0 0 0 23918 43 0 0 25 0 1 0 1785103568 29061120 6494 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7095 6494 145 145 0 6950 0 [pid=5572] vsize: 28380 Current children cumulated CPU time (s) 239.62 Current children cumulated vsize (Kb) 30504 [startup+250.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6762 0 0 0 24917 43 0 0 25 0 1 0 1785103568 29323264 6560 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7159 6560 145 145 0 7014 0 [pid=5572] vsize: 28636 Current children cumulated CPU time (s) 249.61 Current children cumulated vsize (Kb) 30760 [startup+260.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6829 0 0 0 25916 44 0 0 25 0 1 0 1785103568 29593600 6627 4294967295 134512640 135094434 3221224448 3221223040 134557042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7225 6627 145 145 0 7080 0 [pid=5572] vsize: 28900 Current children cumulated CPU time (s) 259.61 Current children cumulated vsize (Kb) 31024 [startup+270.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6897 0 0 0 26915 45 0 0 25 0 1 0 1785103568 29872128 6695 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7293 6695 145 145 0 7148 0 [pid=5572] vsize: 29172 Current children cumulated CPU time (s) 269.61 Current children cumulated vsize (Kb) 31296 [startup+280.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6961 0 0 0 27914 45 0 0 25 0 1 0 1785103568 30126080 6759 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7355 6759 145 145 0 7210 0 [pid=5572] vsize: 29420 Current children cumulated CPU time (s) 279.6 Current children cumulated vsize (Kb) 31544 [startup+290.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7024 0 0 0 28912 46 0 0 25 0 1 0 1785103568 30371840 6822 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7415 6822 145 145 0 7270 0 [pid=5572] vsize: 29660 Current children cumulated CPU time (s) 289.59 Current children cumulated vsize (Kb) 31784 [startup+300.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7081 0 0 0 29911 47 0 0 25 0 1 0 1785103568 30601216 6879 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7471 6879 145 145 0 7326 0 [pid=5572] vsize: 29884 Current children cumulated CPU time (s) 299.59 Current children cumulated vsize (Kb) 32008 [startup+310.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7137 0 0 0 30910 47 0 0 25 0 1 0 1785103568 30826496 6935 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7526 6935 145 145 0 7381 0 [pid=5572] vsize: 30104 Current children cumulated CPU time (s) 309.58 Current children cumulated vsize (Kb) 32228 [startup+320.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7206 0 0 0 31909 48 0 0 25 0 1 0 1785103568 31117312 7004 4294967295 134512640 135094434 3221224448 3221223072 134557606 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7597 7004 145 145 0 7452 0 [pid=5572] vsize: 30388 Current children cumulated CPU time (s) 319.58 Current children cumulated vsize (Kb) 32512 [startup+330.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7285 0 0 0 32908 48 0 0 25 0 1 0 1785103568 31424512 7083 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7672 7083 145 145 0 7527 0 [pid=5572] vsize: 30688 Current children cumulated CPU time (s) 329.57 Current children cumulated vsize (Kb) 32812 [startup+340.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7347 0 0 0 33906 49 0 0 25 0 1 0 1785103568 31674368 7145 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7733 7145 145 145 0 7588 0 [pid=5572] vsize: 30932 Current children cumulated CPU time (s) 339.56 Current children cumulated vsize (Kb) 33056 [startup+350.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7421 0 0 0 34905 50 0 0 25 0 1 0 1785103568 31973376 7219 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7806 7219 145 145 0 7661 0 [pid=5572] vsize: 31224 Current children cumulated CPU time (s) 349.56 Current children cumulated vsize (Kb) 33348 [startup+360.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7494 0 0 0 35904 51 0 0 25 0 1 0 1785103568 32260096 7292 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7876 7292 145 145 0 7731 0 [pid=5572] vsize: 31504 Current children cumulated CPU time (s) 359.56 Current children cumulated vsize (Kb) 33628 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7578 0 0 0 36903 51 0 0 25 0 1 0 1785103568 32600064 7376 4294967295 134512640 135094434 3221224448 3221223040 134557042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 7959 7376 145 145 0 7814 0 [pid=5572] vsize: 31836 Current children cumulated CPU time (s) 369.55 Current children cumulated vsize (Kb) 33960 [startup+380.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7652 0 0 0 37902 52 0 0 25 0 1 0 1785103568 32899072 7450 4294967295 134512640 135094434 3221224448 3221223040 134557182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8032 7450 145 145 0 7887 0 [pid=5572] vsize: 32128 Current children cumulated CPU time (s) 379.55 Current children cumulated vsize (Kb) 34252 [startup+390.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7726 0 0 0 38899 53 0 0 25 0 1 0 1785103568 33198080 7524 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8105 7524 145 145 0 7960 0 [pid=5572] vsize: 32420 Current children cumulated CPU time (s) 389.53 Current children cumulated vsize (Kb) 34544 [startup+400.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7789 0 0 0 39898 53 0 0 25 0 1 0 1785103568 33452032 7587 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8167 7587 145 145 0 8022 0 [pid=5572] vsize: 32668 Current children cumulated CPU time (s) 399.52 Current children cumulated vsize (Kb) 34792 [startup+410.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7861 0 0 0 40897 54 0 0 25 0 1 0 1785103568 33742848 7659 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8238 7659 145 145 0 8093 0 [pid=5572] vsize: 32952 Current children cumulated CPU time (s) 409.52 Current children cumulated vsize (Kb) 35076 [startup+420.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7917 0 0 0 41897 54 0 0 25 0 1 0 1785103568 33980416 7715 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8296 7715 145 145 0 8151 0 [pid=5572] vsize: 33184 Current children cumulated CPU time (s) 419.52 Current children cumulated vsize (Kb) 35308 [startup+430.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7988 0 0 0 42895 55 0 0 25 0 1 0 1785103568 34267136 7786 4294967295 134512640 135094434 3221224448 3221223040 134557363 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8366 7786 145 145 0 8221 0 [pid=5572] vsize: 33464 Current children cumulated CPU time (s) 429.51 Current children cumulated vsize (Kb) 35588 [startup+440.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8046 0 0 0 43893 56 0 0 25 0 1 0 1785103568 34525184 7844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 8429 7844 145 145 0 8284 0 [pid=5572] vsize: 33716 Current children cumulated CPU time (s) 439.5 Current children cumulated vsize (Kb) 35840 [startup+450.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8117 0 0 0 44892 57 0 0 25 0 1 0 1785103568 34816000 7915 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8500 7915 145 145 0 8355 0 [pid=5572] vsize: 34000 Current children cumulated CPU time (s) 449.5 Current children cumulated vsize (Kb) 36124 [startup+460.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8171 0 0 0 45891 57 0 0 25 0 1 0 1785103568 35061760 7969 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8560 7969 145 145 0 8415 0 [pid=5572] vsize: 34240 Current children cumulated CPU time (s) 459.49 Current children cumulated vsize (Kb) 36364 [startup+470.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8218 0 0 0 46891 58 0 0 25 0 1 0 1785103568 35250176 8016 4294967295 134512640 135094434 3221224448 3221223112 134556595 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8606 8016 145 145 0 8461 0 [pid=5572] vsize: 34424 Current children cumulated CPU time (s) 469.5 Current children cumulated vsize (Kb) 36548 [startup+480.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8263 0 0 0 47889 58 0 0 25 0 1 0 1785103568 35430400 8061 4294967295 134512640 135094434 3221224448 3221223072 134557660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8650 8061 145 145 0 8505 0 [pid=5572] vsize: 34600 Current children cumulated CPU time (s) 479.48 Current children cumulated vsize (Kb) 36724 [startup+490.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8311 0 0 0 48888 59 0 0 25 0 1 0 1785103568 35627008 8109 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8698 8109 145 145 0 8553 0 [pid=5572] vsize: 34792 Current children cumulated CPU time (s) 489.48 Current children cumulated vsize (Kb) 36916 [startup+500.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8353 0 0 0 49887 59 0 0 25 0 1 0 1785103568 35799040 8151 4294967295 134512640 135094434 3221224448 3221223072 134557616 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 8740 8151 145 145 0 8595 0 [pid=5572] vsize: 34960 Current children cumulated CPU time (s) 499.47 Current children cumulated vsize (Kb) 37084 [startup+510.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8404 0 0 0 50886 59 0 0 24 0 1 0 1785103568 35999744 8202 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 8789 8202 145 145 0 8644 0 [pid=5572] vsize: 35156 Current children cumulated CPU time (s) 509.46 Current children cumulated vsize (Kb) 37280 [startup+520.047 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8460 0 0 0 51885 60 0 0 25 0 1 0 1785103568 36229120 8258 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 8845 8258 145 145 0 8700 0 [pid=5572] vsize: 35380 Current children cumulated CPU time (s) 519.46 Current children cumulated vsize (Kb) 37504 [startup+530.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8519 0 0 0 52884 62 0 0 25 0 1 0 1785103568 36462592 8317 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 8902 8317 145 145 0 8757 0 [pid=5572] vsize: 35608 Current children cumulated CPU time (s) 529.47 Current children cumulated vsize (Kb) 37732 [startup+540.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8566 0 0 0 53882 62 0 0 25 0 1 0 1785103568 36651008 8364 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 8948 8364 145 145 0 8803 0 [pid=5572] vsize: 35792 Current children cumulated CPU time (s) 539.45 Current children cumulated vsize (Kb) 37916 [startup+550.05 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8624 0 0 0 54881 63 0 0 25 0 1 0 1785103568 36888576 8422 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9006 8422 145 145 0 8861 0 [pid=5572] vsize: 36024 Current children cumulated CPU time (s) 549.45 Current children cumulated vsize (Kb) 38148 [startup+560.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8674 0 0 0 55880 64 0 0 25 0 1 0 1785103568 37355520 8472 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9120 8472 145 145 0 8975 0 [pid=5572] vsize: 36480 Current children cumulated CPU time (s) 559.45 Current children cumulated vsize (Kb) 38604 [startup+570.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8719 0 0 0 56879 64 0 0 25 0 1 0 1785103568 37539840 8517 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9165 8517 145 145 0 9020 0 [pid=5572] vsize: 36660 Current children cumulated CPU time (s) 569.44 Current children cumulated vsize (Kb) 38784 [startup+580.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8771 0 0 0 57878 65 0 0 25 0 1 0 1785103568 37744640 8569 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9215 8569 145 145 0 9070 0 [pid=5572] vsize: 36860 Current children cumulated CPU time (s) 579.44 Current children cumulated vsize (Kb) 38984 [startup+590.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8814 0 0 0 58876 67 0 0 25 0 1 0 1785103568 37924864 8612 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9259 8612 145 145 0 9114 0 [pid=5572] vsize: 37036 Current children cumulated CPU time (s) 589.44 Current children cumulated vsize (Kb) 39160 [startup+600.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8863 0 0 0 59875 67 0 0 25 0 1 0 1785103568 38137856 8661 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9311 8661 145 145 0 9166 0 [pid=5572] vsize: 37244 Current children cumulated CPU time (s) 599.43 Current children cumulated vsize (Kb) 39368 [startup+610.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8903 0 0 0 60874 68 0 0 25 0 1 0 1785103568 38289408 8701 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9348 8701 145 145 0 9203 0 [pid=5572] vsize: 37392 Current children cumulated CPU time (s) 609.43 Current children cumulated vsize (Kb) 39516 [startup+620.057 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8950 0 0 0 61873 69 0 0 25 0 1 0 1785103568 38502400 8748 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9400 8748 145 145 0 9255 0 [pid=5572] vsize: 37600 Current children cumulated CPU time (s) 619.43 Current children cumulated vsize (Kb) 39724 [startup+630.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9009 0 0 0 62872 69 0 0 25 0 1 0 1785103568 38727680 8807 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9455 8807 145 145 0 9310 0 [pid=5572] vsize: 37820 Current children cumulated CPU time (s) 629.42 Current children cumulated vsize (Kb) 39944 [startup+640.059 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9056 0 0 0 63870 70 0 0 25 0 1 0 1785103568 38916096 8854 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9501 8854 145 145 0 9356 0 [pid=5572] vsize: 38004 Current children cumulated CPU time (s) 639.41 Current children cumulated vsize (Kb) 40128 [startup+650.06 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9099 0 0 0 64870 71 0 0 25 0 1 0 1785103568 39088128 8897 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9543 8897 145 145 0 9398 0 [pid=5572] vsize: 38172 Current children cumulated CPU time (s) 649.42 Current children cumulated vsize (Kb) 40296 [startup+660.061 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9159 0 0 0 65869 72 0 0 25 0 1 0 1785103568 39346176 8957 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9606 8957 145 145 0 9461 0 [pid=5572] vsize: 38424 Current children cumulated CPU time (s) 659.42 Current children cumulated vsize (Kb) 40548 [startup+670.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9211 0 0 0 66867 72 0 0 25 0 1 0 1785103568 39542784 9009 4294967295 134512640 135094434 3221224448 3221223076 134557637 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9654 9009 145 145 0 9509 0 [pid=5572] vsize: 38616 Current children cumulated CPU time (s) 669.4 Current children cumulated vsize (Kb) 40740 [startup+680.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9265 0 0 0 67866 73 0 0 25 0 1 0 1785103568 39759872 9063 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9707 9063 145 145 0 9562 0 [pid=5572] vsize: 38828 Current children cumulated CPU time (s) 679.4 Current children cumulated vsize (Kb) 40952 [startup+690.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9312 0 0 0 68865 73 0 0 25 0 1 0 1785103568 40009728 9110 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9768 9110 145 145 0 9623 0 [pid=5572] vsize: 39072 Current children cumulated CPU time (s) 689.39 Current children cumulated vsize (Kb) 41196 [startup+700.065 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9365 0 0 0 69864 74 0 0 25 0 1 0 1785103568 40222720 9163 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9820 9163 145 145 0 9675 0 [pid=5572] vsize: 39280 Current children cumulated CPU time (s) 699.39 Current children cumulated vsize (Kb) 41404 [startup+710.066 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9423 0 0 0 70863 75 0 0 25 0 1 0 1785103568 40456192 9221 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9877 9221 145 145 0 9732 0 [pid=5572] vsize: 39508 Current children cumulated CPU time (s) 709.39 Current children cumulated vsize (Kb) 41632 [startup+720.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9475 0 0 0 71861 76 0 0 25 0 1 0 1785103568 40673280 9273 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9930 9273 145 145 0 9785 0 [pid=5572] vsize: 39720 Current children cumulated CPU time (s) 719.38 Current children cumulated vsize (Kb) 41844 [startup+730.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9517 0 0 0 72860 76 0 0 25 0 1 0 1785103568 40837120 9315 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 9970 9315 145 145 0 9825 0 [pid=5572] vsize: 39880 Current children cumulated CPU time (s) 729.37 Current children cumulated vsize (Kb) 42004 [startup+740.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9573 0 0 0 73858 77 0 0 25 0 1 0 1785103568 41058304 9371 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10024 9371 145 145 0 9879 0 [pid=5572] vsize: 40096 Current children cumulated CPU time (s) 739.36 Current children cumulated vsize (Kb) 42220 [startup+750.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9612 0 0 0 74857 79 0 0 25 0 1 0 1785103568 41222144 9410 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10064 9410 145 145 0 9919 0 [pid=5572] vsize: 40256 Current children cumulated CPU time (s) 749.37 Current children cumulated vsize (Kb) 42380 [startup+760.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9665 0 0 0 75855 80 0 0 25 0 1 0 1785103568 41431040 9463 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10115 9463 145 145 0 9970 0 [pid=5572] vsize: 40460 Current children cumulated CPU time (s) 759.36 Current children cumulated vsize (Kb) 42584 [startup+770.071 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9724 0 0 0 76853 81 0 0 25 0 1 0 1785103568 41668608 9522 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10173 9522 145 145 0 10028 0 [pid=5572] vsize: 40692 Current children cumulated CPU time (s) 769.35 Current children cumulated vsize (Kb) 42816 [startup+780.073 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9773 0 0 0 77852 81 0 0 25 0 1 0 1785103568 41861120 9571 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10220 9571 145 145 0 10075 0 [pid=5572] vsize: 40880 Current children cumulated CPU time (s) 779.34 Current children cumulated vsize (Kb) 43004 [startup+790.073 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9823 0 0 0 78851 82 0 0 25 0 1 0 1785103568 42086400 9621 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10275 9621 145 145 0 10130 0 [pid=5572] vsize: 41100 Current children cumulated CPU time (s) 789.34 Current children cumulated vsize (Kb) 43224 [startup+800.075 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9871 0 0 0 79850 83 0 0 25 0 1 0 1785103568 42274816 9669 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10321 9669 145 145 0 10176 0 [pid=5572] vsize: 41284 Current children cumulated CPU time (s) 799.34 Current children cumulated vsize (Kb) 43408 [startup+810.077 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9937 0 0 0 80849 83 0 0 25 0 1 0 1785103568 42573824 9735 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10394 9735 145 145 0 10249 0 [pid=5572] vsize: 41576 Current children cumulated CPU time (s) 809.33 Current children cumulated vsize (Kb) 43700 [startup+820.077 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10001 0 0 0 81848 84 0 0 25 0 1 0 1785103568 42901504 9799 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10474 9799 145 145 0 10329 0 [pid=5572] vsize: 41896 Current children cumulated CPU time (s) 819.33 Current children cumulated vsize (Kb) 44020 [startup+830.079 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10057 0 0 0 82847 85 0 0 25 0 1 0 1785103568 43171840 9855 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10540 9855 145 145 0 10395 0 [pid=5572] vsize: 42160 Current children cumulated CPU time (s) 829.33 Current children cumulated vsize (Kb) 44284 [startup+840.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10088 0 0 0 83847 85 0 0 25 0 1 0 1785103568 43302912 9886 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10572 9886 145 145 0 10427 0 [pid=5572] vsize: 42288 Current children cumulated CPU time (s) 839.33 Current children cumulated vsize (Kb) 44412 [startup+850.081 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10119 0 0 0 84846 86 0 0 25 0 1 0 1785103568 43421696 9917 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5572/statm): 10601 9917 145 145 0 10456 0 [pid=5572] vsize: 42404 Current children cumulated CPU time (s) 849.33 Current children cumulated vsize (Kb) 44528 [startup+860.082 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10154 0 0 0 85845 86 0 0 25 0 1 0 1785103568 43560960 9952 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10635 9952 145 145 0 10490 0 [pid=5572] vsize: 42540 Current children cumulated CPU time (s) 859.32 Current children cumulated vsize (Kb) 44664 [startup+870.083 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10199 0 0 0 86844 87 0 0 25 0 1 0 1785103568 43741184 9997 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10679 9997 145 145 0 10534 0 [pid=5572] vsize: 42716 Current children cumulated CPU time (s) 869.32 Current children cumulated vsize (Kb) 44840 [startup+880.083 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10244 0 0 0 87843 87 0 0 25 0 1 0 1785103568 43917312 10042 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10722 10042 145 145 0 10577 0 [pid=5572] vsize: 42888 Current children cumulated CPU time (s) 879.31 Current children cumulated vsize (Kb) 45012 [startup+890.084 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10283 0 0 0 88842 88 0 0 25 0 1 0 1785103568 44077056 10081 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10761 10081 145 145 0 10616 0 [pid=5572] vsize: 43044 Current children cumulated CPU time (s) 889.31 Current children cumulated vsize (Kb) 45168 [startup+900.085 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10325 0 0 0 89842 88 0 0 25 0 1 0 1785103568 44244992 10123 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10802 10123 145 145 0 10657 0 [pid=5572] vsize: 43208 Current children cumulated CPU time (s) 899.31 Current children cumulated vsize (Kb) 45332 [startup+910.085 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10374 0 0 0 90841 89 0 0 25 0 1 0 1785103568 44421120 10172 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10845 10172 145 145 0 10700 0 [pid=5572] vsize: 43380 Current children cumulated CPU time (s) 909.31 Current children cumulated vsize (Kb) 45504 [startup+920.086 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10413 0 0 0 91840 89 0 0 25 0 1 0 1785103568 44576768 10211 4294967295 134512640 135094434 3221224448 3221223040 134557522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10883 10211 145 145 0 10738 0 [pid=5572] vsize: 43532 Current children cumulated CPU time (s) 919.3 Current children cumulated vsize (Kb) 45656 [startup+930.087 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10449 0 0 0 92840 89 0 0 25 0 1 0 1785103568 44728320 10247 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10920 10247 145 145 0 10775 0 [pid=5572] vsize: 43680 Current children cumulated CPU time (s) 929.3 Current children cumulated vsize (Kb) 45804 [startup+940.087 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10482 0 0 0 93839 90 0 0 25 0 1 0 1785103568 44859392 10280 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10952 10280 145 145 0 10807 0 [pid=5572] vsize: 43808 Current children cumulated CPU time (s) 939.3 Current children cumulated vsize (Kb) 45932 [startup+950.089 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10519 0 0 0 94839 91 0 0 25 0 1 0 1785103568 45006848 10317 4294967295 134512640 135094434 3221224448 3221223072 134557587 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 10988 10317 145 145 0 10843 0 [pid=5572] vsize: 43952 Current children cumulated CPU time (s) 949.31 Current children cumulated vsize (Kb) 46076 [startup+960.089 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10557 0 0 0 95838 91 0 0 25 0 1 0 1785103568 45158400 10355 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11025 10355 145 145 0 10880 0 [pid=5572] vsize: 44100 Current children cumulated CPU time (s) 959.3 Current children cumulated vsize (Kb) 46224 [startup+970.089 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10599 0 0 0 96838 91 0 0 25 0 1 0 1785103568 45322240 10397 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11065 10397 145 145 0 10920 0 [pid=5572] vsize: 44260 Current children cumulated CPU time (s) 969.3 Current children cumulated vsize (Kb) 46384 [startup+980.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10632 0 0 0 97837 91 0 0 25 0 1 0 1785103568 45457408 10430 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11098 10430 145 145 0 10953 0 [pid=5572] vsize: 44392 Current children cumulated CPU time (s) 979.29 Current children cumulated vsize (Kb) 46516 [startup+990.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10701 0 0 0 98836 92 0 0 25 0 1 0 1785103568 45785088 10499 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11178 10499 145 145 0 11033 0 [pid=5572] vsize: 44712 Current children cumulated CPU time (s) 989.29 Current children cumulated vsize (Kb) 46836 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10767 0 0 0 99836 93 0 0 25 0 1 0 1785103568 46067712 10565 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11247 10565 145 145 0 11102 0 [pid=5572] vsize: 44988 Current children cumulated CPU time (s) 999.3 Current children cumulated vsize (Kb) 47112 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10811 0 0 0 100835 93 0 0 25 0 1 0 1785103568 46239744 10609 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11289 10609 145 145 0 11144 0 [pid=5572] vsize: 45156 Current children cumulated CPU time (s) 1009.29 Current children cumulated vsize (Kb) 47280 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10851 0 0 0 101835 93 0 0 25 0 1 0 1785103568 46403584 10649 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11329 10649 145 145 0 11184 0 [pid=5572] vsize: 45316 Current children cumulated CPU time (s) 1019.29 Current children cumulated vsize (Kb) 47440 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10890 0 0 0 102834 94 0 0 25 0 1 0 1785103568 46559232 10688 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11367 10688 145 145 0 11222 0 [pid=5572] vsize: 45468 Current children cumulated CPU time (s) 1029.29 Current children cumulated vsize (Kb) 47592 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10932 0 0 0 103833 95 0 0 25 0 1 0 1785103568 46731264 10730 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11409 10730 145 145 0 11264 0 [pid=5572] vsize: 45636 Current children cumulated CPU time (s) 1039.29 Current children cumulated vsize (Kb) 47760 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10976 0 0 0 104832 95 0 0 25 0 1 0 1785103568 46915584 10774 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11454 10774 145 145 0 11309 0 [pid=5572] vsize: 45816 Current children cumulated CPU time (s) 1049.28 Current children cumulated vsize (Kb) 47940 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11028 0 0 0 105832 95 0 0 25 0 1 0 1785103568 47165440 10826 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11515 10826 145 145 0 11370 0 [pid=5572] vsize: 46060 Current children cumulated CPU time (s) 1059.28 Current children cumulated vsize (Kb) 48184 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11061 0 0 0 106831 95 0 0 25 0 1 0 1785103568 47259648 10859 4294967295 134512640 135094434 3221224448 3221223040 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11538 10859 145 145 0 11393 0 [pid=5572] vsize: 46152 Current children cumulated CPU time (s) 1069.27 Current children cumulated vsize (Kb) 48276 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11094 0 0 0 107831 96 0 0 25 0 1 0 1785103568 47448064 10892 4294967295 134512640 135094434 3221224448 3221223120 134555953 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11584 10892 145 145 0 11439 0 [pid=5572] vsize: 46336 Current children cumulated CPU time (s) 1079.28 Current children cumulated vsize (Kb) 48460 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11134 0 0 0 108831 96 0 0 25 0 1 0 1785103568 47611904 10932 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11624 10932 145 145 0 11479 0 [pid=5572] vsize: 46496 Current children cumulated CPU time (s) 1089.28 Current children cumulated vsize (Kb) 48620 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11172 0 0 0 109830 96 0 0 25 0 1 0 1785103568 47755264 10970 4294967295 134512640 135094434 3221224448 3221223104 134558295 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11659 10970 145 145 0 11514 0 [pid=5572] vsize: 46636 Current children cumulated CPU time (s) 1099.27 Current children cumulated vsize (Kb) 48760 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11207 0 0 0 110830 96 0 0 25 0 1 0 1785103568 47898624 11005 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11694 11005 145 145 0 11549 0 [pid=5572] vsize: 46776 Current children cumulated CPU time (s) 1109.27 Current children cumulated vsize (Kb) 48900 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11245 0 0 0 111829 97 0 0 25 0 1 0 1785103568 48050176 11043 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11731 11043 145 145 0 11586 0 [pid=5572] vsize: 46924 Current children cumulated CPU time (s) 1119.27 Current children cumulated vsize (Kb) 49048 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11302 0 0 0 112829 97 0 0 25 0 1 0 1785103568 48398336 11100 4294967295 134512640 135094434 3221224448 3221223040 134556914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11816 11100 145 145 0 11671 0 [pid=5572] vsize: 47264 Current children cumulated CPU time (s) 1129.27 Current children cumulated vsize (Kb) 49388 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11332 0 0 0 113829 97 0 0 25 0 1 0 1785103568 48590848 11130 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11863 11130 145 145 0 11718 0 [pid=5572] vsize: 47452 Current children cumulated CPU time (s) 1139.27 Current children cumulated vsize (Kb) 49576 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11367 0 0 0 114829 97 0 0 25 0 1 0 1785103568 48754688 11165 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11903 11165 145 145 0 11758 0 [pid=5572] vsize: 47612 Current children cumulated CPU time (s) 1149.27 Current children cumulated vsize (Kb) 49736 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11403 0 0 0 115829 97 0 0 25 0 1 0 1785103568 48889856 11201 4294967295 134512640 135094434 3221224448 3221223040 134556894 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11936 11201 145 145 0 11791 0 [pid=5572] vsize: 47744 Current children cumulated CPU time (s) 1159.27 Current children cumulated vsize (Kb) 49868 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11439 0 0 0 116828 98 0 0 25 0 1 0 1785103568 49025024 11237 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 11969 11237 145 145 0 11824 0 [pid=5572] vsize: 47876 Current children cumulated CPU time (s) 1169.27 Current children cumulated vsize (Kb) 50000 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11477 0 0 0 117828 98 0 0 25 0 1 0 1785103568 49168384 11275 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 12004 11275 145 145 0 11859 0 [pid=5572] vsize: 48016 Current children cumulated CPU time (s) 1179.27 Current children cumulated vsize (Kb) 50140 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11519 0 0 0 118827 98 0 0 25 0 1 0 1785103568 49369088 11317 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 12053 11317 145 145 0 11908 0 [pid=5572] vsize: 48212 Current children cumulated CPU time (s) 1189.26 Current children cumulated vsize (Kb) 50336 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11557 0 0 0 119827 99 0 0 25 0 1 0 1785103568 49528832 11355 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 12092 11355 145 145 0 11947 0 [pid=5572] vsize: 48368 Current children cumulated CPU time (s) 1199.27 Current children cumulated vsize (Kb) 50492 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11593 0 0 0 120826 99 0 0 25 0 1 0 1785103568 49668096 11391 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 12126 11391 145 145 0 11981 0 [pid=5572] vsize: 48504 Current children cumulated CPU time (s) 1209.26 Current children cumulated vsize (Kb) 50628 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 5572 Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/5568/statm): 531 226 485 147 0 384 0 [pid=5568] vsize: 2124 Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11593 0 0 0 120826 99 0 0 25 0 1 0 1785103568 49668096 11391 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5572/statm): 12126 11391 145 145 0 11981 0 [pid=5572] vsize: 48504 Current children cumulated CPU time (s) 1209.26 Current children cumulated vsize (Kb) 50628 Sending SIGTERM to -5568 Sleeping 2 seconds One traced child (pid=5568) ended because it received signal 15 (SIGTERM) One traced child (pid=5572) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.13 CPU time (s): 1209.28 CPU user time (s): 1208.26 CPU system time (s): 1.01984 CPU usage (%): 99.9298 Max. virtual memory (cumulated for all children) (Kb): 50628
ERROR: no interpretation found !