Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namesubmitted/een/normalized-p0548.opb
MD5SUM422c0da7d5380a26c4dac413428db5c9
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.1
Number of variables527
Total number of constraints156
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints116
Minimum length of a constraint2
Maximum length of a constraint134

Trace number 2271

Launcher Data

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

Solver Data

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 Found solution: 52559
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 % |

Watcher Data

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

Verifier Data

ERROR: no interpretation found !