PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-2.opb
MD5SUM	fe7ff8b16c276b409b25a87eed31b6f9
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-38
Optimality of the best value was proved	NO
Number of terms in the objective function	1150
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	1150
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1150
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	1150
Total number of constraints	80851
Number of constraints which are clauses	80851
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5044

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-13 21:35:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3011 boxname=wulflinc3 idbench=335 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  fe7ff8b16c276b409b25a87eed31b6f9  /oldhome/oroussel/tmp/wulflinc3/normalized-frb50-23-2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc3/normalized-frb50-23-2.opb
IDLAUNCH: 3011
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        908772 kB
Buffers:         35212 kB
Cached:          67320 kB
SwapCached:       3276 kB
Active:          69504 kB
Inactive:        39188 kB
HighTotal:      131008 kB
HighFree:        59668 kB
LowTotal:       903652 kB
LowFree:        849104 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11456 kB
Committed_AS:    71708 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:55:31 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3011 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80851 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 |   80851   161702 |   26950       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  148737   320958 |   49579       0        0     nan |  0.000 % |
c |       101 |  148366   320193 |   54536      85      765     9.0 |  0.441 % |
c |       252 |  148029   319484 |   59990     220     3072    14.0 |  0.844 % |
c |       477 |  147140   317584 |   65989     414     5422    13.1 |  1.937 % |
c |       814 |  145503   314007 |   72588     695    10180    14.6 |  4.025 % |
c |      1320 |  141871   306005 |   79847    1052    14339    13.6 |  8.753 % |
c |      2079 |  136023   292923 |   87832    1565    21384    13.7 | 16.582 % |
c |      3218 |  130632   280671 |   96615    2487    32283    13.0 | 23.974 % |
c |      4926 |  123081   263362 |  106276    3797    51144    13.5 | 34.454 % |
c |      7488 |  115042   244888 |  116904    5568    76837    13.8 | 45.531 % |
c |     11332 |  106902   225592 |  128595    8647   126243    14.6 | 57.367 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12189 |  105355   221989 |   35118    9206   138743    15.1 | 57.367 % |
c |     12292 |  105334   221942 |   38629    9300   142332    15.3 | 59.672 % |
c |     12442 |  105154   221511 |   42492    9437   144616    15.3 | 59.940 % |
c |     12668 |  104547   220088 |   46742    9550   146897    15.4 | 60.812 % |
c |     13005 |  104266   219414 |   51416    9700   149137    15.4 | 61.231 % |
c |     13511 |  102353   214845 |   56557    9851   154585    15.7 | 64.142 % |
c |     14271 |  101471   212704 |   62213   10471   168910    16.1 | 65.388 % |
c |     15410 |  100525   210483 |   68435   11341   190635    16.8 | 66.819 % |
c |     17118 |   98376   205358 |   75278   12589   222288    17.7 | 69.882 % |
c |     19680 |   97425   203063 |   82806   14811   278397    18.8 | 71.285 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19987 |   96638   201152 |   32212   14981   283316    18.9 | 71.285 % |
c |     20087 |   96638   201152 |   35433   15081   285189    18.9 | 72.422 % |
c |     20237 |   96439   200654 |   38976   15146   288150    19.0 | 72.733 % |
c |     20462 |   96306   200334 |   42874   15335   293321    19.1 | 72.932 % |
c |     20799 |   95886   199340 |   47161   15583   300834    19.3 | 73.553 % |
c |     21306 |   95774   199086 |   51877   16064   315316    19.6 | 73.706 % |
c |     22066 |   95551   198555 |   57065   16757   339492    20.3 | 74.033 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22573 |   95160   197669 |   31720   17015   350326    20.6 | 74.033 % |
c |     22673 |   95160   197669 |   34892   17115   356501    20.8 | 74.686 % |
c |     22823 |   95106   197535 |   38381   17261   360565    20.9 | 74.772 % |
c |     23049 |   95013   197310 |   42219   17466   365076    20.9 | 74.910 % |
c |     23386 |   94966   197201 |   46441   17776   378604    21.3 | 74.975 % |
c |     23892 |   94961   197190 |   51085   18276   390433    21.4 | 74.981 % |
c |     24652 |   94399   195810 |   56193   18675   406360    21.8 | 75.842 % |
c |     25792 |   94283   195526 |   61813   19618   439777    22.4 | 76.021 % |
c |     27501 |   93887   194570 |   67994   21188   551252    26.0 | 76.623 % |
c |     30063 |   93580   193835 |   74794   23586   661515    28.0 | 77.085 % |
c |     33907 |   92526   191288 |   82273   26622   855765    32.1 | 78.683 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34660 |   92501   191256 |   30833   27346   890259    32.6 | 78.683 % |
c |     34760 |   92374   190951 |   33916   27407   892203    32.6 | 78.925 % |
c |     34910 |   92374   190951 |   37307   27557   897352    32.6 | 78.925 % |
c |     35135 |   92325   190828 |   41038   27771   909011    32.7 | 78.996 % |
c |     35472 |   92325   190828 |   45142   28108   929804    33.1 | 78.996 % |
c |     35978 |   92325   190828 |   49656   28614   952436    33.3 | 78.996 % |
c |     36737 |   91933   189887 |   54622   29190   998234    34.2 | 79.580 % |
c |     37877 |   91668   189231 |   60084   30184  1050966    34.8 | 79.977 % |
c |     39585 |   91179   188051 |   66093   31104  1123554    36.1 | 80.703 % |
c |     42147 |   90991   187592 |   72702   33536  1352386    40.3 | 80.990 % |
c |     45991 |   90915   187410 |   79972   37245  1889303    50.7 | 81.102 % |
c |     51757 |   90762   187040 |   87970   42879  2343683    54.7 | 81.333 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52914 |   90753   186986 |   30251   43937  2470581    56.2 | 81.333 % |
c |     53014 |   90753   186986 |   33276   44037  2472887    56.2 | 81.351 % |
c |     53164 |   90753   186986 |   36603   44187  2487369    56.3 | 81.351 % |
c |     53390 |   90753   186986 |   40264   44413  2502524    56.3 | 81.351 % |
c |     53727 |   90753   186986 |   44290   44750  2517712    56.3 | 81.351 % |
c |     54234 |   90712   186891 |   48719   45092  2552226    56.6 | 81.407 % |
c |     54995 |   90712   186891 |   53591   45853  2626768    57.3 | 81.407 % |
c |     56134 |   90698   186857 |   58950   46911  2726470    58.1 | 81.429 % |
c |     57843 |   90611   186643 |   64845   48530  2837380    58.5 | 81.556 % |
c |     60405 |   90521   186429 |   71330   50928  3048163    59.9 | 81.685 % |
c |     64249 |   90508   186398 |   78463   54678  3459802    63.3 | 81.705 % |
c |     70016 |   90366   186066 |   86309   60273  4054487    67.3 | 81.907 % |
c |     78665 |   90114   185438 |   94940   68614  5012115    73.0 | 82.308 % |
c |     91640 |   89808   184690 |  104434   80924  6476449    80.0 | 82.780 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    101349 |   89784   184660 |   29928   90515  7625234    84.2 | 82.780 % |
c |    101449 |   89740   184546 |   32920   23637  1615649    68.4 | 82.927 % |
c |    101600 |   89736   184536 |   36212   23784  1622993    68.2 | 82.933 % |
c |    101825 |   89736   184536 |   39834   24009  1640600    68.3 | 82.933 % |
c |    102162 |   89658   184344 |   43817   24307  1661876    68.4 | 83.056 % |
c |    102668 |   89497   183949 |   48199   24754  1694957    68.5 | 83.305 % |
c |    103427 |   89497   183949 |   53019   25513  1767199    69.3 | 83.305 % |
c |    104566 |   89497   183949 |   58321   26652  1884370    70.7 | 83.305 % |
c |    106275 |   89373   183652 |   64153   28323  2061056    72.8 | 83.490 % |
c |    108837 |   89373   183652 |   70568   30885  2343424    75.9 | 83.490 % |
c |    112681 |   89339   183568 |   77625   34664  2898101    83.6 | 83.544 % |
c |    118447 |   88995   182758 |   85388   40297  3742322    92.9 | 84.037 % |
c |    127096 |   88992   182751 |   93926   48945  4973106   101.6 | 84.041 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    128864 |   88967   182666 |   29655   50677  5251581   103.6 | 84.041 % |
c |    128964 |   88962   182655 |   32620   50775  5256860   103.5 | 84.087 % |
c |    129114 |   88962   182655 |   35882   50925  5267190   103.4 | 84.087 % |
c |    129339 |   88962   182655 |   39470   51150  5283543   103.3 | 84.087 % |
c |    129677 |   88962   182655 |   43417   51488  5324792   103.4 | 84.087 % |
c |    130183 |   88962   182655 |   47759   51994  5375997   103.4 | 84.087 % |
c |    130942 |   88962   182655 |   52535   52753  5461119   103.5 | 84.087 % |
c |    132081 |   88962   182655 |   57789   53892  5567309   103.3 | 84.087 % |
c |    133790 |   88962   182655 |   63568   55601  5753628   103.5 | 84.087 % |
c |    136353 |   88870   182433 |   69924   58139  6016906   103.5 | 84.220 % |
c |    140197 |   88770   182167 |   76917   61962  6470826   104.4 | 84.399 % |
c |    145963 |   88768   182163 |   84609   67727  7108180   105.0 | 84.401 % |
c |    154612 |   88725   182047 |   93070   76332  8360934   109.5 | 84.474 % |
c |    167586 |   88673   181922 |  102377   89282 10392161   116.4 | 84.554 % |
c |    187048 |   88609   181774 |  112614  108730 13218100   121.6 | 84.644 % |
c |    216240 |   88592   181733 |  123876  137917 17842959   129.4 | 84.670 % |
c |    260030 |   88397   181266 |  136263   36498  4124381   113.0 | 84.963 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 C806 -C805 -C804 -C803 -C802 -C801 C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 C625 -C624 -C623 -C622 C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 16342
Raw data (stat): 16342 (runsolver) R 16341 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421009260 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 4949 0 0 0 985 13 0 0 25 0 1 0 421009260 23375872 4927 4294967295 134512640 134672761 3221224640 3221223856 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5707 4927 603 41 0 5666 0
vsize: 22828
[startup+20.0019 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 4958 0 0 0 1985 13 0 0 25 0 1 0 421009260 23375872 4936 4294967295 134512640 134672761 3221224640 3221223764 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5707 4936 603 41 0 5666 0
vsize: 22828
[startup+30.0033 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 4967 0 0 0 2984 14 0 0 25 0 1 0 421009260 23375872 4945 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5707 4945 603 41 0 5666 0
vsize: 22828
[startup+40.0035 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 4980 0 0 0 3984 14 0 0 25 0 1 0 421009260 23511040 4958 4294967295 134512640 134672761 3221224640 3221223812 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5740 4958 603 41 0 5699 0
vsize: 22960
[startup+50.0047 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 4989 0 0 0 4984 14 0 0 25 0 1 0 421009260 23511040 4967 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5740 4967 603 41 0 5699 0
vsize: 22960
[startup+60.0047 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 5011 0 0 0 5983 14 0 0 25 0 1 0 421009260 23642112 4989 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5772 4989 603 41 0 5731 0
vsize: 23088
[startup+70.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 5051 0 0 0 6983 15 0 0 25 0 1 0 421009260 23814144 5029 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5814 5029 603 41 0 5773 0
vsize: 23256
[startup+80.0069 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 5329 0 0 0 7982 16 0 0 25 0 1 0 421009260 25821184 5307 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6304 5307 603 41 0 6263 0
vsize: 25216
[startup+90.0062 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 5350 0 0 0 8982 16 0 0 25 0 1 0 421009260 25821184 5328 4294967295 134512640 134672761 3221224640 3221223812 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6304 5328 603 41 0 6263 0
vsize: 25216
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 5508 0 0 0 9981 17 0 0 25 0 1 0 421009260 26476544 5486 4294967295 134512640 134672761 3221224640 3221223880 1074743793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6464 5486 603 41 0 6423 0
vsize: 25856
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 5866 0 0 0 10980 19 0 0 25 0 1 0 421009260 27959296 5844 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6826 5844 603 41 0 6785 0
vsize: 27304
[startup+120.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 6142 0 0 0 11978 20 0 0 25 0 1 0 421009260 29138944 6120 4294967295 134512640 134672761 3221224640 3221223812 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7114 6120 603 41 0 7073 0
vsize: 28456
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 6496 0 0 0 12977 21 0 0 25 0 1 0 421009260 30478336 6474 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7441 6474 603 41 0 7400 0
vsize: 29764
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 7122 0 0 0 13974 23 0 0 25 0 1 0 421009260 33280000 7100 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8125 7100 603 41 0 8084 0
vsize: 32500
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 7577 0 0 0 14973 25 0 0 25 0 1 0 421009260 35028992 7555 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8552 7555 603 41 0 8511 0
vsize: 34208
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 8015 0 0 0 15971 26 0 0 25 0 1 0 421009260 36859904 7993 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8999 7993 603 41 0 8958 0
vsize: 35996
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 8361 0 0 0 16969 28 0 0 25 0 1 0 421009260 38199296 8339 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9326 8339 603 41 0 9285 0
vsize: 37304
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 8809 0 0 0 17967 30 0 0 25 0 1 0 421009260 40079360 8787 4294967295 134512640 134672761 3221224640 3221223744 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9785 8787 603 41 0 9744 0
vsize: 39140
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 9193 0 0 0 18966 31 0 0 25 0 1 0 421009260 41558016 9171 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10146 9171 603 41 0 10105 0
vsize: 40584
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 9631 0 0 0 19965 32 0 0 25 0 1 0 421009260 43438080 9609 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10605 9609 603 41 0 10564 0
vsize: 42420
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 9966 0 0 0 20964 34 0 0 25 0 1 0 421009260 44781568 9944 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 9944 603 41 0 10892 0
vsize: 43732
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 10412 0 0 0 21962 35 0 0 25 0 1 0 421009260 46792704 10390 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11424 10390 603 41 0 11383 0
vsize: 45696
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 10826 0 0 0 22961 37 0 0 25 0 1 0 421009260 48537600 10804 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11850 10804 603 41 0 11809 0
vsize: 47400
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 11186 0 0 0 23959 39 0 0 25 0 1 0 421009260 50008064 11164 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12209 11164 603 41 0 12168 0
vsize: 48836
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 11552 0 0 0 24957 40 0 0 25 0 1 0 421009260 51490816 11530 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12571 11530 603 41 0 12530 0
vsize: 50284
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 11911 0 0 0 25955 42 0 0 25 0 1 0 421009260 52969472 11889 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12932 11889 603 41 0 12891 0
vsize: 51728
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 12198 0 0 0 26954 43 0 0 25 0 1 0 421009260 54034432 12176 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13192 12176 603 41 0 13151 0
vsize: 52768
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 12509 0 0 0 27953 44 0 0 25 0 1 0 421009260 55373824 12487 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13519 12487 603 41 0 13478 0
vsize: 54076
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 12878 0 0 0 28952 46 0 0 25 0 1 0 421009260 56844288 12856 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13878 12856 603 41 0 13837 0
vsize: 55512
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13266 0 0 0 29950 47 0 0 25 0 1 0 421009260 58445824 13244 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14269 13244 603 41 0 14228 0
vsize: 57076
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 30950 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 31950 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 32950 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 33950 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 34950 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 35951 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 36951 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 37951 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223940 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 38951 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 39951 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 40951 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 41952 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 42952 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223596 1075350205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13442 0 0 0 43952 48 0 0 25 0 1 0 421009260 59092992 13420 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14427 13420 603 41 0 14386 0
vsize: 57708
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13565 0 0 0 44952 48 0 0 25 0 1 0 421009260 59633664 13543 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14559 13543 603 41 0 14518 0
vsize: 58236
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 13940 0 0 0 45951 50 0 0 25 0 1 0 421009260 61247488 13918 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14953 13918 603 41 0 14912 0
vsize: 59812
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 14316 0 0 0 46950 51 0 0 25 0 1 0 421009260 62713856 14294 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15311 14294 603 41 0 15270 0
vsize: 61244
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 14615 0 0 0 47949 52 0 0 25 0 1 0 421009260 63913984 14593 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15604 14593 603 41 0 15563 0
vsize: 62416
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 14947 0 0 0 48949 52 0 0 25 0 1 0 421009260 65257472 14925 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15932 14925 603 41 0 15891 0
vsize: 63728
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 15331 0 0 0 49948 53 0 0 25 0 1 0 421009260 66867200 15309 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16325 15309 603 41 0 16284 0
vsize: 65300
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 15769 0 0 0 50946 55 0 0 25 0 1 0 421009260 68612096 15747 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 15747 603 41 0 16710 0
vsize: 67004
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 16218 0 0 0 51945 57 0 0 25 0 1 0 421009260 70488064 16196 4294967295 134512640 134672761 3221224640 3221223800 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17209 16196 603 41 0 17168 0
vsize: 68836
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 16610 0 0 0 52944 58 0 0 25 0 1 0 421009260 72097792 16588 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17602 16588 603 41 0 17561 0
vsize: 70408
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 16957 0 0 0 53944 58 0 0 25 0 1 0 421009260 73576448 16935 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17963 16935 603 41 0 17922 0
vsize: 71852
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 17280 0 0 0 54943 59 0 0 25 0 1 0 421009260 74899456 17258 4294967295 134512640 134672761 3221224640 3221223744 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18286 17258 603 41 0 18245 0
vsize: 73144
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 17613 0 0 0 55942 61 0 0 25 0 1 0 421009260 76226560 17591 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18610 17591 603 41 0 18569 0
vsize: 74440
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 17932 0 0 0 56941 61 0 0 25 0 1 0 421009260 77561856 17910 4294967295 134512640 134672761 3221224640 3221223808 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18936 17910 603 41 0 18895 0
vsize: 75744
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 18278 0 0 0 57940 63 0 0 25 0 1 0 421009260 78901248 18256 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19263 18256 603 41 0 19222 0
vsize: 77052
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 18592 0 0 0 58939 64 0 0 25 0 1 0 421009260 80224256 18570 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19586 18570 603 41 0 19545 0
vsize: 78344
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 18876 0 0 0 59938 65 0 0 25 0 1 0 421009260 81297408 18854 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19848 18854 603 41 0 19807 0
vsize: 79392
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 19223 0 0 0 60937 66 0 0 25 0 1 0 421009260 82763776 19201 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20206 19201 603 41 0 20165 0
vsize: 80824
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 19514 0 0 0 61936 67 0 0 25 0 1 0 421009260 83976192 19492 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20502 19492 603 41 0 20461 0
vsize: 82008
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 19760 0 0 0 62935 68 0 0 25 0 1 0 421009260 84910080 19738 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20730 19738 603 41 0 20689 0
vsize: 82920
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 20015 0 0 0 63934 70 0 0 25 0 1 0 421009260 85983232 19993 4294967295 134512640 134672761 3221224640 3221223812 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20992 19993 603 41 0 20951 0
vsize: 83968
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 20243 0 0 0 64934 70 0 0 25 0 1 0 421009260 86929408 20221 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21223 20221 603 41 0 21182 0
vsize: 84892
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 20505 0 0 0 65934 71 0 0 25 0 1 0 421009260 88002560 20483 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21485 20483 603 41 0 21444 0
vsize: 85940
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 20776 0 0 0 66933 72 0 0 25 0 1 0 421009260 89083904 20754 4294967295 134512640 134672761 3221224640 3221223808 134561360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21749 20754 603 41 0 21708 0
vsize: 86996
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 21051 0 0 0 67932 72 0 0 25 0 1 0 421009260 90152960 21029 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22010 21029 603 41 0 21969 0
vsize: 88040
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 21353 0 0 0 68932 73 0 0 25 0 1 0 421009260 91475968 21331 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22333 21331 603 41 0 22292 0
vsize: 89332
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 21664 0 0 0 69931 74 0 0 25 0 1 0 421009260 92667904 21642 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22624 21642 603 41 0 22583 0
vsize: 90496
[startup+710.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 21969 0 0 0 70930 75 0 0 25 0 1 0 421009260 94003200 21947 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22950 21947 603 41 0 22909 0
vsize: 91800
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 22298 0 0 0 71930 76 0 0 25 0 1 0 421009260 95330304 22276 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23274 22276 603 41 0 23233 0
vsize: 93096
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 22626 0 0 0 72929 77 0 0 25 0 1 0 421009260 96661504 22604 4294967295 134512640 134672761 3221224640 3221223596 1075349771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23599 22604 603 41 0 23558 0
vsize: 94396
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 22948 0 0 0 73928 78 0 0 25 0 1 0 421009260 98508800 22926 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24050 22926 603 41 0 24009 0
vsize: 96200
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 23305 0 0 0 74927 79 0 0 25 0 1 0 421009260 99971072 23283 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24407 23283 603 41 0 24366 0
vsize: 97628
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 23641 0 0 0 75926 80 0 0 25 0 1 0 421009260 101302272 23619 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24732 23619 603 41 0 24691 0
vsize: 98928
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 23938 0 0 0 76925 81 0 0 25 0 1 0 421009260 102494208 23916 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25023 23916 603 41 0 24982 0
vsize: 100092
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 24243 0 0 0 77924 82 0 0 25 0 1 0 421009260 103817216 24221 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25346 24221 603 41 0 25305 0
vsize: 101384
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 24461 0 0 0 78923 83 0 0 25 0 1 0 421009260 104628224 24439 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25544 24439 603 41 0 25503 0
vsize: 102176
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 24748 0 0 0 79922 85 0 0 25 0 1 0 421009260 105844736 24726 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25841 24726 603 41 0 25800 0
vsize: 103364
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 24959 0 0 0 80921 86 0 0 25 0 1 0 421009260 106659840 24937 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26040 24937 603 41 0 25999 0
vsize: 104160
[startup+820.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 25240 0 0 0 81921 86 0 0 25 0 1 0 421009260 107864064 25218 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26334 25218 603 41 0 26293 0
vsize: 105336
[startup+830.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 25462 0 0 0 82921 87 0 0 25 0 1 0 421009260 108802048 25440 4294967295 134512640 134672761 3221224640 3221223808 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26563 25440 603 41 0 26522 0
vsize: 106252
[startup+840.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 25724 0 0 0 83921 87 0 0 25 0 1 0 421009260 109740032 25702 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26792 25702 603 41 0 26751 0
vsize: 107168
[startup+850.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 25895 0 0 0 84921 88 0 0 25 0 1 0 421009260 110546944 25873 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26989 25873 603 41 0 26948 0
vsize: 107956
[startup+860.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 26210 0 0 0 85921 88 0 0 25 0 1 0 421009260 111755264 26188 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27284 26188 603 41 0 27243 0
vsize: 109136
[startup+870.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 26486 0 0 0 86920 89 0 0 25 0 1 0 421009260 112959488 26464 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27578 26464 603 41 0 27537 0
vsize: 110312
[startup+880.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 26721 0 0 0 87920 90 0 0 25 0 1 0 421009260 113881088 26699 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27803 26699 603 41 0 27762 0
vsize: 111212
[startup+890.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 26971 0 0 0 88919 91 0 0 25 0 1 0 421009260 114941952 26949 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28062 26949 603 41 0 28021 0
vsize: 112248
[startup+900.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 27234 0 0 0 89918 92 0 0 25 0 1 0 421009260 116006912 27212 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28322 27212 603 41 0 28281 0
vsize: 113288
[startup+910.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 27484 0 0 0 90918 92 0 0 25 0 1 0 421009260 116940800 27462 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28550 27462 603 41 0 28509 0
vsize: 114200
[startup+920.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 27742 0 0 0 91917 94 0 0 25 0 1 0 421009260 117997568 27720 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28808 27720 603 41 0 28767 0
vsize: 115232
[startup+930.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 27959 0 0 0 92916 94 0 0 25 0 1 0 421009260 118939648 27937 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29038 27937 603 41 0 28997 0
vsize: 116152
[startup+940.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 28218 0 0 0 93916 95 0 0 25 0 1 0 421009260 120004608 28196 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29298 28196 603 41 0 29257 0
vsize: 117192
[startup+950.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 28468 0 0 0 94915 95 0 0 25 0 1 0 421009260 120938496 28446 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29526 28447 603 41 0 29485 0
vsize: 118104
[startup+960.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 28700 0 0 0 95915 96 0 0 25 0 1 0 421009260 121876480 28678 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 28678 603 41 0 29714 0
vsize: 119020
[startup+970.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 28983 0 0 0 96914 97 0 0 25 0 1 0 421009260 123076608 28961 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30048 28961 603 41 0 30007 0
vsize: 120192
[startup+980.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 97914 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+990.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 98914 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 99915 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 100914 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 101914 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 102914 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 103914 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 104914 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223776 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 105914 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 106915 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 107915 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 108915 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 109915 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 110915 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 111916 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 112916 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223824 134558890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 113916 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 114916 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 115916 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223792 134542676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 116917 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 117917 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 118917 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16342
Raw data (stat): 16342 (minisat+) R 16341 10720 10719 0 -1 0 29050 0 0 0 119917 97 0 0 25 0 1 0 421009260 123338752 29028 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 29028 603 41 0 30071 0
vsize: 120448
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 16342
Raw data (stat): 16342 (minisat+) Z 16341 10720 10719 0 -1 12 29053 0 0 0 119917 103 0 0 25 0 1 0 421009260 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.12
CPU time (s): 1200.21
CPU user time (s): 1199.18
CPU system time (s): 1.03284
CPU usage (%): 100.008
Max. virtual memory (Kb): 120448
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####