Name | submitted/een/normalized-p0548.opb |
MD5SUM | 422c0da7d5380a26c4dac413428db5c9 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 18745 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 416 |
Biggest coefficient in the objective function | 11000 |
Number of bits for the biggest coefficient in the objective function | 14 |
Sum of the numbers in the objective function | 96797 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 11000 |
Number of bits of the biggest number in a constraint | 14 |
Biggest sum of numbers in a constraint | 96797 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.1 |
Number of variables | 527 |
Total number of constraints | 156 |
Number of constraints which are clauses | 40 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 116 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 134 |
LAUNCH ON wulflinc27 THE 2005-09-18 18:28:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2630 boxname=wulflinc27 idbench=286 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 422c0da7d5380a26c4dac413428db5c9 /oldhome/oroussel/tmp/wulflinc27/normalized-p0548.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-p0548.opb IDLAUNCH: 2630 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 911340 kB Buffers: 35992 kB Cached: 55316 kB SwapCached: 764 kB Active: 66872 kB Inactive: 27012 kB HighTotal: 131008 kB HighFree: 73080 kB LowTotal: 903652 kB LowFree: 838260 kB SwapTotal: 2097892 kB SwapFree: 2096616 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5724 kB Slab: 23888 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:48:19 (client local time) WITH STATUS 10 IN 1209.57 SECONDS stats: 2630 7 1209.57 10
c Parsing PB file... c Converting 156 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................ss.ssssss.s.s. c ---[ 125]---> BDD-cost: 3 c ---[ 124]---> BDD-cost: 3 c ---[ 123]---> BDD-cost: 3 c ---[ 122]---> BDD-cost: 3 c ---[ 121]---> BDD-cost: 3 c ---[ 120]---> BDD-cost: 3 c ---[ 119]---> BDD-cost: 3 c ---[ 118]---> BDD-cost: 3 c ---[ 117]---> BDD-cost: 3 c ---[ 116]---> BDD-cost: 3 c ---[ 115]---> BDD-cost: 3 c ---[ 114]---> BDD-cost: 3 c ---[ 113]---> BDD-cost: 3 c ---[ 112]---> BDD-cost: 3 c ---[ 111]---> BDD-cost: 3 c ---[ 110]---> BDD-cost: 3 c ---[ 109]---> BDD-cost: 3 c ---[ 108]---> BDD-cost: 3 c ---[ 107]---> BDD-cost: 3 c ---[ 106]---> BDD-cost: 3 c ---[ 105]---> BDD-cost: 3 c ---[ 104]---> BDD-cost: 3 c ---[ 103]---> BDD-cost: 5 c ---[ 102]---> BDD-cost: 8 c ---[ 101]---> BDD-cost: 6 c ---[ 100]---> BDD-cost: 8 c ---[ 99]---> BDD-cost: 6 c ---[ 98]---> BDD-cost: 7 c ---[ 96]---> BDD-cost: 19 c ---[ 93]---> BDD-cost: 8 c ---[ 92]---> BDD-cost: 15 c ---[ 91]---> BDD-cost: 15 c ---[ 90]---> BDD-cost: 4 c ---[ 89]---> BDD-cost: 24 c ---[ 88]---> BDD-cost: 14 c ---[ 87]---> BDD-cost: 12 c ---[ 86]---> BDD-cost: 28 c ---[ 85]---> BDD-cost: 13 c ---[ 83]---> BDD-cost: 7 c ---[ 82]---> BDD-cost: 14 c ---[ 81]---> BDD-cost: 9 c ---[ 80]---> BDD-cost: 25 c ---[ 76]---> BDD-cost: 32 c ---[ 75]---> BDD-cost: 10 c ---[ 74]---> BDD-cost: 19 c ---[ 72]---> BDD-cost: 24 c ---[ 70]---> BDD-cost: 23 c ---[ 69]---> BDD-cost: 8 c ---[ 68]---> BDD-cost: 27 c ---[ 67]---> BDD-cost: 9 c ---[ 66]---> BDD-cost: 11 c ---[ 65]---> BDD-cost: 56 c ---[ 64]---> BDD-cost: 50 c ---[ 63]---> BDD-cost: 20 c ---[ 61]---> BDD-cost: 33 c ---[ 60]---> BDD-cost: 12 c ---[ 58]---> BDD-cost: 9 c ---[ 57]---> BDD-cost: 34 c ---[ 56]---> BDD-cost: 33 c ---[ 55]---> BDD-cost: 23 c ---[ 54]---> BDD-cost: 75 c ---[ 53]---> BDD-cost: 24 c ---[ 52]---> BDD-cost: 37 c ---[ 51]---> BDD-cost: 37 c ---[ 50]---> BDD-cost: 95 c ---[ 49]---> BDD-cost: 11 c ---[ 48]---> BDD-cost: 107 c ---[ 47]---> BDD-cost: 115 c ---[ 46]---> BDD-cost: 120 c ---[ 45]---> BDD-cost: 104 c ---[ 44]---> BDD-cost: 29 c ---[ 43]---> BDD-cost: 51 c ---[ 42]---> BDD-cost: 35 c ---[ 41]---> BDD-cost: 24 c ---[ 39]---> BDD-cost: 61 c ---[ 38]---> BDD-cost: 109 c ---[ 37]---> BDD-cost: 153 c ---[ 36]---> BDD-cost: 120 c ---[ 35]---> BDD-cost: 13 c ---[ 34]---> BDD-cost: 25 c ---[ 33]---> BDD-cost: 121 c ---[ 32]---> BDD-cost: 32 c ---[ 31]---> BDD-cost: 70 c ---[ 30]---> BDD-cost: 56 c ---[ 29]---> BDD-cost: 78 c ---[ 28]---> BDD-cost: 84 c ---[ 27]---> BDD-cost: 36 c ---[ 26]---> BDD-cost: 91 c ---[ 25]---> BDD-cost: 42 c ---[ 23]---> BDD-cost: 39 c ---[ 22]---> BDD-cost: 128 c ---[ 21]---> BDD-cost: 61 c ---[ 19]---> BDD-cost: 85 c ---[ 18]---> BDD-cost: 55 c ---[ 17]---> BDD-cost: 79 c ---[ 16]---> Sorter-cost: 1212 Base: 2 3 2 3 c ---[ 15]---> BDD-cost: 26 c ---[ 14]---> Adder-cost: 171 maxlim: 103 bits: 8/7 c ---[ 13]---> Adder-cost: 190 maxlim: 736 bits: 10/10 c ---[ 12]---> BDD-cost: 49 c ---[ 11]---> BDD-cost: 49 c ---[ 10]---> Adder-cost: 750 maxlim: 2650 bits: 13/12 c ---[ 9]---> BDD-cost: 2 c ---[ 8]---> BDD-cost: 2 c ---[ 7]---> BDD-cost: 9 c ---[ 6]---> BDD-cost: 2 c ---[ 5]---> BDD-cost: 4 c ---[ 4]---> BDD-cost: 7 c ---[ 3]---> BDD-cost: 5 c ---[ 2]---> BDD-cost: 11 c ---[ 1]---> BDD-cost: 9 c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 19074 57624 | 6358 0 0 nan | 0.000 % | c | 100 | 19074 57624 | 6993 100 383 3.8 | 2.252 % | c | 250 | 19050 57540 | 7693 243 1471 6.1 | 2.288 % | c | 475 | 19050 57540 | 8462 468 4052 8.7 | 2.288 % | c | 812 | 19011 57410 | 9308 799 7772 9.7 | 2.361 % | c | 1321 | 19011 57410 | 10239 1308 21339 16.3 | 2.361 % | c | 2080 | 19011 57410 | 11263 2067 39807 19.3 | 2.361 % | c | 3219 | 19002 57379 | 12389 3203 61387 19.2 | 2.379 % | c | 4929 | 18969 57279 | 13628 4905 111590 22.8 | 2.434 % | c | 7491 | 18952 57224 | 14991 7466 185570 24.9 | 2.470 % | c | 11335 | 18952 57224 | 16491 11310 302929 26.8 | 2.470 % | c | 17101 | 18905 57066 | 18140 8619 230651 26.8 | 2.579 % | c | 25754 | 18905 57066 | 19954 17272 547223 31.7 | 2.579 % | c | 38729 | 18877 56968 | 21949 20002 728606 36.4 | 2.633 % | c | 58190 | 18855 56892 | 24144 17072 501826 29.4 | 2.688 % | c | 87383 | 18855 56892 | 26558 21476 1433413 66.7 | 2.688 % | c ============================================================================== c [1mFound solution: 52559[0m c ---[ 0]---> Adder-cost: 2954 maxlim: 44238 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115060 | 39469 130542 | 13156 21856 1211248 55.4 | 2.688 % | c | 115160 | 39469 130542 | 14471 11028 574450 52.1 | 1.865 % | c | 115310 | 39469 130542 | 15918 11178 576227 51.6 | 1.865 % | c | 115535 | 39469 130542 | 17510 11403 580967 50.9 | 1.865 % | c | 115872 | 39469 130542 | 19261 11740 589305 50.2 | 1.865 % | c | 116378 | 39469 130542 | 21187 12246 599863 49.0 | 1.865 % | c | 117137 | 39469 130542 | 23306 13005 616416 47.4 | 1.865 % | c | 118277 | 39469 130542 | 25637 14145 652577 46.1 | 1.865 % | c | 119985 | 39469 130542 | 28201 15853 698827 44.1 | 1.865 % | c | 122547 | 39469 130542 | 31021 18415 771171 41.9 | 1.865 % | c | 126392 | 39469 130542 | 34123 22260 874497 39.3 | 1.865 % | c | 132160 | 39469 130542 | 37535 28028 1200711 42.8 | 1.865 % | c | 140809 | 39469 130542 | 41289 36677 1563685 42.6 | 1.865 % | c | 153784 | 39469 130542 | 45418 21376 978593 45.8 | 1.865 % | c | 173246 | 39469 130542 | 49959 40838 1783298 43.7 | 1.865 % | c | 202439 | 39469 130542 | 54955 34214 1463768 42.8 | 1.865 % | c | 246229 | 39469 130542 | 60451 37728 1678400 44.5 | 1.865 % | c | 311913 | 39469 130542 | 66496 56527 2405637 42.6 | 1.865 % | c | 410440 | 39469 130542 | 73146 55718 2558579 45.9 | 1.865 % | c | 558229 | 39469 130542 | 80460 33120 1706066 51.5 | 1.865 % |
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/9568/stat): 9568 (minisat+_script) R 9567 9568 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843399094 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/9568/statm): 174 3 169 147 0 27 0 [pid=9568] 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=9569 New process pid=9570 New process pid=9571 One traced child (pid=9570) exited with status: 0 execve syscall for /bin/sed executable 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=9571) exited with status: 0 One traced child (pid=9569) exited with status: 0 New process pid=9572 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-p0548.opb [startup+10.0035 s] Raw data (loadavg): 0.93 0.95 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 1399 0 0 0 979 6 0 0 25 0 1 0 1843399099 6070272 1347 4294967295 134512640 135094434 3221224448 3221223104 134558141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9572/statm): 1482 1347 145 145 0 1337 0 [pid=9572] vsize: 5928 Current children cumulated CPU time (s) 9.86 Current children cumulated vsize (Kb) 8052 [startup+20.0053 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 1668 0 0 0 1976 7 0 0 25 0 1 0 1843399099 7159808 1616 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 1748 1616 145 145 0 1603 0 [pid=9572] vsize: 6992 Current children cumulated CPU time (s) 19.84 Current children cumulated vsize (Kb) 9116 [startup+30.0061 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 1861 0 0 0 2973 8 0 0 25 0 1 0 1843399099 7942144 1809 4294967295 134512640 135094434 3221224448 3221223040 134551457 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 1939 1809 145 145 0 1794 0 [pid=9572] vsize: 7756 Current children cumulated CPU time (s) 29.82 Current children cumulated vsize (Kb) 9880 [startup+40.007 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 1986 0 0 0 3971 9 0 0 25 0 1 0 1843399099 8445952 1934 4294967295 134512640 135094434 3221224448 3221223120 134555585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 2062 1934 145 145 0 1917 0 [pid=9572] vsize: 8248 Current children cumulated CPU time (s) 39.81 Current children cumulated vsize (Kb) 10372 [startup+50.0088 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 2371 0 0 0 4963 13 0 0 25 0 1 0 1843399099 10027008 2319 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 2448 2319 145 145 0 2303 0 [pid=9572] vsize: 9792 Current children cumulated CPU time (s) 49.77 Current children cumulated vsize (Kb) 11916 [startup+60.0096 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 2468 0 0 0 5961 14 0 0 25 0 1 0 1843399099 10416128 2416 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 2543 2416 145 145 0 2398 0 [pid=9572] vsize: 10172 Current children cumulated CPU time (s) 59.76 Current children cumulated vsize (Kb) 12296 [startup+70.0114 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 2851 0 0 0 6954 18 0 0 25 0 1 0 1843399099 11988992 2799 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 2927 2799 145 145 0 2782 0 [pid=9572] vsize: 11708 Current children cumulated CPU time (s) 69.73 Current children cumulated vsize (Kb) 13832 [startup+80.0122 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 2855 0 0 0 7954 18 0 0 25 0 1 0 1843399099 12005376 2803 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 2931 2803 145 145 0 2786 0 [pid=9572] vsize: 11724 Current children cumulated CPU time (s) 79.73 Current children cumulated vsize (Kb) 13848 [startup+90.0131 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 4195 0 0 0 8950 21 0 0 25 0 1 0 1843399099 16896000 3847 4294967295 134512640 135094434 3221224448 3221223104 134558026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 4125 3847 145 145 0 3980 0 [pid=9572] vsize: 16500 Current children cumulated CPU time (s) 89.72 Current children cumulated vsize (Kb) 18624 [startup+100.014 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 4201 0 0 0 9950 21 0 0 25 0 1 0 1843399099 16912384 3853 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 4129 3853 145 145 0 3984 0 [pid=9572] vsize: 16516 Current children cumulated CPU time (s) 99.72 Current children cumulated vsize (Kb) 18640 [startup+110.015 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 4729 0 0 0 10942 24 0 0 25 0 1 0 1843399099 19165184 4381 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 4679 4381 145 145 0 4534 0 [pid=9572] vsize: 18716 Current children cumulated CPU time (s) 109.67 Current children cumulated vsize (Kb) 20840 [startup+120.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 4950 0 0 0 11938 26 0 0 25 0 1 0 1843399099 20054016 4602 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 4896 4602 145 145 0 4751 0 [pid=9572] vsize: 19584 Current children cumulated CPU time (s) 119.65 Current children cumulated vsize (Kb) 21708 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 4950 0 0 0 12938 26 0 0 25 0 1 0 1843399099 20054016 4602 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 4896 4602 145 145 0 4751 0 [pid=9572] vsize: 19584 Current children cumulated CPU time (s) 129.65 Current children cumulated vsize (Kb) 21708 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 4967 0 0 0 13938 26 0 0 25 0 1 0 1843399099 20135936 4619 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 4916 4619 145 145 0 4771 0 [pid=9572] vsize: 19664 Current children cumulated CPU time (s) 139.65 Current children cumulated vsize (Kb) 21788 [startup+150.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5253 0 0 0 14933 29 0 0 25 0 1 0 1843399099 21315584 4905 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5204 4905 145 145 0 5059 0 [pid=9572] vsize: 20816 Current children cumulated CPU time (s) 149.63 Current children cumulated vsize (Kb) 22940 [startup+160.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5479 0 0 0 15929 31 0 0 25 0 1 0 1843399099 22233088 5131 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5428 5131 145 145 0 5283 0 [pid=9572] vsize: 21712 Current children cumulated CPU time (s) 159.61 Current children cumulated vsize (Kb) 23836 [startup+170.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5479 0 0 0 16929 31 0 0 25 0 1 0 1843399099 22233088 5131 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5428 5131 145 145 0 5283 0 [pid=9572] vsize: 21712 Current children cumulated CPU time (s) 169.61 Current children cumulated vsize (Kb) 23836 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5508 0 0 0 17929 31 0 0 25 0 1 0 1843399099 22364160 5160 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5460 5160 145 145 0 5315 0 [pid=9572] vsize: 21840 Current children cumulated CPU time (s) 179.61 Current children cumulated vsize (Kb) 23964 [startup+190.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5508 0 0 0 18929 31 0 0 25 0 1 0 1843399099 22364160 5160 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5460 5160 145 145 0 5315 0 [pid=9572] vsize: 21840 Current children cumulated CPU time (s) 189.61 Current children cumulated vsize (Kb) 23964 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5508 0 0 0 19929 31 0 0 25 0 1 0 1843399099 22364160 5160 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5460 5160 145 145 0 5315 0 [pid=9572] vsize: 21840 Current children cumulated CPU time (s) 199.61 Current children cumulated vsize (Kb) 23964 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5537 0 0 0 20929 32 0 0 25 0 1 0 1843399099 22495232 5189 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5492 5189 145 145 0 5347 0 [pid=9572] vsize: 21968 Current children cumulated CPU time (s) 209.62 Current children cumulated vsize (Kb) 24092 [startup+220.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5656 0 0 0 21927 33 0 0 25 0 1 0 1843399099 22970368 5308 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5608 5308 145 145 0 5463 0 [pid=9572] vsize: 22432 Current children cumulated CPU time (s) 219.61 Current children cumulated vsize (Kb) 24556 [startup+230.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5662 0 0 0 22927 33 0 0 25 0 1 0 1843399099 23003136 5314 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5616 5314 145 145 0 5471 0 [pid=9572] vsize: 22464 Current children cumulated CPU time (s) 229.61 Current children cumulated vsize (Kb) 24588 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5673 0 0 0 23927 33 0 0 25 0 1 0 1843399099 23064576 5325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5631 5325 145 145 0 5486 0 [pid=9572] vsize: 22524 Current children cumulated CPU time (s) 239.61 Current children cumulated vsize (Kb) 24648 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5679 0 0 0 24928 33 0 0 25 0 1 0 1843399099 23097344 5331 4294967295 134512640 135094434 3221224448 3221223104 134557976 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5639 5331 145 145 0 5494 0 [pid=9572] vsize: 22556 Current children cumulated CPU time (s) 249.62 Current children cumulated vsize (Kb) 24680 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5691 0 0 0 25928 33 0 0 25 0 1 0 1843399099 23162880 5343 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5655 5343 145 145 0 5510 0 [pid=9572] vsize: 22620 Current children cumulated CPU time (s) 259.62 Current children cumulated vsize (Kb) 24744 [startup+270.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 5896 0 0 0 26924 35 0 0 25 0 1 0 1843399099 24002560 5548 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 5860 5548 145 145 0 5715 0 [pid=9572] vsize: 23440 Current children cumulated CPU time (s) 269.6 Current children cumulated vsize (Kb) 25564 [startup+280.03 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) T 9568 9568 28974 0 -1 0 6159 0 0 0 27919 37 0 0 25 0 1 0 1843399099 25063424 5811 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6119 5811 145 145 0 5974 0 [pid=9572] vsize: 24476 Current children cumulated CPU time (s) 279.57 Current children cumulated vsize (Kb) 26600 [startup+290.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6222 0 0 0 28918 37 0 0 25 0 1 0 1843399099 25317376 5874 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6181 5874 145 145 0 6036 0 [pid=9572] vsize: 24724 Current children cumulated CPU time (s) 289.56 Current children cumulated vsize (Kb) 26848 [startup+300.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6234 0 0 0 29918 37 0 0 25 0 1 0 1843399099 25382912 5886 4294967295 134512640 135094434 3221224448 3221223088 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6197 5886 145 145 0 6052 0 [pid=9572] vsize: 24788 Current children cumulated CPU time (s) 299.56 Current children cumulated vsize (Kb) 26912 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6234 0 0 0 30918 37 0 0 25 0 1 0 1843399099 25382912 5886 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6197 5886 145 145 0 6052 0 [pid=9572] vsize: 24788 Current children cumulated CPU time (s) 309.56 Current children cumulated vsize (Kb) 26912 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6243 0 0 0 31918 37 0 0 25 0 1 0 1843399099 25448448 5895 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6213 5895 145 145 0 6068 0 [pid=9572] vsize: 24852 Current children cumulated CPU time (s) 319.56 Current children cumulated vsize (Kb) 26976 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6264 0 0 0 32918 37 0 0 25 0 1 0 1843399099 25559040 5916 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6240 5916 145 145 0 6095 0 [pid=9572] vsize: 24960 Current children cumulated CPU time (s) 329.56 Current children cumulated vsize (Kb) 27084 [startup+340.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6264 0 0 0 33918 37 0 0 25 0 1 0 1843399099 25559040 5916 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6240 5916 145 145 0 6095 0 [pid=9572] vsize: 24960 Current children cumulated CPU time (s) 339.56 Current children cumulated vsize (Kb) 27084 [startup+350.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6287 0 0 0 34918 38 0 0 25 0 1 0 1843399099 25657344 5939 4294967295 134512640 135094434 3221224448 3221223088 134557059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6264 5939 145 145 0 6119 0 [pid=9572] vsize: 25056 Current children cumulated CPU time (s) 349.57 Current children cumulated vsize (Kb) 27180 [startup+360.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6345 0 0 0 35917 38 0 0 25 0 1 0 1843399099 25907200 5997 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6325 5997 145 145 0 6180 0 [pid=9572] vsize: 25300 Current children cumulated CPU time (s) 359.56 Current children cumulated vsize (Kb) 27424 [startup+370.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6550 0 0 0 36915 39 0 0 25 0 1 0 1843399099 27004928 6202 4294967295 134512640 135094434 3221224448 3221223040 134551448 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6593 6202 145 145 0 6448 0 [pid=9572] vsize: 26372 Current children cumulated CPU time (s) 369.55 Current children cumulated vsize (Kb) 28496 [startup+380.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6550 0 0 0 37915 39 0 0 25 0 1 0 1843399099 27004928 6202 4294967295 134512640 135094434 3221224448 3221223104 134561701 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6593 6202 145 145 0 6448 0 [pid=9572] vsize: 26372 Current children cumulated CPU time (s) 379.55 Current children cumulated vsize (Kb) 28496 [startup+390.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6550 0 0 0 38915 39 0 0 25 0 1 0 1843399099 27004928 6202 4294967295 134512640 135094434 3221224448 3221223120 134556538 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6593 6202 145 145 0 6448 0 [pid=9572] vsize: 26372 Current children cumulated CPU time (s) 389.55 Current children cumulated vsize (Kb) 28496 [startup+400.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6561 0 0 0 39915 39 0 0 25 0 1 0 1843399099 27070464 6213 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6609 6213 145 145 0 6464 0 [pid=9572] vsize: 26436 Current children cumulated CPU time (s) 399.55 Current children cumulated vsize (Kb) 28560 [startup+410.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6576 0 0 0 40915 39 0 0 25 0 1 0 1843399099 27136000 6228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6625 6228 145 145 0 6480 0 [pid=9572] vsize: 26500 Current children cumulated CPU time (s) 409.55 Current children cumulated vsize (Kb) 28624 [startup+420.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6577 0 0 0 41916 39 0 0 25 0 1 0 1843399099 27136000 6229 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6625 6229 145 145 0 6480 0 [pid=9572] vsize: 26500 Current children cumulated CPU time (s) 419.56 Current children cumulated vsize (Kb) 28624 [startup+430.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6598 0 0 0 42916 40 0 0 25 0 1 0 1843399099 27267072 6250 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6657 6250 145 145 0 6512 0 [pid=9572] vsize: 26628 Current children cumulated CPU time (s) 429.57 Current children cumulated vsize (Kb) 28752 [startup+440.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6610 0 0 0 43916 40 0 0 25 0 1 0 1843399099 27332608 6262 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6673 6262 145 145 0 6528 0 [pid=9572] vsize: 26692 Current children cumulated CPU time (s) 439.57 Current children cumulated vsize (Kb) 28816 [startup+450.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6717 0 0 0 44914 41 0 0 25 0 1 0 1843399099 27770880 6369 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6780 6369 145 145 0 6635 0 [pid=9572] vsize: 27120 Current children cumulated CPU time (s) 449.56 Current children cumulated vsize (Kb) 29244 [startup+460.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6717 0 0 0 45914 41 0 0 25 0 1 0 1843399099 27770880 6369 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6780 6369 145 145 0 6635 0 [pid=9572] vsize: 27120 Current children cumulated CPU time (s) 459.56 Current children cumulated vsize (Kb) 29244 [startup+470.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6721 0 0 0 46914 41 0 0 25 0 1 0 1843399099 27787264 6373 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6784 6373 145 145 0 6639 0 [pid=9572] vsize: 27136 Current children cumulated CPU time (s) 469.56 Current children cumulated vsize (Kb) 29260 [startup+480.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6729 0 0 0 47914 41 0 0 25 0 1 0 1843399099 27820032 6381 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6792 6381 145 145 0 6647 0 [pid=9572] vsize: 27168 Current children cumulated CPU time (s) 479.56 Current children cumulated vsize (Kb) 29292 [startup+490.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6730 0 0 0 48914 41 0 0 25 0 1 0 1843399099 27820032 6382 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6792 6382 145 145 0 6647 0 [pid=9572] vsize: 27168 Current children cumulated CPU time (s) 489.56 Current children cumulated vsize (Kb) 29292 [startup+500.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6730 0 0 0 49915 41 0 0 25 0 1 0 1843399099 27820032 6382 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6792 6382 145 145 0 6647 0 [pid=9572] vsize: 27168 Current children cumulated CPU time (s) 499.57 Current children cumulated vsize (Kb) 29292 [startup+510.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6753 0 0 0 50914 41 0 0 25 0 1 0 1843399099 27951104 6405 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9572/statm): 6824 6405 145 145 0 6679 0 [pid=9572] vsize: 27296 Current children cumulated CPU time (s) 509.56 Current children cumulated vsize (Kb) 29420 [startup+520.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 6859 0 0 0 51911 42 0 0 25 0 1 0 1843399099 28397568 6511 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 6933 6511 145 145 0 6788 0 [pid=9572] vsize: 27732 Current children cumulated CPU time (s) 519.54 Current children cumulated vsize (Kb) 29856 [startup+530.05 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) T 9568 9568 28974 0 -1 0 7115 0 0 0 52907 44 0 0 25 0 1 0 1843399099 29437952 6767 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7187 6767 145 145 0 7042 0 [pid=9572] vsize: 28748 Current children cumulated CPU time (s) 529.52 Current children cumulated vsize (Kb) 30872 [startup+540.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7225 0 0 0 53906 45 0 0 25 0 1 0 1843399099 29876224 6877 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7294 6877 145 145 0 7149 0 [pid=9572] vsize: 29176 Current children cumulated CPU time (s) 539.52 Current children cumulated vsize (Kb) 31300 [startup+550.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7235 0 0 0 54906 45 0 0 25 0 1 0 1843399099 29941760 6887 4294967295 134512640 135094434 3221224448 3221223192 134559249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7310 6887 145 145 0 7165 0 [pid=9572] vsize: 29240 Current children cumulated CPU time (s) 549.52 Current children cumulated vsize (Kb) 31364 [startup+560.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7241 0 0 0 55906 45 0 0 25 0 1 0 1843399099 29941760 6893 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7310 6893 145 145 0 7165 0 [pid=9572] vsize: 29240 Current children cumulated CPU time (s) 559.52 Current children cumulated vsize (Kb) 31364 [startup+570.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7256 0 0 0 56907 45 0 0 25 0 1 0 1843399099 30007296 6908 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7326 6908 145 145 0 7181 0 [pid=9572] vsize: 29304 Current children cumulated CPU time (s) 569.53 Current children cumulated vsize (Kb) 31428 [startup+580.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7268 0 0 0 57907 45 0 0 25 0 1 0 1843399099 30072832 6920 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7342 6920 145 145 0 7197 0 [pid=9572] vsize: 29368 Current children cumulated CPU time (s) 579.53 Current children cumulated vsize (Kb) 31492 [startup+590.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7268 0 0 0 58907 45 0 0 25 0 1 0 1843399099 30072832 6920 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7342 6920 145 145 0 7197 0 [pid=9572] vsize: 29368 Current children cumulated CPU time (s) 589.53 Current children cumulated vsize (Kb) 31492 [startup+600.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7281 0 0 0 59907 45 0 0 25 0 1 0 1843399099 30138368 6933 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7358 6933 145 145 0 7213 0 [pid=9572] vsize: 29432 Current children cumulated CPU time (s) 599.53 Current children cumulated vsize (Kb) 31556 [startup+610.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7282 0 0 0 60907 45 0 0 25 0 1 0 1843399099 30138368 6934 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7358 6934 145 145 0 7213 0 [pid=9572] vsize: 29432 Current children cumulated CPU time (s) 609.53 Current children cumulated vsize (Kb) 31556 [startup+620.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7282 0 0 0 61907 45 0 0 25 0 1 0 1843399099 30138368 6934 4294967295 134512640 135094434 3221224448 3221223040 134551457 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7358 6934 145 145 0 7213 0 [pid=9572] vsize: 29432 Current children cumulated CPU time (s) 619.53 Current children cumulated vsize (Kb) 31556 [startup+630.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7282 0 0 0 62908 45 0 0 25 0 1 0 1843399099 30138368 6934 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7358 6934 145 145 0 7213 0 [pid=9572] vsize: 29432 Current children cumulated CPU time (s) 629.54 Current children cumulated vsize (Kb) 31556 [startup+640.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7282 0 0 0 63908 45 0 0 25 0 1 0 1843399099 30138368 6934 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7358 6934 145 145 0 7213 0 [pid=9572] vsize: 29432 Current children cumulated CPU time (s) 639.54 Current children cumulated vsize (Kb) 31556 [startup+650.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7282 0 0 0 64908 45 0 0 25 0 1 0 1843399099 30138368 6934 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7358 6934 145 145 0 7213 0 [pid=9572] vsize: 29432 Current children cumulated CPU time (s) 649.54 Current children cumulated vsize (Kb) 31556 [startup+660.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7282 0 0 0 65908 45 0 0 25 0 1 0 1843399099 30138368 6934 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7358 6934 145 145 0 7213 0 [pid=9572] vsize: 29432 Current children cumulated CPU time (s) 659.54 Current children cumulated vsize (Kb) 31556 [startup+670.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7282 0 0 0 66908 46 0 0 25 0 1 0 1843399099 30138368 6934 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7358 6934 145 145 0 7213 0 [pid=9572] vsize: 29432 Current children cumulated CPU time (s) 669.55 Current children cumulated vsize (Kb) 31556 [startup+680.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7287 0 0 0 67908 46 0 0 25 0 1 0 1843399099 30171136 6939 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7366 6939 145 145 0 7221 0 [pid=9572] vsize: 29464 Current children cumulated CPU time (s) 679.55 Current children cumulated vsize (Kb) 31588 [startup+690.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7300 0 0 0 68909 46 0 0 25 0 1 0 1843399099 30236672 6952 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7382 6952 145 145 0 7237 0 [pid=9572] vsize: 29528 Current children cumulated CPU time (s) 689.56 Current children cumulated vsize (Kb) 31652 [startup+700.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7517 0 0 0 69904 48 0 0 25 0 1 0 1843399099 31121408 7169 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7598 7169 145 145 0 7453 0 [pid=9572] vsize: 30392 Current children cumulated CPU time (s) 699.53 Current children cumulated vsize (Kb) 32516 [startup+710.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 7800 0 0 0 70898 49 0 0 25 0 1 0 1843399099 32280576 7452 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 7881 7452 145 145 0 7736 0 [pid=9572] vsize: 31524 Current children cumulated CPU time (s) 709.48 Current children cumulated vsize (Kb) 33648 [startup+720.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8086 0 0 0 71894 51 0 0 25 0 1 0 1843399099 33472512 7738 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8172 7738 145 145 0 8027 0 [pid=9572] vsize: 32688 Current children cumulated CPU time (s) 719.46 Current children cumulated vsize (Kb) 34812 [startup+730.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8319 0 0 0 72891 52 0 0 25 0 1 0 1843399099 34451456 7971 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9572/statm): 8411 7971 145 145 0 8266 0 [pid=9572] vsize: 33644 Current children cumulated CPU time (s) 729.44 Current children cumulated vsize (Kb) 35768 [startup+740.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8371 0 0 0 73889 53 0 0 25 0 1 0 1843399099 34660352 8023 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8462 8023 145 145 0 8317 0 [pid=9572] vsize: 33848 Current children cumulated CPU time (s) 739.43 Current children cumulated vsize (Kb) 35972 [startup+750.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8371 0 0 0 74890 53 0 0 25 0 1 0 1843399099 34660352 8023 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8462 8023 145 145 0 8317 0 [pid=9572] vsize: 33848 Current children cumulated CPU time (s) 749.44 Current children cumulated vsize (Kb) 35972 [startup+760.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8371 0 0 0 75889 53 0 0 25 0 1 0 1843399099 34660352 8023 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8462 8023 145 145 0 8317 0 [pid=9572] vsize: 33848 Current children cumulated CPU time (s) 759.43 Current children cumulated vsize (Kb) 35972 [startup+770.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8388 0 0 0 76889 53 0 0 25 0 1 0 1843399099 34742272 8040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8482 8040 145 145 0 8337 0 [pid=9572] vsize: 33928 Current children cumulated CPU time (s) 769.43 Current children cumulated vsize (Kb) 36052 [startup+780.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8406 0 0 0 77889 53 0 0 25 0 1 0 1843399099 34824192 8058 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8502 8058 145 145 0 8357 0 [pid=9572] vsize: 34008 Current children cumulated CPU time (s) 779.43 Current children cumulated vsize (Kb) 36132 [startup+790.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8416 0 0 0 78890 53 0 0 25 0 1 0 1843399099 34873344 8068 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8514 8068 145 145 0 8369 0 [pid=9572] vsize: 34056 Current children cumulated CPU time (s) 789.44 Current children cumulated vsize (Kb) 36180 [startup+800.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8425 0 0 0 79890 53 0 0 25 0 1 0 1843399099 34922496 8077 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8526 8077 145 145 0 8381 0 [pid=9572] vsize: 34104 Current children cumulated CPU time (s) 799.44 Current children cumulated vsize (Kb) 36228 [startup+810.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8432 0 0 0 80890 53 0 0 25 0 1 0 1843399099 34938880 8084 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8530 8084 145 145 0 8385 0 [pid=9572] vsize: 34120 Current children cumulated CPU time (s) 809.44 Current children cumulated vsize (Kb) 36244 [startup+820.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8446 0 0 0 81890 54 0 0 25 0 1 0 1843399099 35004416 8098 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8546 8098 145 145 0 8401 0 [pid=9572] vsize: 34184 Current children cumulated CPU time (s) 819.45 Current children cumulated vsize (Kb) 36308 [startup+830.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8468 0 0 0 82890 54 0 0 25 0 1 0 1843399099 35086336 8120 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8566 8120 145 145 0 8421 0 [pid=9572] vsize: 34264 Current children cumulated CPU time (s) 829.45 Current children cumulated vsize (Kb) 36388 [startup+840.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8470 0 0 0 83891 54 0 0 25 0 1 0 1843399099 35086336 8122 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8566 8122 145 145 0 8421 0 [pid=9572] vsize: 34264 Current children cumulated CPU time (s) 839.46 Current children cumulated vsize (Kb) 36388 [startup+850.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8471 0 0 0 84891 54 0 0 25 0 1 0 1843399099 35086336 8123 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8566 8123 145 145 0 8421 0 [pid=9572] vsize: 34264 Current children cumulated CPU time (s) 849.46 Current children cumulated vsize (Kb) 36388 [startup+860.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8471 0 0 0 85891 54 0 0 25 0 1 0 1843399099 35086336 8123 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8566 8123 145 145 0 8421 0 [pid=9572] vsize: 34264 Current children cumulated CPU time (s) 859.46 Current children cumulated vsize (Kb) 36388 [startup+870.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8497 0 0 0 86891 54 0 0 25 0 1 0 1843399099 35217408 8149 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8598 8149 145 145 0 8453 0 [pid=9572] vsize: 34392 Current children cumulated CPU time (s) 869.46 Current children cumulated vsize (Kb) 36516 [startup+880.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8499 0 0 0 87891 54 0 0 25 0 1 0 1843399099 35217408 8151 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8598 8151 145 145 0 8453 0 [pid=9572] vsize: 34392 Current children cumulated CPU time (s) 879.46 Current children cumulated vsize (Kb) 36516 [startup+890.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8504 0 0 0 88891 54 0 0 25 0 1 0 1843399099 35348480 8156 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8630 8156 145 145 0 8485 0 [pid=9572] vsize: 34520 Current children cumulated CPU time (s) 889.46 Current children cumulated vsize (Kb) 36644 [startup+900.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8506 0 0 0 89892 54 0 0 25 0 1 0 1843399099 35348480 8158 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8630 8158 145 145 0 8485 0 [pid=9572] vsize: 34520 Current children cumulated CPU time (s) 899.47 Current children cumulated vsize (Kb) 36644 [startup+910.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8508 0 0 0 90892 54 0 0 25 0 1 0 1843399099 35348480 8160 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8630 8160 145 145 0 8485 0 [pid=9572] vsize: 34520 Current children cumulated CPU time (s) 909.47 Current children cumulated vsize (Kb) 36644 [startup+920.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8510 0 0 0 91892 54 0 0 25 0 1 0 1843399099 35348480 8162 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8630 8162 145 145 0 8485 0 [pid=9572] vsize: 34520 Current children cumulated CPU time (s) 919.47 Current children cumulated vsize (Kb) 36644 [startup+930.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8540 0 0 0 92893 54 0 0 25 0 1 0 1843399099 35414016 8192 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8646 8192 145 145 0 8501 0 [pid=9572] vsize: 34584 Current children cumulated CPU time (s) 929.48 Current children cumulated vsize (Kb) 36708 [startup+940.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8555 0 0 0 93893 54 0 0 25 0 1 0 1843399099 35545088 8207 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8207 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 939.48 Current children cumulated vsize (Kb) 36836 [startup+950.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8558 0 0 0 94893 54 0 0 25 0 1 0 1843399099 35545088 8210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8210 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 949.48 Current children cumulated vsize (Kb) 36836 [startup+960.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8559 0 0 0 95893 54 0 0 25 0 1 0 1843399099 35545088 8211 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8211 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 959.48 Current children cumulated vsize (Kb) 36836 [startup+970.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8561 0 0 0 96893 54 0 0 25 0 1 0 1843399099 35545088 8213 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8213 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 969.48 Current children cumulated vsize (Kb) 36836 [startup+980.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8567 0 0 0 97894 55 0 0 25 0 1 0 1843399099 35545088 8219 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8219 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 979.5 Current children cumulated vsize (Kb) 36836 [startup+990.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8570 0 0 0 98894 55 0 0 25 0 1 0 1843399099 35545088 8222 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8222 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 989.5 Current children cumulated vsize (Kb) 36836 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8570 0 0 0 99894 55 0 0 25 0 1 0 1843399099 35545088 8222 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8222 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 999.5 Current children cumulated vsize (Kb) 36836 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8570 0 0 0 100894 55 0 0 25 0 1 0 1843399099 35545088 8222 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8222 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 1009.5 Current children cumulated vsize (Kb) 36836 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8570 0 0 0 101894 55 0 0 25 0 1 0 1843399099 35545088 8222 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8222 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 1019.5 Current children cumulated vsize (Kb) 36836 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8570 0 0 0 102895 55 0 0 25 0 1 0 1843399099 35545088 8222 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8222 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 1029.51 Current children cumulated vsize (Kb) 36836 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8570 0 0 0 103895 55 0 0 25 0 1 0 1843399099 35545088 8222 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8222 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 1039.51 Current children cumulated vsize (Kb) 36836 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8570 0 0 0 104895 55 0 0 25 0 1 0 1843399099 35545088 8222 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8222 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 1049.51 Current children cumulated vsize (Kb) 36836 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8572 0 0 0 105895 55 0 0 25 0 1 0 1843399099 35545088 8224 4294967295 134512640 135094434 3221224448 3221223104 134558240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8678 8224 145 145 0 8533 0 [pid=9572] vsize: 34712 Current children cumulated CPU time (s) 1059.51 Current children cumulated vsize (Kb) 36836 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8582 0 0 0 106895 55 0 0 25 0 1 0 1843399099 35610624 8234 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8694 8234 145 145 0 8549 0 [pid=9572] vsize: 34776 Current children cumulated CPU time (s) 1069.51 Current children cumulated vsize (Kb) 36900 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8582 0 0 0 107896 55 0 0 25 0 1 0 1843399099 35610624 8234 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8694 8234 145 145 0 8549 0 [pid=9572] vsize: 34776 Current children cumulated CPU time (s) 1079.52 Current children cumulated vsize (Kb) 36900 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8582 0 0 0 108896 55 0 0 25 0 1 0 1843399099 35610624 8234 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8694 8234 145 145 0 8549 0 [pid=9572] vsize: 34776 Current children cumulated CPU time (s) 1089.52 Current children cumulated vsize (Kb) 36900 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8582 0 0 0 109896 55 0 0 25 0 1 0 1843399099 35610624 8234 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8694 8234 145 145 0 8549 0 [pid=9572] vsize: 34776 Current children cumulated CPU time (s) 1099.52 Current children cumulated vsize (Kb) 36900 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8607 0 0 0 110896 55 0 0 25 0 1 0 1843399099 35741696 8259 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8726 8259 145 145 0 8581 0 [pid=9572] vsize: 34904 Current children cumulated CPU time (s) 1109.52 Current children cumulated vsize (Kb) 37028 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8608 0 0 0 111896 55 0 0 25 0 1 0 1843399099 35741696 8260 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8726 8260 145 145 0 8581 0 [pid=9572] vsize: 34904 Current children cumulated CPU time (s) 1119.52 Current children cumulated vsize (Kb) 37028 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8608 0 0 0 112897 55 0 0 25 0 1 0 1843399099 35741696 8260 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8726 8260 145 145 0 8581 0 [pid=9572] vsize: 34904 Current children cumulated CPU time (s) 1129.53 Current children cumulated vsize (Kb) 37028 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8608 0 0 0 113897 55 0 0 25 0 1 0 1843399099 35741696 8260 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8726 8260 145 145 0 8581 0 [pid=9572] vsize: 34904 Current children cumulated CPU time (s) 1139.53 Current children cumulated vsize (Kb) 37028 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8609 0 0 0 114897 55 0 0 25 0 1 0 1843399099 35741696 8261 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8726 8261 145 145 0 8581 0 [pid=9572] vsize: 34904 Current children cumulated CPU time (s) 1149.53 Current children cumulated vsize (Kb) 37028 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8611 0 0 0 115897 55 0 0 25 0 1 0 1843399099 35741696 8263 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8726 8263 145 145 0 8581 0 [pid=9572] vsize: 34904 Current children cumulated CPU time (s) 1159.53 Current children cumulated vsize (Kb) 37028 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8624 0 0 0 116897 56 0 0 25 0 1 0 1843399099 35807232 8276 4294967295 134512640 135094434 3221224448 3221221004 134563353 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8742 8276 145 145 0 8597 0 [pid=9572] vsize: 34968 Current children cumulated CPU time (s) 1169.54 Current children cumulated vsize (Kb) 37092 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8624 0 0 0 117897 56 0 0 25 0 1 0 1843399099 35807232 8276 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8742 8276 145 145 0 8597 0 [pid=9572] vsize: 34968 Current children cumulated CPU time (s) 1179.54 Current children cumulated vsize (Kb) 37092 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8624 0 0 0 118898 56 0 0 25 0 1 0 1843399099 35807232 8276 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8742 8276 145 145 0 8597 0 [pid=9572] vsize: 34968 Current children cumulated CPU time (s) 1189.55 Current children cumulated vsize (Kb) 37092 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8624 0 0 0 119898 56 0 0 25 0 1 0 1843399099 35807232 8276 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8742 8276 145 145 0 8597 0 [pid=9572] vsize: 34968 Current children cumulated CPU time (s) 1199.55 Current children cumulated vsize (Kb) 37092 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8624 0 0 0 120898 56 0 0 25 0 1 0 1843399099 35807232 8276 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8742 8276 145 145 0 8597 0 [pid=9572] vsize: 34968 Current children cumulated CPU time (s) 1209.55 Current children cumulated vsize (Kb) 37092 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9572 Raw data (/proc/9568/stat): 9568 (minisat+_script) S 9567 9568 28974 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843399094 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9568/statm): 531 226 485 147 0 384 0 [pid=9568] vsize: 2124 Raw data (/proc/9572/stat): 9572 (minisat+_64-bit) R 9568 9568 28974 0 -1 0 8624 0 0 0 120898 56 0 0 25 0 1 0 1843399099 35807232 8276 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9572/statm): 8742 8276 145 145 0 8597 0 [pid=9572] vsize: 34968 Current children cumulated CPU time (s) 1209.55 Current children cumulated vsize (Kb) 37092 Sending SIGTERM to -9568 Sleeping 2 seconds One traced child (pid=9568) ended because it received signal 15 (SIGTERM) One traced child (pid=9572) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1209.57 CPU user time (s): 1208.99 CPU system time (s): 0.581911 CPU usage (%): 99.9533 Max. virtual memory (cumulated for all children) (Kb): 37092
ERROR: no interpretation found !