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/aloul/FPGA_SAT05/normalized-fpga40_40_sat_pb.cnf.cr.opb
MD5SUMf9a3a990ebca4aa5457d0675d3f1fe27
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.91671
Number of variables2400
Total number of constraints1720
Number of constraints which are clauses1640
Number of constraints which are cardinality constraints (but not clauses)80
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint40

Trace number 895

Launcher Data

LAUNCH ON wulflinc10 THE 2005-09-18 12:34:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2393 boxname=wulflinc10 idbench=49 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f9a3a990ebca4aa5457d0675d3f1fe27  /oldhome/oroussel/tmp/wulflinc10/normalized-fpga40_40_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-fpga40_40_sat_pb.cnf.cr.opb
IDLAUNCH: 2393
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        948020 kB
Buffers:         34052 kB
Cached:          25968 kB
SwapCached:        228 kB
Active:          54116 kB
Inactive:         8872 kB
HighTotal:      131008 kB
HighFree:       101248 kB
LowTotal:       903652 kB
LowFree:        846772 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            18112 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 12:54:47 (client local time) WITH STATUS 0 IN 1208.36 SECONDS
stats: 2393 7 1208.36 0

Solver Data

c Parsing PB file...
c Converting 1720 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  79]---> BDD-cost:   77
c ---[  78]---> BDD-cost:   77
c ---[  77]---> BDD-cost:   77
c ---[  76]---> BDD-cost:   77
c ---[  75]---> BDD-cost:   77
c ---[  74]---> BDD-cost:   77
c ---[  73]---> BDD-cost:   77
c ---[  72]---> BDD-cost:   77
c ---[  71]---> BDD-cost:   77
c ---[  70]---> BDD-cost:   77
c ---[  69]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  67]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  65]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  63]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   77
c ---[  61]---> BDD-cost:   77
c ---[  60]---> BDD-cost:   77
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   37
c ---[  38]---> BDD-cost:   37
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12920    64560 |    4306       0        0     nan |  0.000 % |
c |       100 |   12920    64560 |    4736     100    26004   260.0 |  1.149 % |
c |       252 |   12920    64560 |    5210     252    37714   149.7 |  1.150 % |
c |       477 |   12920    64560 |    5731     477    76875   161.2 |  1.149 % |
c |       814 |   12920    64560 |    6304     814   161811   198.8 |  1.149 % |
c |      1321 |   12920    64560 |    6934    1321   261531   198.0 |  1.149 % |
c |      2084 |   12920    64560 |    7628    2084   359745   172.6 |  1.149 % |
c |      3223 |   12920    64560 |    8391    3223   791517   245.6 |  1.149 % |
c |      4932 |   12920    64560 |    9230    4932  1197916   242.9 |  1.149 % |
c |      7496 |   12920    64560 |   10153    7496  2266760   302.4 |  1.150 % |
c |     11341 |   12920    64560 |   11168   11341  3377694   297.8 |  1.149 % |
c |     17108 |   12920    64560 |   12285   11438  4096533   358.2 |  1.149 % |
c |     25758 |   12920    64560 |   13514   12002  3744055   312.0 |  1.149 % |
c |     38732 |   12920    64560 |   14865   15473  2381199   153.9 |  1.149 % |
c |     58193 |   12920    64560 |   16352   17728  7855736   443.1 |  1.149 % |
c |     87385 |   12920    64560 |   17987   17936  6971394   388.7 |  1.149 % |
c |    131175 |   12920    64560 |   19785   15044  2526709   168.0 |  1.149 % |
c |    196861 |   12920    64560 |   21764   20319  9340279   459.7 |  1.149 % |
c |    295389 |   12920    64560 |   23941   18363  2895214   157.7 |  1.149 % |

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/25130/stat): 25130 (minisat+_script) R 25129 25130 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783101960 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/25130/statm): 174 3 169 147 0 27 0
[pid=25130] 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=25131
New process pid=25132
New process pid=25133
execve syscall for /bin/sed executable
One traced child (pid=25132) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=25133) exited with status: 0
One traced child (pid=25131) exited with status: 0
New process pid=25134
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-fpga40_40_sat_pb.cnf.cr.opb

[startup+10.0046 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 2798 0 2 0 948 12 0 0 25 0 1 0 1783101965 11763712 2786 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 2872 2786 145 145 0 2727 0
[pid=25134] vsize: 11488
Current children cumulated CPU time (s) 9.6
Current children cumulated vsize (Kb) 13612

[startup+20.0051 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 4298 0 2 0 1923 23 0 0 25 0 1 0 1783101965 17928192 4286 4294967295 134512640 135094434 3221224432 3221223024 134556908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 4377 4286 145 145 0 4232 0
[pid=25134] vsize: 17508
Current children cumulated CPU time (s) 19.46
Current children cumulated vsize (Kb) 19632

[startup+30.0057 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 4746 0 2 0 2916 26 0 0 25 0 1 0 1783101965 19763200 4734 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25134/statm): 4825 4734 145 145 0 4680 0
[pid=25134] vsize: 19300
Current children cumulated CPU time (s) 29.42
Current children cumulated vsize (Kb) 21424

[startup+40.0063 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6286 0 2 0 3897 34 0 0 25 0 1 0 1783101965 26062848 6274 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25134/statm): 6363 6274 145 145 0 6218 0
[pid=25134] vsize: 25452
Current children cumulated CPU time (s) 39.31
Current children cumulated vsize (Kb) 27576

[startup+50.0078 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 4891 35 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0
[pid=25134] vsize: 26636
Current children cumulated CPU time (s) 49.26
Current children cumulated vsize (Kb) 28760

[startup+60.0084 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 5891 36 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0
[pid=25134] vsize: 26636
Current children cumulated CPU time (s) 59.27
Current children cumulated vsize (Kb) 28760

[startup+70.0089 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 6891 36 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0
[pid=25134] vsize: 26636
Current children cumulated CPU time (s) 69.27
Current children cumulated vsize (Kb) 28760

[startup+80.0095 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 7891 36 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0
[pid=25134] vsize: 26636
Current children cumulated CPU time (s) 79.27
Current children cumulated vsize (Kb) 28760

[startup+90.009 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 8891 36 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0
[pid=25134] vsize: 26636
Current children cumulated CPU time (s) 89.27
Current children cumulated vsize (Kb) 28760

[startup+100.01 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6925 0 2 0 9886 39 0 0 25 0 1 0 1783101965 28700672 6913 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 7007 6913 145 145 0 6862 0
[pid=25134] vsize: 28028
Current children cumulated CPU time (s) 99.25
Current children cumulated vsize (Kb) 30152

[startup+110.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 7419 0 2 0 10878 42 0 0 25 0 1 0 1783101965 30748672 7407 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 7507 7407 145 145 0 7362 0
[pid=25134] vsize: 30028
Current children cumulated CPU time (s) 109.2
Current children cumulated vsize (Kb) 32152

[startup+120.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 7468 0 2 0 11878 42 0 0 25 0 1 0 1783101965 30953472 7456 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 7557 7456 145 145 0 7412 0
[pid=25134] vsize: 30228
Current children cumulated CPU time (s) 119.2
Current children cumulated vsize (Kb) 32352

[startup+130.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 7487 0 2 0 12878 42 0 0 25 0 1 0 1783101965 31019008 7475 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 7573 7475 145 145 0 7428 0
[pid=25134] vsize: 30292
Current children cumulated CPU time (s) 129.2
Current children cumulated vsize (Kb) 32416

[startup+140.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 7547 0 2 0 13877 42 0 0 25 0 1 0 1783101965 31322112 7535 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 7647 7535 145 145 0 7502 0
[pid=25134] vsize: 30588
Current children cumulated CPU time (s) 139.19
Current children cumulated vsize (Kb) 32712

[startup+150.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 8084 0 2 0 14869 47 0 0 25 0 1 0 1783101965 33521664 8072 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 8184 8072 145 145 0 8039 0
[pid=25134] vsize: 32736
Current children cumulated CPU time (s) 149.16
Current children cumulated vsize (Kb) 34860

[startup+160.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 8805 0 2 0 15859 51 0 0 25 0 1 0 1783101965 36511744 8793 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 8914 8793 145 145 0 8769 0
[pid=25134] vsize: 35656
Current children cumulated CPU time (s) 159.1
Current children cumulated vsize (Kb) 37780

[startup+170.014 s]
Raw data (loadavg): 1.07 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9532 0 2 0 16847 55 0 0 25 0 1 0 1783101965 39505920 9520 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9645 9520 145 145 0 9500 0
[pid=25134] vsize: 38580
Current children cumulated CPU time (s) 169.02
Current children cumulated vsize (Kb) 40704

[startup+180.014 s]
Raw data (loadavg): 1.06 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 17846 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0
[pid=25134] vsize: 38732
Current children cumulated CPU time (s) 179.02
Current children cumulated vsize (Kb) 40856

[startup+190.015 s]
Raw data (loadavg): 1.05 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 18847 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0
[pid=25134] vsize: 38732
Current children cumulated CPU time (s) 189.03
Current children cumulated vsize (Kb) 40856

[startup+200.016 s]
Raw data (loadavg): 1.04 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 19847 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0
[pid=25134] vsize: 38732
Current children cumulated CPU time (s) 199.03
Current children cumulated vsize (Kb) 40856

[startup+210.017 s]
Raw data (loadavg): 1.03 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 20847 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0
[pid=25134] vsize: 38732
Current children cumulated CPU time (s) 209.03
Current children cumulated vsize (Kb) 40856

[startup+220.017 s]
Raw data (loadavg): 1.03 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 21847 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0
[pid=25134] vsize: 38732
Current children cumulated CPU time (s) 219.03
Current children cumulated vsize (Kb) 40856

[startup+230.018 s]
Raw data (loadavg): 1.02 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 22848 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0
[pid=25134] vsize: 38732
Current children cumulated CPU time (s) 229.04
Current children cumulated vsize (Kb) 40856

[startup+240.017 s]
Raw data (loadavg): 1.02 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 23848 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0
[pid=25134] vsize: 38732
Current children cumulated CPU time (s) 239.04
Current children cumulated vsize (Kb) 40856

[startup+250.018 s]
Raw data (loadavg): 1.02 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 24848 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0
[pid=25134] vsize: 38732
Current children cumulated CPU time (s) 249.04
Current children cumulated vsize (Kb) 40856

[startup+260.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 25848 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223024 134557251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0
[pid=25134] vsize: 38732
Current children cumulated CPU time (s) 259.04
Current children cumulated vsize (Kb) 40856

[startup+270.019 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9855 0 2 0 26844 57 0 0 25 0 1 0 1783101965 40853504 9843 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 9974 9843 145 145 0 9829 0
[pid=25134] vsize: 39896
Current children cumulated CPU time (s) 269.01
Current children cumulated vsize (Kb) 42020

[startup+280.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9882 0 2 0 27844 58 0 0 25 0 1 0 1783101965 41037824 9870 4294967295 134512640 135094434 3221224432 3221223104 134555335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 10019 9870 145 145 0 9874 0
[pid=25134] vsize: 40076
Current children cumulated CPU time (s) 279.02
Current children cumulated vsize (Kb) 42200

[startup+290.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9905 0 2 0 28844 58 0 0 25 0 1 0 1783101965 41168896 9893 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 10051 9893 145 145 0 9906 0
[pid=25134] vsize: 40204
Current children cumulated CPU time (s) 289.02
Current children cumulated vsize (Kb) 42328

[startup+300.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9957 0 2 0 29844 58 0 0 25 0 1 0 1783101965 41496576 9945 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 10131 9945 145 145 0 9986 0
[pid=25134] vsize: 40524
Current children cumulated CPU time (s) 299.02
Current children cumulated vsize (Kb) 42648

[startup+310.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9960 0 2 0 30844 58 0 0 25 0 1 0 1783101965 41496576 9948 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25134/statm): 10131 9948 145 145 0 9986 0
[pid=25134] vsize: 40524
Current children cumulated CPU time (s) 309.02
Current children cumulated vsize (Kb) 42648

[startup+320.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 31829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 318.94
Current children cumulated vsize (Kb) 46940

[startup+330.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 32829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 328.94
Current children cumulated vsize (Kb) 46940

[startup+340.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 33829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 338.94
Current children cumulated vsize (Kb) 46940

[startup+350.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 34829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 348.94
Current children cumulated vsize (Kb) 46940

[startup+360.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 35829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 358.94
Current children cumulated vsize (Kb) 46940

[startup+370.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 36830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 368.95
Current children cumulated vsize (Kb) 46940

[startup+380.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 37830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558129 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 378.95
Current children cumulated vsize (Kb) 46940

[startup+390.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 38830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 388.95
Current children cumulated vsize (Kb) 46940

[startup+400.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 39830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 398.95
Current children cumulated vsize (Kb) 46940

[startup+410.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 40830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223024 134556982 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 408.95
Current children cumulated vsize (Kb) 46940

[startup+420.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 41831 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 418.96
Current children cumulated vsize (Kb) 46940

[startup+430.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 42831 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 428.96
Current children cumulated vsize (Kb) 46940

[startup+440.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 43831 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 438.96
Current children cumulated vsize (Kb) 46940

[startup+450.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 44831 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 448.96
Current children cumulated vsize (Kb) 46940

[startup+460.026 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 45832 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0
[pid=25134] vsize: 44816
Current children cumulated CPU time (s) 458.97
Current children cumulated vsize (Kb) 46940

[startup+470.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 12399 0 2 0 46810 75 0 0 25 0 1 0 1783101965 51486720 12387 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25134/statm): 12570 12387 145 145 0 12425 0
[pid=25134] vsize: 50280
Current children cumulated CPU time (s) 468.85
Current children cumulated vsize (Kb) 52404

[startup+480.026 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13669 0 2 0 47789 85 0 0 25 0 1 0 1783101965 56692736 13657 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 13841 13657 145 145 0 13696 0
[pid=25134] vsize: 55364
Current children cumulated CPU time (s) 478.74
Current children cumulated vsize (Kb) 57488

[startup+490.027 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13714 0 2 0 48788 85 0 0 25 0 1 0 1783101965 56877056 13702 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 13886 13702 145 145 0 13741 0
[pid=25134] vsize: 55544
Current children cumulated CPU time (s) 488.73
Current children cumulated vsize (Kb) 57668

[startup+500.028 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13714 0 2 0 49789 85 0 0 25 0 1 0 1783101965 56877056 13702 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 13886 13702 145 145 0 13741 0
[pid=25134] vsize: 55544
Current children cumulated CPU time (s) 498.74
Current children cumulated vsize (Kb) 57668

[startup+510.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13714 0 2 0 50789 85 0 0 25 0 1 0 1783101965 56877056 13702 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 13886 13702 145 145 0 13741 0
[pid=25134] vsize: 55544
Current children cumulated CPU time (s) 508.74
Current children cumulated vsize (Kb) 57668

[startup+520.028 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13714 0 2 0 51789 85 0 0 25 0 1 0 1783101965 56877056 13702 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 13886 13702 145 145 0 13741 0
[pid=25134] vsize: 55544
Current children cumulated CPU time (s) 518.74
Current children cumulated vsize (Kb) 57668

[startup+530.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13986 0 2 0 52786 86 0 0 25 0 1 0 1783101965 57991168 13974 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14158 13974 145 145 0 14013 0
[pid=25134] vsize: 56632
Current children cumulated CPU time (s) 528.72
Current children cumulated vsize (Kb) 58756

[startup+540.028 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14196 0 2 0 53783 88 0 0 25 0 1 0 1783101965 58855424 14184 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14369 14184 145 145 0 14224 0
[pid=25134] vsize: 57476
Current children cumulated CPU time (s) 538.71
Current children cumulated vsize (Kb) 59600

[startup+550.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14197 0 2 0 54783 88 0 0 25 0 1 0 1783101965 58855424 14185 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14369 14185 145 145 0 14224 0
[pid=25134] vsize: 57476
Current children cumulated CPU time (s) 548.71
Current children cumulated vsize (Kb) 59600

[startup+560.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14197 0 2 0 55784 88 0 0 25 0 1 0 1783101965 58855424 14185 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14369 14185 145 145 0 14224 0
[pid=25134] vsize: 57476
Current children cumulated CPU time (s) 558.72
Current children cumulated vsize (Kb) 59600

[startup+570.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14197 0 2 0 56784 88 0 0 25 0 1 0 1783101965 58855424 14185 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14369 14185 145 145 0 14224 0
[pid=25134] vsize: 57476
Current children cumulated CPU time (s) 568.72
Current children cumulated vsize (Kb) 59600

[startup+580.031 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 57784 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0
[pid=25134] vsize: 57476
Current children cumulated CPU time (s) 578.72
Current children cumulated vsize (Kb) 59600

[startup+590.031 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 58784 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0
[pid=25134] vsize: 57476
Current children cumulated CPU time (s) 588.72
Current children cumulated vsize (Kb) 59600

[startup+600.032 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 59784 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0
[pid=25134] vsize: 57476
Current children cumulated CPU time (s) 598.72
Current children cumulated vsize (Kb) 59600

[startup+610.032 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 60785 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223076 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0
[pid=25134] vsize: 57476
Current children cumulated CPU time (s) 608.73
Current children cumulated vsize (Kb) 59600

[startup+620.033 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 61785 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0
[pid=25134] vsize: 57476
Current children cumulated CPU time (s) 618.73
Current children cumulated vsize (Kb) 59600

[startup+630.033 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14329 0 2 0 62783 88 0 0 25 0 1 0 1783101965 59392000 14317 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14500 14317 145 145 0 14355 0
[pid=25134] vsize: 58000
Current children cumulated CPU time (s) 628.71
Current children cumulated vsize (Kb) 60124

[startup+640.034 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 63783 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0
[pid=25134] vsize: 58164
Current children cumulated CPU time (s) 638.72
Current children cumulated vsize (Kb) 60288

[startup+650.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 64783 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0
[pid=25134] vsize: 58164
Current children cumulated CPU time (s) 648.72
Current children cumulated vsize (Kb) 60288

[startup+660.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 65784 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0
[pid=25134] vsize: 58164
Current children cumulated CPU time (s) 658.73
Current children cumulated vsize (Kb) 60288

[startup+670.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 66784 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0
[pid=25134] vsize: 58164
Current children cumulated CPU time (s) 668.73
Current children cumulated vsize (Kb) 60288

[startup+680.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 67784 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0
[pid=25134] vsize: 58164
Current children cumulated CPU time (s) 678.73
Current children cumulated vsize (Kb) 60288

[startup+690.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 68782 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 688.72
Current children cumulated vsize (Kb) 60768

[startup+700.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 69782 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 698.72
Current children cumulated vsize (Kb) 60768

[startup+710.037 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 70783 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 708.73
Current children cumulated vsize (Kb) 60768

[startup+720.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 71783 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 718.73
Current children cumulated vsize (Kb) 60768

[startup+730.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 72783 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 728.73
Current children cumulated vsize (Kb) 60768

[startup+740.039 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 73783 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 738.73
Current children cumulated vsize (Kb) 60768

[startup+750.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 74784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 748.74
Current children cumulated vsize (Kb) 60768

[startup+760.041 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 75784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223024 134557111 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 758.74
Current children cumulated vsize (Kb) 60768

[startup+770.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 76784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223080 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 768.74
Current children cumulated vsize (Kb) 60768

[startup+780.041 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 77784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 778.74
Current children cumulated vsize (Kb) 60768

[startup+790.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 78784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 788.74
Current children cumulated vsize (Kb) 60768

[startup+800.041 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 79785 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 798.75
Current children cumulated vsize (Kb) 60768

[startup+810.042 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 80785 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 808.75
Current children cumulated vsize (Kb) 60768

[startup+820.042 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 81785 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 818.75
Current children cumulated vsize (Kb) 60768

[startup+830.043 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 82785 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 828.75
Current children cumulated vsize (Kb) 60768

[startup+840.043 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 83786 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 838.76
Current children cumulated vsize (Kb) 60768

[startup+850.045 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 84786 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 848.76
Current children cumulated vsize (Kb) 60768

[startup+860.045 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 85786 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 858.76
Current children cumulated vsize (Kb) 60768

[startup+870.046 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 86786 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 868.76
Current children cumulated vsize (Kb) 60768

[startup+880.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 87787 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 878.77
Current children cumulated vsize (Kb) 60768

[startup+890.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 88787 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 888.77
Current children cumulated vsize (Kb) 60768

[startup+900.049 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 89787 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 898.77
Current children cumulated vsize (Kb) 60768

[startup+910.049 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 90788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 908.78
Current children cumulated vsize (Kb) 60768

[startup+920.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 91788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 918.78
Current children cumulated vsize (Kb) 60768

[startup+930.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 92788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 928.78
Current children cumulated vsize (Kb) 60768

[startup+940.051 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 93788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 938.78
Current children cumulated vsize (Kb) 60768

[startup+950.052 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 94788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 948.78
Current children cumulated vsize (Kb) 60768

[startup+960.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 95789 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 958.79
Current children cumulated vsize (Kb) 60768

[startup+970.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 96789 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 968.79
Current children cumulated vsize (Kb) 60768

[startup+980.053 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 97789 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 978.79
Current children cumulated vsize (Kb) 60768

[startup+990.054 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 98789 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0
[pid=25134] vsize: 58644
Current children cumulated CPU time (s) 988.79
Current children cumulated vsize (Kb) 60768

[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 15039 0 2 0 99781 94 0 0 25 0 1 0 1783101965 62304256 15027 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 15211 15027 145 145 0 15066 0
[pid=25134] vsize: 60844
Current children cumulated CPU time (s) 998.75
Current children cumulated vsize (Kb) 62968

[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 15845 0 2 0 100766 101 0 0 25 0 1 0 1783101965 65617920 15833 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 16020 15833 145 145 0 15875 0
[pid=25134] vsize: 64080
Current children cumulated CPU time (s) 1008.67
Current children cumulated vsize (Kb) 66204

[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 16533 0 2 0 101756 105 0 0 25 0 1 0 1783101965 68435968 16521 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 16708 16521 145 145 0 16563 0
[pid=25134] vsize: 66832
Current children cumulated CPU time (s) 1018.61
Current children cumulated vsize (Kb) 68956

[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17016 0 2 0 102748 108 0 0 25 0 1 0 1783101965 70447104 17004 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17199 17004 145 145 0 17054 0
[pid=25134] vsize: 68796
Current children cumulated CPU time (s) 1028.56
Current children cumulated vsize (Kb) 70920

[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17273 0 2 0 103744 110 0 0 25 0 1 0 1783101965 71491584 17261 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17261 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1038.54
Current children cumulated vsize (Kb) 71940

[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17274 0 2 0 104744 110 0 0 25 0 1 0 1783101965 71491584 17262 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17262 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1048.54
Current children cumulated vsize (Kb) 71940

[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 105745 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1058.55
Current children cumulated vsize (Kb) 71940

[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 106745 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1068.55
Current children cumulated vsize (Kb) 71940

[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 107745 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1078.55
Current children cumulated vsize (Kb) 71940

[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 108745 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1088.55
Current children cumulated vsize (Kb) 71940

[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 109746 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1098.56
Current children cumulated vsize (Kb) 71940

[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 110746 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1108.56
Current children cumulated vsize (Kb) 71940

[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17278 0 2 0 111746 110 0 0 25 0 1 0 1783101965 71491584 17266 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17266 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1118.56
Current children cumulated vsize (Kb) 71940

[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17278 0 2 0 112746 110 0 0 25 0 1 0 1783101965 71491584 17266 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17266 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1128.56
Current children cumulated vsize (Kb) 71940

[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17278 0 2 0 113747 110 0 0 25 0 1 0 1783101965 71491584 17266 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17266 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1138.57
Current children cumulated vsize (Kb) 71940

[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17278 0 2 0 114747 110 0 0 25 0 1 0 1783101965 71491584 17266 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17454 17266 145 145 0 17309 0
[pid=25134] vsize: 69816
Current children cumulated CPU time (s) 1148.57
Current children cumulated vsize (Kb) 71940

[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17641 0 2 0 115741 113 0 0 25 0 1 0 1783101965 72990720 17629 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 17820 17629 145 145 0 17675 0
[pid=25134] vsize: 71280
Current children cumulated CPU time (s) 1158.54
Current children cumulated vsize (Kb) 73404

[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 18098 0 2 0 116733 116 0 0 25 0 1 0 1783101965 74866688 18086 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 18278 18086 145 145 0 18133 0
[pid=25134] vsize: 73112
Current children cumulated CPU time (s) 1168.49
Current children cumulated vsize (Kb) 75236

[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 1.00 1/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) T 25130 25130 22582 0 -1 0 18729 0 2 0 117723 121 0 0 25 0 1 0 1783101965 77443072 18717 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/25134/statm): 18907 18717 145 145 0 18762 0
[pid=25134] vsize: 75628
Current children cumulated CPU time (s) 1178.44
Current children cumulated vsize (Kb) 77752

[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 19121 0 2 0 118718 123 0 0 25 0 1 0 1783101965 79077376 19109 4294967295 134512640 135094434 3221224432 3221223024 134556779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 19306 19109 145 145 0 19161 0
[pid=25134] vsize: 77224
Current children cumulated CPU time (s) 1188.41
Current children cumulated vsize (Kb) 79348

[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 19567 0 2 0 119710 127 0 0 25 0 1 0 1783101965 80900096 19555 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 19751 19555 145 145 0 19606 0
[pid=25134] vsize: 79004
Current children cumulated CPU time (s) 1198.37
Current children cumulated vsize (Kb) 81128

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 20125 0 2 0 120701 130 0 0 25 0 1 0 1783101965 83206144 20113 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 20314 20113 145 145 0 20169 0
[pid=25134] vsize: 81256
Current children cumulated CPU time (s) 1208.31
Current children cumulated vsize (Kb) 83380



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 1.00 2/57 25134
Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25130/statm): 531 226 485 147 0 384 0
[pid=25130] vsize: 2124
Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 20125 0 2 0 120701 130 0 0 25 0 1 0 1783101965 83206144 20113 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25134/statm): 20314 20113 145 145 0 20169 0
[pid=25134] vsize: 81256
Current children cumulated CPU time (s) 1208.31
Current children cumulated vsize (Kb) 83380

Sending SIGTERM to -25130
Sleeping 2 seconds
One traced child (pid=25130) ended because it received signal 15 (SIGTERM)
One traced child (pid=25134) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.11
CPU time (s): 1208.36
CPU user time (s): 1207.01
CPU system time (s): 1.3448
CPU usage (%): 99.8555
Max. virtual memory (cumulated for all children) (Kb): 83380

Verifier Data

ERROR: no interpretation found !