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/manquinho/primes-dimacs-cnf/normalized-f2000.opb
MD5SUM4675a5d50c7e04c9a0597ae768da1a88
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 4000
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 4000
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 4000
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables4000
Total number of constraints10500
Number of constraints which are clauses10500
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint3

Trace number 1461

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        693576 kB
Buffers:         35624 kB
Cached:         274324 kB
SwapCached:       1016 kB
Active:         102388 kB
Inactive:       210380 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        693324 kB
SwapTotal:     2097892 kB
SwapFree:      2096404 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5768 kB
Slab:            22580 kB
Committed_AS:    64340 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 15:29:07 (client local time) WITH STATUS 0 IN 1209.83 SECONDS
stats: 2467 7 1209.83 0

Solver Data

c Parsing PB file...
c Converting 10500 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10500    29500 |    3500       0        0     nan |  0.000 % |
c |       101 |   10500    29500 |    3850     101     5214    51.6 |  0.000 % |
c |       254 |   10500    29500 |    4235     254    16768    66.0 |  0.000 % |
c |       480 |   10500    29500 |    4658     480    31254    65.1 |  0.000 % |
c |       818 |   10500    29500 |    5124     818    54667    66.8 |  0.000 % |
c |      1325 |   10500    29500 |    5636    1325    91945    69.4 |  0.000 % |
c |      2085 |   10500    29500 |    6200    2085   147368    70.7 |  0.000 % |
c |      3224 |   10500    29500 |    6820    3224   227442    70.5 |  0.000 % |
c |      4933 |   10500    29500 |    7502    4933   356310    72.2 |  0.000 % |
c |      7498 |   10500    29500 |    8252    7498   558986    74.6 |  0.000 % |
c |     11342 |   10500    29500 |    9078    7035   532667    75.7 |  0.000 % |
c |     17110 |   10500    29500 |    9985    8082   628618    77.8 |  0.000 % |
c |     25760 |   10500    29500 |   10984    6399   501007    78.3 |  0.000 % |
c |     38734 |   10500    29500 |   12082    8099   680844    84.1 |  0.000 % |
c |     58195 |   10500    29500 |   13291    8833   695144    78.7 |  0.000 % |
c |     87387 |   10500    29500 |   14620   10633   872256    82.0 |  0.000 % |
c |    131179 |   10500    29500 |   16082    9098   714655    78.6 |  0.000 % |
c |    196863 |   10500    29500 |   17690    8808   654716    74.3 |  0.000 % |
c |    295391 |   10500    29500 |   19459   16874  1288385    76.4 |  0.000 % |
c |    443181 |   10500    29500 |   21405   15399  1144903    74.3 |  0.000 % |
c |    664864 |   10500    29500 |   23546   18740  1450858    77.4 |  0.000 % |

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/14295/stat): 14295 (minisat+_script) R 14294 14295 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842179474 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14295/statm): 174 3 169 147 0 27 0
[pid=14295] 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=14296
New process pid=14297
New process pid=14298
execve syscall for /bin/sed executable
One traced child (pid=14297) 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=14298) exited with status: 0
One traced child (pid=14296) exited with status: 0
New process pid=14299
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-f2000.opb

[startup+10.0042 s]
Raw data (loadavg): 0.59 0.86 0.94 2/58 14299
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1238 0 0 0 983 6 0 0 25 0 1 0 1842179479 5390336 1225 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 1316 1225 145 145 0 1171 0
[pid=14299] vsize: 5264
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 7388

[startup+20.0051 s]
Raw data (loadavg): 0.65 0.86 0.94 2/58 14299
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1495 0 0 0 1978 9 0 0 25 0 1 0 1842179479 6434816 1482 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 1571 1482 145 145 0 1426 0
[pid=14299] vsize: 6284
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 8408

[startup+30.0061 s]
Raw data (loadavg): 0.71 0.87 0.94 2/58 14301
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1660 0 0 0 2975 10 0 0 25 0 1 0 1842179479 7106560 1647 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 1735 1647 145 145 0 1590 0
[pid=14299] vsize: 6940
Current children cumulated CPU time (s) 29.85
Current children cumulated vsize (Kb) 9064

[startup+40.007 s]
Raw data (loadavg): 0.75 0.87 0.94 2/58 14301
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1748 0 0 0 3973 11 0 0 25 0 1 0 1842179479 7471104 1735 4294967295 134512640 135094434 3221224448 3221223088 134562095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 1824 1735 145 145 0 1679 0
[pid=14299] vsize: 7296
Current children cumulated CPU time (s) 39.84
Current children cumulated vsize (Kb) 9420

[startup+50.009 s]
Raw data (loadavg): 0.79 0.87 0.94 2/58 14301
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1835 0 0 0 4970 13 0 0 25 0 1 0 1842179479 7823360 1822 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 1910 1822 145 145 0 1765 0
[pid=14299] vsize: 7640
Current children cumulated CPU time (s) 49.83
Current children cumulated vsize (Kb) 9764

[startup+60.0109 s]
Raw data (loadavg): 0.82 0.88 0.94 2/58 14301
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1875 0 0 0 5970 13 0 0 25 0 1 0 1842179479 7995392 1862 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 1952 1862 145 145 0 1807 0
[pid=14299] vsize: 7808
Current children cumulated CPU time (s) 59.83
Current children cumulated vsize (Kb) 9932

[startup+70.0118 s]
Raw data (loadavg): 0.85 0.88 0.94 2/58 14301
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 1985 0 0 0 6967 14 0 0 25 0 1 0 1842179479 8441856 1972 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2061 1972 145 145 0 1916 0
[pid=14299] vsize: 8244
Current children cumulated CPU time (s) 69.81
Current children cumulated vsize (Kb) 10368

[startup+80.0127 s]
Raw data (loadavg): 0.87 0.89 0.94 2/58 14301
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2052 0 0 0 7965 16 0 0 25 0 1 0 1842179479 8716288 2039 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2128 2039 145 145 0 1983 0
[pid=14299] vsize: 8512
Current children cumulated CPU time (s) 79.81
Current children cumulated vsize (Kb) 10636

[startup+90.0147 s]
Raw data (loadavg): 0.89 0.89 0.94 2/58 14303
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2132 0 0 0 8962 17 0 0 25 0 1 0 1842179479 9043968 2119 4294967295 134512640 135094434 3221224448 3221223104 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2208 2119 145 145 0 2063 0
[pid=14299] vsize: 8832
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 10956

[startup+100.016 s]
Raw data (loadavg): 0.91 0.89 0.94 2/58 14303
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2145 0 0 0 9961 19 0 0 25 0 1 0 1842179479 9097216 2132 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2221 2132 145 145 0 2076 0
[pid=14299] vsize: 8884
Current children cumulated CPU time (s) 99.8
Current children cumulated vsize (Kb) 11008

[startup+110.018 s]
Raw data (loadavg): 0.92 0.89 0.94 2/58 14303
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2254 0 0 0 10958 20 0 0 25 0 1 0 1842179479 9535488 2241 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2328 2241 145 145 0 2183 0
[pid=14299] vsize: 9312
Current children cumulated CPU time (s) 109.78
Current children cumulated vsize (Kb) 11436

[startup+120.019 s]
Raw data (loadavg): 0.93 0.90 0.94 2/58 14303
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2280 0 0 0 11957 21 0 0 25 0 1 0 1842179479 9650176 2267 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2356 2267 145 145 0 2211 0
[pid=14299] vsize: 9424
Current children cumulated CPU time (s) 119.78
Current children cumulated vsize (Kb) 11548

[startup+130.02 s]
Raw data (loadavg): 0.94 0.90 0.94 2/58 14303
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2317 0 0 0 12956 22 0 0 25 0 1 0 1842179479 9801728 2304 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2393 2304 145 145 0 2248 0
[pid=14299] vsize: 9572
Current children cumulated CPU time (s) 129.78
Current children cumulated vsize (Kb) 11696

[startup+140.022 s]
Raw data (loadavg): 0.95 0.90 0.94 2/58 14303
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2317 0 0 0 13956 23 0 0 25 0 1 0 1842179479 9801728 2304 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2393 2304 145 145 0 2248 0
[pid=14299] vsize: 9572
Current children cumulated CPU time (s) 139.79
Current children cumulated vsize (Kb) 11696

[startup+150.023 s]
Raw data (loadavg): 0.96 0.91 0.94 2/58 14305
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2327 0 0 0 14955 23 0 0 25 0 1 0 1842179479 9846784 2314 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2404 2314 145 145 0 2259 0
[pid=14299] vsize: 9616
Current children cumulated CPU time (s) 149.78
Current children cumulated vsize (Kb) 11740

[startup+160.024 s]
Raw data (loadavg): 0.96 0.91 0.94 2/58 14305
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2349 0 0 0 15954 24 0 0 25 0 1 0 1842179479 9936896 2336 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2426 2336 145 145 0 2281 0
[pid=14299] vsize: 9704
Current children cumulated CPU time (s) 159.78
Current children cumulated vsize (Kb) 11828

[startup+170.025 s]
Raw data (loadavg): 0.97 0.91 0.94 2/58 14305
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2367 0 0 0 16954 25 0 0 25 0 1 0 1842179479 10010624 2354 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2444 2354 145 145 0 2299 0
[pid=14299] vsize: 9776
Current children cumulated CPU time (s) 169.79
Current children cumulated vsize (Kb) 11900

[startup+180.026 s]
Raw data (loadavg): 0.97 0.91 0.94 2/58 14305
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2481 0 0 0 17952 25 0 0 25 0 1 0 1842179479 10539008 2468 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2573 2468 145 145 0 2428 0
[pid=14299] vsize: 10292
Current children cumulated CPU time (s) 179.77
Current children cumulated vsize (Kb) 12416

[startup+190.028 s]
Raw data (loadavg): 0.98 0.92 0.94 2/58 14305
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2481 0 0 0 18952 25 0 0 25 0 1 0 1842179479 10539008 2468 4294967295 134512640 135094434 3221224448 3221223040 134557263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2573 2468 145 145 0 2428 0
[pid=14299] vsize: 10292
Current children cumulated CPU time (s) 189.77
Current children cumulated vsize (Kb) 12416

[startup+200.029 s]
Raw data (loadavg): 0.98 0.92 0.94 2/58 14305
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2486 0 0 0 19951 26 0 0 25 0 1 0 1842179479 10559488 2473 4294967295 134512640 135094434 3221224448 3221223120 134555967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2578 2473 145 145 0 2433 0
[pid=14299] vsize: 10312
Current children cumulated CPU time (s) 199.77
Current children cumulated vsize (Kb) 12436

[startup+210.031 s]
Raw data (loadavg): 0.98 0.92 0.94 2/58 14307
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2501 0 0 0 20950 27 0 0 25 0 1 0 1842179479 10620928 2488 4294967295 134512640 135094434 3221224448 3221223072 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2593 2488 145 145 0 2448 0
[pid=14299] vsize: 10372
Current children cumulated CPU time (s) 209.77
Current children cumulated vsize (Kb) 12496

[startup+220.033 s]
Raw data (loadavg): 0.98 0.92 0.94 2/58 14307
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2507 0 0 0 21950 28 0 0 25 0 1 0 1842179479 10645504 2494 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 2599 2494 145 145 0 2454 0
[pid=14299] vsize: 10396
Current children cumulated CPU time (s) 219.78
Current children cumulated vsize (Kb) 12520

[startup+230.034 s]
Raw data (loadavg): 0.99 0.92 0.94 2/58 14307
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2547 0 0 0 22949 28 0 0 25 0 1 0 1842179479 10825728 2534 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2643 2534 145 145 0 2498 0
[pid=14299] vsize: 10572
Current children cumulated CPU time (s) 229.77
Current children cumulated vsize (Kb) 12696

[startup+240.035 s]
Raw data (loadavg): 0.99 0.93 0.94 2/58 14307
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2551 0 0 0 23949 28 0 0 25 0 1 0 1842179479 10842112 2538 4294967295 134512640 135094434 3221224448 3221223104 134558240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2647 2538 145 145 0 2502 0
[pid=14299] vsize: 10588
Current children cumulated CPU time (s) 239.77
Current children cumulated vsize (Kb) 12712

[startup+250.035 s]
Raw data (loadavg): 0.99 0.93 0.94 2/58 14307
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2551 0 0 0 24949 28 0 0 25 0 1 0 1842179479 10842112 2538 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2647 2538 145 145 0 2502 0
[pid=14299] vsize: 10588
Current children cumulated CPU time (s) 249.77
Current children cumulated vsize (Kb) 12712

[startup+260.037 s]
Raw data (loadavg): 0.99 0.93 0.94 2/58 14307
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2589 0 0 0 25949 29 0 0 25 0 1 0 1842179479 10993664 2576 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2684 2576 145 145 0 2539 0
[pid=14299] vsize: 10736
Current children cumulated CPU time (s) 259.78
Current children cumulated vsize (Kb) 12860

[startup+270.038 s]
Raw data (loadavg): 0.99 0.93 0.94 2/58 14309
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2694 0 0 0 26947 29 0 0 25 0 1 0 1842179479 11415552 2681 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2787 2681 145 145 0 2642 0
[pid=14299] vsize: 11148
Current children cumulated CPU time (s) 269.76
Current children cumulated vsize (Kb) 13272

[startup+280.038 s]
Raw data (loadavg): 0.99 0.93 0.94 2/58 14309
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2694 0 0 0 27947 29 0 0 25 0 1 0 1842179479 11415552 2681 4294967295 134512640 135094434 3221224448 3221223040 134557348 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2787 2681 145 145 0 2642 0
[pid=14299] vsize: 11148
Current children cumulated CPU time (s) 279.76
Current children cumulated vsize (Kb) 13272

[startup+290.04 s]
Raw data (loadavg): 0.99 0.94 0.94 2/58 14309
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2755 0 0 0 28947 29 0 0 25 0 1 0 1842179479 11665408 2742 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2848 2742 145 145 0 2703 0
[pid=14299] vsize: 11392
Current children cumulated CPU time (s) 289.76
Current children cumulated vsize (Kb) 13516

[startup+300.041 s]
Raw data (loadavg): 0.99 0.94 0.94 2/58 14309
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2793 0 0 0 29947 30 0 0 25 0 1 0 1842179479 11829248 2780 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2888 2780 145 145 0 2743 0
[pid=14299] vsize: 11552
Current children cumulated CPU time (s) 299.77
Current children cumulated vsize (Kb) 13676

[startup+310.042 s]
Raw data (loadavg): 0.99 0.94 0.94 2/58 14309
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2806 0 0 0 30947 30 0 0 25 0 1 0 1842179479 11890688 2793 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2903 2793 145 145 0 2758 0
[pid=14299] vsize: 11612
Current children cumulated CPU time (s) 309.77
Current children cumulated vsize (Kb) 13736

[startup+320.043 s]
Raw data (loadavg): 0.99 0.94 0.94 2/58 14309
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2813 0 0 0 31947 30 0 0 25 0 1 0 1842179479 11923456 2800 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2911 2800 145 145 0 2766 0
[pid=14299] vsize: 11644
Current children cumulated CPU time (s) 319.77
Current children cumulated vsize (Kb) 13768

[startup+330.044 s]
Raw data (loadavg): 0.99 0.94 0.94 2/58 14311
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2813 0 0 0 32947 30 0 0 25 0 1 0 1842179479 11923456 2800 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2911 2800 145 145 0 2766 0
[pid=14299] vsize: 11644
Current children cumulated CPU time (s) 329.77
Current children cumulated vsize (Kb) 13768

[startup+340.045 s]
Raw data (loadavg): 0.99 0.94 0.94 2/58 14311
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2813 0 0 0 33947 30 0 0 25 0 1 0 1842179479 11923456 2800 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2911 2800 145 145 0 2766 0
[pid=14299] vsize: 11644
Current children cumulated CPU time (s) 339.77
Current children cumulated vsize (Kb) 13768

[startup+350.046 s]
Raw data (loadavg): 0.99 0.94 0.94 2/58 14311
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2820 0 0 0 34947 30 0 0 25 0 1 0 1842179479 11952128 2807 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2918 2807 145 145 0 2773 0
[pid=14299] vsize: 11672
Current children cumulated CPU time (s) 349.77
Current children cumulated vsize (Kb) 13796

[startup+360.048 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14311
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2848 0 0 0 35947 30 0 0 25 0 1 0 1842179479 12083200 2835 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2950 2835 145 145 0 2805 0
[pid=14299] vsize: 11800
Current children cumulated CPU time (s) 359.77
Current children cumulated vsize (Kb) 13924

[startup+370.049 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14311
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2848 0 0 0 36947 31 0 0 25 0 1 0 1842179479 12083200 2835 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2950 2835 145 145 0 2805 0
[pid=14299] vsize: 11800
Current children cumulated CPU time (s) 369.78
Current children cumulated vsize (Kb) 13924

[startup+380.05 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14311
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2848 0 0 0 37948 31 0 0 25 0 1 0 1842179479 12083200 2835 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2950 2835 145 145 0 2805 0
[pid=14299] vsize: 11800
Current children cumulated CPU time (s) 379.79
Current children cumulated vsize (Kb) 13924

[startup+390.05 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14313
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2885 0 0 0 38947 31 0 0 25 0 1 0 1842179479 12234752 2872 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 2987 2872 145 145 0 2842 0
[pid=14299] vsize: 11948
Current children cumulated CPU time (s) 389.78
Current children cumulated vsize (Kb) 14072

[startup+400.051 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14313
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 2936 0 0 0 39946 31 0 0 25 0 1 0 1842179479 12443648 2923 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 3038 2923 145 145 0 2893 0
[pid=14299] vsize: 12152
Current children cumulated CPU time (s) 399.77
Current children cumulated vsize (Kb) 14276

[startup+410.053 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14313
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3011 0 0 0 40944 32 0 0 25 0 1 0 1842179479 12746752 2998 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3112 2998 145 145 0 2967 0
[pid=14299] vsize: 12448
Current children cumulated CPU time (s) 409.76
Current children cumulated vsize (Kb) 14572

[startup+420.054 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14313
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3014 0 0 0 41944 32 0 0 25 0 1 0 1842179479 12759040 3001 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3115 3001 145 145 0 2970 0
[pid=14299] vsize: 12460
Current children cumulated CPU time (s) 419.76
Current children cumulated vsize (Kb) 14584

[startup+430.055 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14313
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3039 0 0 0 42944 33 0 0 25 0 1 0 1842179479 12869632 3026 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3142 3026 145 145 0 2997 0
[pid=14299] vsize: 12568
Current children cumulated CPU time (s) 429.77
Current children cumulated vsize (Kb) 14692

[startup+440.056 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14313
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3048 0 0 0 43944 33 0 0 25 0 1 0 1842179479 12910592 3035 4294967295 134512640 135094434 3221224448 3221223120 134555771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3152 3035 145 145 0 3007 0
[pid=14299] vsize: 12608
Current children cumulated CPU time (s) 439.77
Current children cumulated vsize (Kb) 14732

[startup+450.057 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14315
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3060 0 0 0 44944 33 0 0 25 0 1 0 1842179479 12955648 3047 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3163 3047 145 145 0 3018 0
[pid=14299] vsize: 12652
Current children cumulated CPU time (s) 449.77
Current children cumulated vsize (Kb) 14776

[startup+460.059 s]
Raw data (loadavg): 0.99 0.95 0.94 2/58 14315
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3089 0 0 0 45943 33 0 0 25 0 1 0 1842179479 13074432 3076 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3192 3076 145 145 0 3047 0
[pid=14299] vsize: 12768
Current children cumulated CPU time (s) 459.76
Current children cumulated vsize (Kb) 14892

[startup+470.06 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14315
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3093 0 0 0 46943 33 0 0 25 0 1 0 1842179479 13090816 3080 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3196 3080 145 145 0 3051 0
[pid=14299] vsize: 12784
Current children cumulated CPU time (s) 469.76
Current children cumulated vsize (Kb) 14908

[startup+480.061 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14315
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3098 0 0 0 47944 33 0 0 25 0 1 0 1842179479 13111296 3085 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3201 3085 145 145 0 3056 0
[pid=14299] vsize: 12804
Current children cumulated CPU time (s) 479.77
Current children cumulated vsize (Kb) 14928

[startup+490.062 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14315
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3115 0 0 0 48943 33 0 0 25 0 1 0 1842179479 13197312 3102 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3222 3102 145 145 0 3077 0
[pid=14299] vsize: 12888
Current children cumulated CPU time (s) 489.76
Current children cumulated vsize (Kb) 15012

[startup+500.063 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14315
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3123 0 0 0 49944 34 0 0 25 0 1 0 1842179479 13230080 3110 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3230 3110 145 145 0 3085 0
[pid=14299] vsize: 12920
Current children cumulated CPU time (s) 499.78
Current children cumulated vsize (Kb) 15044

[startup+510.064 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14317
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3123 0 0 0 50944 34 0 0 25 0 1 0 1842179479 13230080 3110 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3230 3110 145 145 0 3085 0
[pid=14299] vsize: 12920
Current children cumulated CPU time (s) 509.78
Current children cumulated vsize (Kb) 15044

[startup+520.065 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14317
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3123 0 0 0 51944 34 0 0 25 0 1 0 1842179479 13230080 3110 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3230 3110 145 145 0 3085 0
[pid=14299] vsize: 12920
Current children cumulated CPU time (s) 519.78
Current children cumulated vsize (Kb) 15044

[startup+530.066 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14317
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3130 0 0 0 52944 34 0 0 25 0 1 0 1842179479 13262848 3117 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3238 3117 145 145 0 3093 0
[pid=14299] vsize: 12952
Current children cumulated CPU time (s) 529.78
Current children cumulated vsize (Kb) 15076

[startup+540.067 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14317
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3130 0 0 0 53945 34 0 0 25 0 1 0 1842179479 13262848 3117 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3238 3117 145 145 0 3093 0
[pid=14299] vsize: 12952
Current children cumulated CPU time (s) 539.79
Current children cumulated vsize (Kb) 15076

[startup+550.068 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14317
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3133 0 0 0 54945 34 0 0 25 0 1 0 1842179479 13275136 3120 4294967295 134512640 135094434 3221224448 3221223120 134556236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3241 3120 145 145 0 3096 0
[pid=14299] vsize: 12964
Current children cumulated CPU time (s) 549.79
Current children cumulated vsize (Kb) 15088

[startup+560.069 s]
Raw data (loadavg): 0.99 0.96 0.94 2/58 14317
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3159 0 0 0 55945 34 0 0 25 0 1 0 1842179479 13381632 3146 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3267 3146 145 145 0 3122 0
[pid=14299] vsize: 13068
Current children cumulated CPU time (s) 559.79
Current children cumulated vsize (Kb) 15192

[startup+570.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14319
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3159 0 0 0 56945 34 0 0 25 0 1 0 1842179479 13381632 3146 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3267 3146 145 145 0 3122 0
[pid=14299] vsize: 13068
Current children cumulated CPU time (s) 569.79
Current children cumulated vsize (Kb) 15192

[startup+580.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14319
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3223 0 0 0 57944 34 0 0 25 0 1 0 1842179479 13647872 3210 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3332 3210 145 145 0 3187 0
[pid=14299] vsize: 13328
Current children cumulated CPU time (s) 579.78
Current children cumulated vsize (Kb) 15452

[startup+590.071 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14319
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3271 0 0 0 58944 34 0 0 25 0 1 0 1842179479 13844480 3258 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3380 3258 145 145 0 3235 0
[pid=14299] vsize: 13520
Current children cumulated CPU time (s) 589.78
Current children cumulated vsize (Kb) 15644

[startup+600.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14319
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3279 0 0 0 59944 34 0 0 25 0 1 0 1842179479 13893632 3266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3392 3266 145 145 0 3247 0
[pid=14299] vsize: 13568
Current children cumulated CPU time (s) 599.78
Current children cumulated vsize (Kb) 15692

[startup+610.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14319
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3279 0 0 0 60944 34 0 0 25 0 1 0 1842179479 13893632 3266 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 3392 3266 145 145 0 3247 0
[pid=14299] vsize: 13568
Current children cumulated CPU time (s) 609.78
Current children cumulated vsize (Kb) 15692

[startup+620.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14319
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3391 0 0 0 61941 35 0 0 25 0 1 0 1842179479 14331904 3378 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 3499 3378 145 145 0 3354 0
[pid=14299] vsize: 13996
Current children cumulated CPU time (s) 619.76
Current children cumulated vsize (Kb) 16120

[startup+630.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14321
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3394 0 0 0 62941 36 0 0 25 0 1 0 1842179479 14348288 3381 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3503 3381 145 145 0 3358 0
[pid=14299] vsize: 14012
Current children cumulated CPU time (s) 629.77
Current children cumulated vsize (Kb) 16136

[startup+640.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14321
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3495 0 0 0 63939 37 0 0 25 0 1 0 1842179479 14761984 3482 4294967295 134512640 135094434 3221224448 3221223120 134555828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3604 3482 145 145 0 3459 0
[pid=14299] vsize: 14416
Current children cumulated CPU time (s) 639.76
Current children cumulated vsize (Kb) 16540

[startup+650.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14321
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3502 0 0 0 64939 37 0 0 25 0 1 0 1842179479 14794752 3489 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3612 3489 145 145 0 3467 0
[pid=14299] vsize: 14448
Current children cumulated CPU time (s) 649.76
Current children cumulated vsize (Kb) 16572

[startup+660.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14321
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3571 0 0 0 65937 38 0 0 25 0 1 0 1842179479 15081472 3558 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3682 3558 145 145 0 3537 0
[pid=14299] vsize: 14728
Current children cumulated CPU time (s) 659.75
Current children cumulated vsize (Kb) 16852

[startup+670.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14321
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3581 0 0 0 66937 38 0 0 25 0 1 0 1842179479 15147008 3568 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3698 3568 145 145 0 3553 0
[pid=14299] vsize: 14792
Current children cumulated CPU time (s) 669.75
Current children cumulated vsize (Kb) 16916

[startup+680.08 s]
Raw data (loadavg): 0.99 0.97 0.94 2/58 14321
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3581 0 0 0 67937 38 0 0 25 0 1 0 1842179479 15147008 3568 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3698 3568 145 145 0 3553 0
[pid=14299] vsize: 14792
Current children cumulated CPU time (s) 679.75
Current children cumulated vsize (Kb) 16916

[startup+690.081 s]
Raw data (loadavg): 1.07 0.99 0.95 2/58 14323
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3581 0 0 0 68937 38 0 0 25 0 1 0 1842179479 15147008 3568 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3698 3568 145 145 0 3553 0
[pid=14299] vsize: 14792
Current children cumulated CPU time (s) 689.75
Current children cumulated vsize (Kb) 16916

[startup+700.082 s]
Raw data (loadavg): 1.06 0.99 0.95 2/58 14323
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3581 0 0 0 69938 38 0 0 25 0 1 0 1842179479 15147008 3568 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3698 3568 145 145 0 3553 0
[pid=14299] vsize: 14792
Current children cumulated CPU time (s) 699.76
Current children cumulated vsize (Kb) 16916

[startup+710.084 s]
Raw data (loadavg): 1.05 0.99 0.95 2/58 14323
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3586 0 0 0 70938 38 0 0 25 0 1 0 1842179479 15155200 3573 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3700 3573 145 145 0 3555 0
[pid=14299] vsize: 14800
Current children cumulated CPU time (s) 709.76
Current children cumulated vsize (Kb) 16924

[startup+720.085 s]
Raw data (loadavg): 1.04 0.99 0.95 2/58 14323
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3586 0 0 0 71938 38 0 0 25 0 1 0 1842179479 15155200 3573 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3700 3573 145 145 0 3555 0
[pid=14299] vsize: 14800
Current children cumulated CPU time (s) 719.76
Current children cumulated vsize (Kb) 16924

[startup+730.086 s]
Raw data (loadavg): 1.04 0.99 0.95 2/58 14323
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3586 0 0 0 72938 38 0 0 25 0 1 0 1842179479 15155200 3573 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3700 3573 145 145 0 3555 0
[pid=14299] vsize: 14800
Current children cumulated CPU time (s) 729.76
Current children cumulated vsize (Kb) 16924

[startup+740.087 s]
Raw data (loadavg): 1.03 0.99 0.95 2/58 14323
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3586 0 0 0 73939 38 0 0 25 0 1 0 1842179479 15155200 3573 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3700 3573 145 145 0 3555 0
[pid=14299] vsize: 14800
Current children cumulated CPU time (s) 739.77
Current children cumulated vsize (Kb) 16924

[startup+750.088 s]
Raw data (loadavg): 1.11 1.00 0.95 2/58 14325
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3594 0 0 0 74939 38 0 0 25 0 1 0 1842179479 15204352 3581 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3712 3581 145 145 0 3567 0
[pid=14299] vsize: 14848
Current children cumulated CPU time (s) 749.77
Current children cumulated vsize (Kb) 16972

[startup+760.09 s]
Raw data (loadavg): 1.09 1.00 0.95 2/58 14325
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3600 0 0 0 75939 38 0 0 25 0 1 0 1842179479 15224832 3587 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3717 3587 145 145 0 3572 0
[pid=14299] vsize: 14868
Current children cumulated CPU time (s) 759.77
Current children cumulated vsize (Kb) 16992

[startup+770.091 s]
Raw data (loadavg): 1.07 1.00 0.95 2/58 14325
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3628 0 0 0 76939 38 0 0 25 0 1 0 1842179479 15339520 3615 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3745 3615 145 145 0 3600 0
[pid=14299] vsize: 14980
Current children cumulated CPU time (s) 769.77
Current children cumulated vsize (Kb) 17104

[startup+780.092 s]
Raw data (loadavg): 1.06 1.00 0.95 2/58 14325
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3653 0 0 0 77939 39 0 0 25 0 1 0 1842179479 15441920 3640 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3770 3640 145 145 0 3625 0
[pid=14299] vsize: 15080
Current children cumulated CPU time (s) 779.78
Current children cumulated vsize (Kb) 17204

[startup+790.093 s]
Raw data (loadavg): 1.05 1.00 0.95 2/58 14325
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3653 0 0 0 78939 39 0 0 25 0 1 0 1842179479 15441920 3640 4294967295 134512640 135094434 3221224448 3221223008 134550333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3770 3640 145 145 0 3625 0
[pid=14299] vsize: 15080
Current children cumulated CPU time (s) 789.78
Current children cumulated vsize (Kb) 17204

[startup+800.094 s]
Raw data (loadavg): 1.04 1.00 0.95 2/58 14325
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3653 0 0 0 79939 39 0 0 25 0 1 0 1842179479 15441920 3640 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3770 3640 145 145 0 3625 0
[pid=14299] vsize: 15080
Current children cumulated CPU time (s) 799.78
Current children cumulated vsize (Kb) 17204

[startup+810.095 s]
Raw data (loadavg): 1.04 1.00 0.95 2/58 14327
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3653 0 0 0 80939 39 0 0 25 0 1 0 1842179479 15441920 3640 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3770 3640 145 145 0 3625 0
[pid=14299] vsize: 15080
Current children cumulated CPU time (s) 809.78
Current children cumulated vsize (Kb) 17204

[startup+820.095 s]
Raw data (loadavg): 1.03 1.00 0.95 2/58 14327
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3656 0 0 0 81940 39 0 0 25 0 1 0 1842179479 15454208 3643 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3773 3643 145 145 0 3628 0
[pid=14299] vsize: 15092
Current children cumulated CPU time (s) 819.79
Current children cumulated vsize (Kb) 17216

[startup+830.096 s]
Raw data (loadavg): 1.03 1.00 0.95 2/58 14327
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3671 0 0 0 82940 39 0 0 25 0 1 0 1842179479 15515648 3658 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3788 3658 145 145 0 3643 0
[pid=14299] vsize: 15152
Current children cumulated CPU time (s) 829.79
Current children cumulated vsize (Kb) 17276

[startup+840.097 s]
Raw data (loadavg): 1.02 1.00 0.95 2/58 14327
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3675 0 0 0 83940 39 0 0 25 0 1 0 1842179479 15532032 3662 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3792 3662 145 145 0 3647 0
[pid=14299] vsize: 15168
Current children cumulated CPU time (s) 839.79
Current children cumulated vsize (Kb) 17292

[startup+850.098 s]
Raw data (loadavg): 1.02 1.00 0.95 2/58 14327
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3680 0 0 0 84940 39 0 0 25 0 1 0 1842179479 15552512 3667 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3797 3667 145 145 0 3652 0
[pid=14299] vsize: 15188
Current children cumulated CPU time (s) 849.79
Current children cumulated vsize (Kb) 17312

[startup+860.1 s]
Raw data (loadavg): 1.01 1.00 0.95 2/58 14327
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3680 0 0 0 85940 39 0 0 25 0 1 0 1842179479 15552512 3667 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3797 3667 145 145 0 3652 0
[pid=14299] vsize: 15188
Current children cumulated CPU time (s) 859.79
Current children cumulated vsize (Kb) 17312

[startup+870.101 s]
Raw data (loadavg): 1.01 1.00 0.95 2/58 14329
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3684 0 0 0 86941 39 0 0 25 0 1 0 1842179479 15568896 3671 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3801 3671 145 145 0 3656 0
[pid=14299] vsize: 15204
Current children cumulated CPU time (s) 869.8
Current children cumulated vsize (Kb) 17328

[startup+880.102 s]
Raw data (loadavg): 1.01 1.00 0.95 2/58 14329
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3684 0 0 0 87941 39 0 0 25 0 1 0 1842179479 15568896 3671 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3801 3671 145 145 0 3656 0
[pid=14299] vsize: 15204
Current children cumulated CPU time (s) 879.8
Current children cumulated vsize (Kb) 17328

[startup+890.103 s]
Raw data (loadavg): 1.01 1.00 0.95 2/58 14329
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3684 0 0 0 88941 39 0 0 25 0 1 0 1842179479 15568896 3671 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3801 3671 145 145 0 3656 0
[pid=14299] vsize: 15204
Current children cumulated CPU time (s) 889.8
Current children cumulated vsize (Kb) 17328

[startup+900.104 s]
Raw data (loadavg): 1.01 1.00 0.95 2/58 14329
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3684 0 0 0 89941 39 0 0 25 0 1 0 1842179479 15568896 3671 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3801 3671 145 145 0 3656 0
[pid=14299] vsize: 15204
Current children cumulated CPU time (s) 899.8
Current children cumulated vsize (Kb) 17328

[startup+910.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14329
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3732 0 0 0 90941 39 0 0 25 0 1 0 1842179479 15765504 3719 4294967295 134512640 135094434 3221224448 3221223008 134550329 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3849 3719 145 145 0 3704 0
[pid=14299] vsize: 15396
Current children cumulated CPU time (s) 909.8
Current children cumulated vsize (Kb) 17520

[startup+920.107 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14329
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3732 0 0 0 91941 39 0 0 25 0 1 0 1842179479 15765504 3719 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3849 3719 145 145 0 3704 0
[pid=14299] vsize: 15396
Current children cumulated CPU time (s) 919.8
Current children cumulated vsize (Kb) 17520

[startup+930.108 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14331
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3776 0 0 0 92940 40 0 0 25 0 1 0 1842179479 15958016 3763 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3896 3763 145 145 0 3751 0
[pid=14299] vsize: 15584
Current children cumulated CPU time (s) 929.8
Current children cumulated vsize (Kb) 17708

[startup+940.109 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14331
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3776 0 0 0 93941 40 0 0 25 0 1 0 1842179479 15958016 3763 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3896 3763 145 145 0 3751 0
[pid=14299] vsize: 15584
Current children cumulated CPU time (s) 939.81
Current children cumulated vsize (Kb) 17708

[startup+950.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14331
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3776 0 0 0 94941 40 0 0 25 0 1 0 1842179479 15958016 3763 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 3896 3763 145 145 0 3751 0
[pid=14299] vsize: 15584
Current children cumulated CPU time (s) 949.81
Current children cumulated vsize (Kb) 17708

[startup+960.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14331
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3776 0 0 0 95941 40 0 0 25 0 1 0 1842179479 15958016 3763 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 3896 3763 145 145 0 3751 0
[pid=14299] vsize: 15584
Current children cumulated CPU time (s) 959.81
Current children cumulated vsize (Kb) 17708

[startup+970.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14331
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3864 0 0 0 96938 41 0 0 25 0 1 0 1842179479 16310272 3851 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 3982 3851 145 145 0 3837 0
[pid=14299] vsize: 15928
Current children cumulated CPU time (s) 969.79
Current children cumulated vsize (Kb) 18052

[startup+980.113 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14331
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3870 0 0 0 97938 42 0 0 25 0 1 0 1842179479 16343040 3857 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 3990 3857 145 145 0 3845 0
[pid=14299] vsize: 15960
Current children cumulated CPU time (s) 979.8
Current children cumulated vsize (Kb) 18084

[startup+990.114 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14333
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3876 0 0 0 98937 43 0 0 25 0 1 0 1842179479 16367616 3863 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 3996 3863 145 145 0 3851 0
[pid=14299] vsize: 15984
Current children cumulated CPU time (s) 989.8
Current children cumulated vsize (Kb) 18108

[startup+1000.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14333
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3884 0 0 0 99936 44 0 0 25 0 1 0 1842179479 16416768 3871 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4008 3871 145 145 0 3863 0
[pid=14299] vsize: 16032
Current children cumulated CPU time (s) 999.8
Current children cumulated vsize (Kb) 18156

[startup+1010.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14333
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3887 0 0 0 100935 44 0 0 25 0 1 0 1842179479 16429056 3874 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4011 3874 145 145 0 3866 0
[pid=14299] vsize: 16044
Current children cumulated CPU time (s) 1009.79
Current children cumulated vsize (Kb) 18168

[startup+1020.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14333
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3890 0 0 0 101935 45 0 0 25 0 1 0 1842179479 16445440 3877 4294967295 134512640 135094434 3221224448 3221223120 134555169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4015 3877 145 145 0 3870 0
[pid=14299] vsize: 16060
Current children cumulated CPU time (s) 1019.8
Current children cumulated vsize (Kb) 18184

[startup+1030.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14333
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3892 0 0 0 102935 45 0 0 25 0 1 0 1842179479 16453632 3879 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4017 3879 145 145 0 3872 0
[pid=14299] vsize: 16068
Current children cumulated CPU time (s) 1029.8
Current children cumulated vsize (Kb) 18192

[startup+1040.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14333
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3892 0 0 0 103935 45 0 0 25 0 1 0 1842179479 16453632 3879 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4017 3879 145 145 0 3872 0
[pid=14299] vsize: 16068
Current children cumulated CPU time (s) 1039.8
Current children cumulated vsize (Kb) 18192

[startup+1050.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14335
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3892 0 0 0 104934 46 0 0 25 0 1 0 1842179479 16453632 3879 4294967295 134512640 135094434 3221224448 3221223040 134556933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4017 3879 145 145 0 3872 0
[pid=14299] vsize: 16068
Current children cumulated CPU time (s) 1049.8
Current children cumulated vsize (Kb) 18192

[startup+1060.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14335
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3892 0 0 0 105934 46 0 0 25 0 1 0 1842179479 16453632 3879 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4017 3879 145 145 0 3872 0
[pid=14299] vsize: 16068
Current children cumulated CPU time (s) 1059.8
Current children cumulated vsize (Kb) 18192

[startup+1070.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14335
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3909 0 0 0 106934 47 0 0 25 0 1 0 1842179479 16519168 3896 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4033 3896 145 145 0 3888 0
[pid=14299] vsize: 16132
Current children cumulated CPU time (s) 1069.81
Current children cumulated vsize (Kb) 18256

[startup+1080.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14335
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3913 0 0 0 107933 47 0 0 25 0 1 0 1842179479 16535552 3900 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4037 3900 145 145 0 3892 0
[pid=14299] vsize: 16148
Current children cumulated CPU time (s) 1079.8
Current children cumulated vsize (Kb) 18272

[startup+1090.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14335
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3949 0 0 0 108932 48 0 0 25 0 1 0 1842179479 16683008 3936 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4073 3936 145 145 0 3928 0
[pid=14299] vsize: 16292
Current children cumulated CPU time (s) 1089.8
Current children cumulated vsize (Kb) 18416

[startup+1100.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14335
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 3953 0 0 0 109932 48 0 0 25 0 1 0 1842179479 16699392 3940 4294967295 134512640 135094434 3221224448 3221223136 134554748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14299/statm): 4077 3940 145 145 0 3932 0
[pid=14299] vsize: 16308
Current children cumulated CPU time (s) 1099.8
Current children cumulated vsize (Kb) 18432

[startup+1110.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14337
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4009 0 0 0 110930 49 0 0 25 0 1 0 1842179479 16928768 3996 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4133 3996 145 145 0 3988 0
[pid=14299] vsize: 16532
Current children cumulated CPU time (s) 1109.79
Current children cumulated vsize (Kb) 18656

[startup+1120.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14337
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4013 0 0 0 111930 49 0 0 25 0 1 0 1842179479 16945152 4000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4137 4000 145 145 0 3992 0
[pid=14299] vsize: 16548
Current children cumulated CPU time (s) 1119.79
Current children cumulated vsize (Kb) 18672

[startup+1130.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14337
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4030 0 0 0 112930 49 0 0 25 0 1 0 1842179479 17027072 4017 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4157 4017 145 145 0 4012 0
[pid=14299] vsize: 16628
Current children cumulated CPU time (s) 1129.79
Current children cumulated vsize (Kb) 18752

[startup+1140.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14337
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4030 0 0 0 113931 49 0 0 25 0 1 0 1842179479 17027072 4017 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4157 4017 145 145 0 4012 0
[pid=14299] vsize: 16628
Current children cumulated CPU time (s) 1139.8
Current children cumulated vsize (Kb) 18752

[startup+1150.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14337
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4035 0 0 0 114931 50 0 0 25 0 1 0 1842179479 17059840 4022 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4165 4022 145 145 0 4020 0
[pid=14299] vsize: 16660
Current children cumulated CPU time (s) 1149.81
Current children cumulated vsize (Kb) 18784

[startup+1160.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14337
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4035 0 0 0 115931 50 0 0 25 0 1 0 1842179479 17059840 4022 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4165 4022 145 145 0 4020 0
[pid=14299] vsize: 16660
Current children cumulated CPU time (s) 1159.81
Current children cumulated vsize (Kb) 18784

[startup+1170.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14339
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4035 0 0 0 116931 50 0 0 25 0 1 0 1842179479 17059840 4022 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4165 4022 145 145 0 4020 0
[pid=14299] vsize: 16660
Current children cumulated CPU time (s) 1169.81
Current children cumulated vsize (Kb) 18784

[startup+1180.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14339
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4035 0 0 0 117931 50 0 0 25 0 1 0 1842179479 17059840 4022 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4165 4022 145 145 0 4020 0
[pid=14299] vsize: 16660
Current children cumulated CPU time (s) 1179.81
Current children cumulated vsize (Kb) 18784

[startup+1190.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14339
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4058 0 0 0 118931 50 0 0 25 0 1 0 1842179479 17154048 4045 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4188 4045 145 145 0 4043 0
[pid=14299] vsize: 16752
Current children cumulated CPU time (s) 1189.81
Current children cumulated vsize (Kb) 18876

[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14339
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4061 0 0 0 119931 50 0 0 25 0 1 0 1842179479 17170432 4048 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4192 4048 145 145 0 4047 0
[pid=14299] vsize: 16768
Current children cumulated CPU time (s) 1199.81
Current children cumulated vsize (Kb) 18892

[startup+1210.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14339
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4062 0 0 0 120932 50 0 0 25 0 1 0 1842179479 17170432 4049 4294967295 134512640 135094434 3221224448 3221223120 134556502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4192 4049 145 145 0 4047 0
[pid=14299] vsize: 16768
Current children cumulated CPU time (s) 1209.82
Current children cumulated vsize (Kb) 18892



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/58 14339
Raw data (/proc/14295/stat): 14295 (minisat+_script) S 14294 14295 9102 0 -1 0 288 239 0 0 0 0 0 0 16 0 1 0 1842179474 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14295/statm): 531 226 485 147 0 384 0
[pid=14295] vsize: 2124
Raw data (/proc/14299/stat): 14299 (minisat+_64-bit) R 14295 14295 9102 0 -1 0 4062 0 0 0 120932 50 0 0 25 0 1 0 1842179479 17170432 4049 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14299/statm): 4192 4049 145 145 0 4047 0
[pid=14299] vsize: 16768
Current children cumulated CPU time (s) 1209.82
Current children cumulated vsize (Kb) 18892

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1209.83
CPU user time (s): 1209.32
CPU system time (s): 0.509922
CPU usage (%): 99.9734
Max. virtual memory (cumulated for all children) (Kb): 18892

Verifier Data

ERROR: no interpretation found !