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-3.opb
MD5SUM	140696e76e8ed6af142b84a22a9a8f01
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	81068
Number of constraints which are clauses	81068
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 5045

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        906856 kB
Buffers:         34264 kB
Cached:          57192 kB
SwapCached:          4 kB
Active:          51164 kB
Inactive:        43140 kB
HighTotal:      131008 kB
HighFree:        70224 kB
LowTotal:       903652 kB
LowFree:        836632 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27936 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:55:44 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 3020 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 81068 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 |   81068   162136 |   27022       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -34[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 |  148824   321085 |   49608       0        0     nan |  0.000 % |
c |       100 |  148525   320464 |   54568      89      647     7.3 |  0.364 % |
c |       250 |  147550   318365 |   60025     172     1582     9.2 |  1.583 % |
c |       475 |  146282   315603 |   66028     352     3233     9.2 |  3.202 % |
c |       813 |  144245   311162 |   72631     579     5643     9.7 |  5.871 % |
c |      1319 |  142081   306384 |   79894     969     9530     9.8 |  8.642 % |
c |      2078 |  137736   296703 |   87883    1563    16664    10.7 | 14.500 % |
c |      3217 |  131537   282628 |   96671    2418    27257    11.3 | 23.018 % |
c |      4925 |  123620   264611 |  106339    3613    42907    11.9 | 33.844 % |
c |      7487 |  113550   241172 |  116973    5356    67950    12.7 | 47.966 % |
c ==============================================================================
c [1mFound solution: -35[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 |      8942 |  109479   231646 |   36493    6398    83738    13.1 | 47.966 % |
c |      9042 |  109425   231526 |   40142    6488    84756    13.1 | 54.101 % |
c |      9192 |  108817   230122 |   44156    6542    85696    13.1 | 54.940 % |
c |      9417 |  108742   229957 |   48572    6753    88958    13.2 | 55.038 % |
c |      9754 |  107510   227021 |   53429    6943    92761    13.4 | 56.846 % |
c |     10260 |  105913   223216 |   58772    7155    97498    13.6 | 59.215 % |
c |     11020 |  105175   221476 |   64649    7673   105317    13.7 | 60.288 % |
c |     12159 |  103203   216846 |   71114    8489   120338    14.2 | 63.131 % |
c ==============================================================================
c [1mFound solution: -36[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 |     13203 |  100733   210967 |   33577    9056   136886    15.1 | 63.131 % |
c |     13303 |  100611   210685 |   36934    9131   139212    15.2 | 66.860 % |
c |     13453 |  100325   210019 |   40628    9181   139747    15.2 | 67.265 % |
c |     13678 |  100059   209371 |   44690    9352   142290    15.2 | 67.665 % |
c |     14015 |   99707   208499 |   49160    9535   150995    15.8 | 68.219 % |
c |     14522 |   99276   207440 |   54076   10000   163255    16.3 | 68.874 % |
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 |     14905 |   99017   206836 |   33005   10349   176652    17.1 | 68.874 % |
c |     15005 |   98880   206528 |   36305   10433   177386    17.0 | 69.468 % |
c |     15156 |   98646   205978 |   39936   10557   180672    17.1 | 69.807 % |
c |     15381 |   98366   205323 |   43929   10660   183391    17.2 | 70.205 % |
c |     15718 |   97960   204346 |   48322   10906   188208    17.3 | 70.808 % |
c |     16224 |   97329   202834 |   53154   11259   197451    17.5 | 71.755 % |
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 |     16609 |   97142   202333 |   32380   11543   200782    17.4 | 71.755 % |
c |     16709 |   97045   202091 |   35618   11621   201582    17.3 | 72.198 % |
c |     16860 |   96950   201864 |   39179   11735   204990    17.5 | 72.347 % |
c |     17088 |   96889   201715 |   43097   11909   209728    17.6 | 72.433 % |
c |     17425 |   96380   200482 |   47407   12147   216033    17.8 | 73.196 % |
c |     17932 |   96079   199749 |   52148   12412   237148    19.1 | 73.650 % |
c |     18692 |   95763   198984 |   57363   13024   253885    19.5 | 74.133 % |
c ==============================================================================
c [1mFound solution: -39[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 |     19374 |   95715   198918 |   31905   13669   272269    19.9 | 74.133 % |
c |     19474 |   95715   198918 |   35095   13769   274839    20.0 | 74.287 % |
c |     19624 |   95609   198662 |   38605   13853   276879    20.0 | 74.444 % |
c |     19849 |   95504   198406 |   42465   14055   280648    20.0 | 74.608 % |
c |     20186 |   95321   197961 |   46712   14273   290024    20.3 | 74.888 % |
c |     20692 |   95154   197572 |   51383   14648   305122    20.8 | 75.121 % |
c |     21451 |   94801   196722 |   56521   15251   327192    21.5 | 75.643 % |
c |     22590 |   93726   194151 |   62173   16066   352985    22.0 | 77.246 % |
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 |     23429 |   93460   193538 |   31153   16809   378976    22.5 | 77.246 % |
c |     23529 |   93460   193538 |   34268   16909   381017    22.5 | 77.671 % |
c |     23679 |   93460   193538 |   37695   17059   388758    22.8 | 77.671 % |
c |     23904 |   93460   193538 |   41464   17284   395681    22.9 | 77.671 % |
c |     24241 |   93370   193322 |   45611   17561   402866    22.9 | 77.805 % |
c |     24748 |   93155   192800 |   50172   17880   419682    23.5 | 78.132 % |
c |     25507 |   92786   191894 |   55189   18335   435938    23.8 | 78.691 % |
c |     26646 |   92029   190018 |   60708   19085   465968    24.4 | 79.853 % |
c |     28354 |   91911   189738 |   66779   20687   567048    27.4 | 80.025 % |
c |     30918 |   91718   189266 |   73457   23148   724187    31.3 | 80.312 % |
c |     34763 |   91541   188853 |   80802   26821  1007077    37.5 | 80.553 % |
c |     40529 |   91425   188555 |   88883   32336  1405077    43.5 | 80.745 % |
c |     49178 |   90591   186576 |   97771   40058  2307923    57.6 | 81.963 % |
c |     62152 |   90053   185258 |  107548   52252  3904159    74.7 | 82.791 % |
c |     81614 |   89718   184449 |  118303   70757  6817442    96.4 | 83.299 % |
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 |     92949 |   89145   183005 |   29715   81197  8186868   100.8 | 83.299 % |
c |     93050 |   89145   183005 |   32686   22034  1602261    72.7 | 84.175 % |
c |     93200 |   89036   182740 |   35955   22132  1607001    72.6 | 84.341 % |
c |     93426 |   88996   182646 |   39550   22127  1611092    72.8 | 84.397 % |
c |     93763 |   88996   182646 |   43505   22464  1641209    73.1 | 84.397 % |
c |     94269 |   88996   182646 |   47856   22970  1706790    74.3 | 84.397 % |
c |     95028 |   88949   182534 |   52641   23714  1783041    75.2 | 84.460 % |
c |     96167 |   88941   182514 |   57906   24846  1915727    77.1 | 84.472 % |
c |     97876 |   88901   182419 |   63696   26515  2138859    80.7 | 84.529 % |
c |    100438 |   88795   182161 |   70066   29050  2363631    81.4 | 84.692 % |
c |    104282 |   88753   182051 |   77073   32854  2852036    86.8 | 84.766 % |
c |    110048 |   88753   182051 |   84780   38620  3734405    96.7 | 84.766 % |
c |    118697 |   88753   182051 |   93258   47269  5406231   114.4 | 84.766 % |
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 |    129419 |   88785   182147 |   29595   57991  7188448   124.0 | 84.766 % |
c |    129519 |   88747   182048 |   32554   58060  7189895   123.8 | 84.813 % |
c |    129669 |   88747   182048 |   35809   58210  7203645   123.8 | 84.813 % |
c |    129894 |   88747   182048 |   39390   58435  7222308   123.6 | 84.813 % |
c |    130231 |   88747   182048 |   43330   58772  7240654   123.2 | 84.813 % |
c |    130737 |   88747   182048 |   47663   59278  7308626   123.3 | 84.813 % |
c |    131496 |   88747   182048 |   52429   60037  7397997   123.2 | 84.813 % |
c |    132635 |   88747   182048 |   57672   61176  7525501   123.0 | 84.813 % |
c |    134344 |   88747   182048 |   63439   62885  7690787   122.3 | 84.813 % |
c |    136908 |   88747   182048 |   69783   65449  7984177   122.0 | 84.813 % |
c |    140752 |   88734   182017 |   76761   69270  8519695   123.0 | 84.832 % |
c |    146518 |   88734   182017 |   84437   75036  9316076   124.2 | 84.832 % |
c |    155169 |   88734   182017 |   92881   83687 10482862   125.3 | 84.832 % |
c |    168144 |   88731   182010 |  102169   96657 12423900   128.5 | 84.837 % |
c |    187605 |   88731   182010 |  112386  116118 15556343   134.0 | 84.837 % |
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 |    200502 |   88705   181922 |   29568  127023 16926154   133.3 | 84.837 % |
c |    200602 |   88705   181922 |   32524   23397  1923533    82.2 | 84.876 % |
c |    200752 |   88705   181922 |   35777   23547  1936394    82.2 | 84.876 % |
c |    200977 |   88705   181922 |   39355   23772  1958482    82.4 | 84.876 % |
c |    201315 |   88705   181922 |   43290   24110  1985133    82.3 | 84.876 % |
c |    201821 |   88705   181922 |   47619   24616  2015838    81.9 | 84.876 % |
c |    202582 |   88689   181882 |   52381   25361  2086362    82.3 | 84.902 % |
c |    203721 |   88689   181882 |   57619   26500  2187127    82.5 | 84.902 % |
c |    205432 |   88689   181882 |   63381   28211  2387337    84.6 | 84.902 % |
c |    207994 |   88689   181882 |   69719   30773  2779868    90.3 | 84.902 % |
c |    211839 |   88689   181882 |   76691   34618  3316548    95.8 | 84.902 % |
c |    217605 |   88689   181882 |   84360   40384  4220056   104.5 | 84.902 % |
c |    226255 |   88679   181858 |   92797   49031  5387721   109.9 | 84.917 % |
c |    239230 |   88669   181834 |  102076   61996  7218396   116.4 | 84.932 % |
c |    258691 |   88669   181834 |  112284   81457 11453565   140.6 | 84.932 % |
c |    287884 |   88657   181806 |  123512  110646 15171541   137.1 | 84.949 % |
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.85 0.95 0.91 2/54 14380
Raw data (stat): 14380 (runsolver) R 14379 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479240077 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.0006 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 4948 0 0 0 985 13 0 0 25 0 1 0 479240077 23384064 4926 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5709 4926 603 41 0 5668 0
vsize: 22836
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 4956 0 0 0 1985 13 0 0 25 0 1 0 479240077 23384064 4934 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5709 4934 603 41 0 5668 0
vsize: 22836
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 4967 0 0 0 2985 13 0 0 25 0 1 0 479240077 23384064 4945 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5709 4945 603 41 0 5668 0
vsize: 22836
[startup+40.0028 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 4975 0 0 0 3984 13 0 0 25 0 1 0 479240077 23384064 4953 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5709 4953 603 41 0 5668 0
vsize: 22836
[startup+50.0033 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 4988 0 0 0 4984 14 0 0 25 0 1 0 479240077 23519232 4966 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5742 4966 603 41 0 5701 0
vsize: 22968
[startup+60.0026 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 4998 0 0 0 5984 14 0 0 25 0 1 0 479240077 23519232 4976 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5742 4976 603 41 0 5701 0
vsize: 22968
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 5281 0 0 0 6983 15 0 0 25 0 1 0 479240077 25509888 5259 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6228 5259 603 41 0 6187 0
vsize: 24912
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 5281 0 0 0 7983 15 0 0 25 0 1 0 479240077 25509888 5259 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6228 5259 603 41 0 6187 0
vsize: 24912
[startup+90.005 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 5282 0 0 0 8983 15 0 0 25 0 1 0 479240077 25509888 5260 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6228 5260 603 41 0 6187 0
vsize: 24912
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 5403 0 0 0 9982 15 0 0 25 0 1 0 479240077 26021888 5381 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6353 5381 603 41 0 6312 0
vsize: 25412
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 5581 0 0 0 10982 16 0 0 25 0 1 0 479240077 26882048 5559 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6563 5559 603 41 0 6522 0
vsize: 26252
[startup+120.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 6050 0 0 0 11980 18 0 0 25 0 1 0 479240077 28762112 6028 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7022 6028 603 41 0 6981 0
vsize: 28088
[startup+130.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 6521 0 0 0 12978 20 0 0 25 0 1 0 479240077 30650368 6499 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7483 6499 603 41 0 7442 0
vsize: 29932
[startup+140.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 6900 0 0 0 13978 21 0 0 25 0 1 0 479240077 32264192 6878 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7877 6878 603 41 0 7836 0
vsize: 31508
[startup+150.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 7508 0 0 0 14976 23 0 0 25 0 1 0 479240077 34807808 7486 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8498 7486 603 41 0 8457 0
vsize: 33992
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 7938 0 0 0 15975 24 0 0 25 0 1 0 479240077 36556800 7916 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8925 7916 603 41 0 8884 0
vsize: 35700
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 8553 0 0 0 16973 26 0 0 25 0 1 0 479240077 38985728 8531 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9518 8531 603 41 0 9477 0
vsize: 38072
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 9018 0 0 0 17970 29 0 0 25 0 1 0 479240077 40869888 8996 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9978 8996 603 41 0 9937 0
vsize: 39912
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 9443 0 0 0 18970 30 0 0 25 0 1 0 479240077 42618880 9421 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10405 9421 603 41 0 10364 0
vsize: 41620
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 10010 0 0 0 19968 32 0 0 25 0 1 0 479240077 44896256 9988 4294967295 134512640 134672761 3221224624 3221223728 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10961 9988 603 41 0 10920 0
vsize: 43844
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 10535 0 0 0 20966 34 0 0 25 0 1 0 479240077 47046656 10513 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11486 10513 603 41 0 11445 0
vsize: 45944
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 11027 0 0 0 21965 35 0 0 25 0 1 0 479240077 49061888 11005 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11978 11005 603 41 0 11937 0
vsize: 47912
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 11704 0 0 0 22963 38 0 0 25 0 1 0 479240077 52146176 11682 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12731 11682 603 41 0 12690 0
vsize: 50924
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 12123 0 0 0 23962 39 0 0 25 0 1 0 479240077 53882880 12101 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13155 12101 603 41 0 13114 0
vsize: 52620
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 12432 0 0 0 24961 40 0 0 25 0 1 0 479240077 55095296 12410 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 12410 603 41 0 13410 0
vsize: 53804
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 12541 0 0 0 25961 40 0 0 25 0 1 0 479240077 55496704 12519 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13549 12519 603 41 0 13508 0
vsize: 54196
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 12849 0 0 0 26960 42 0 0 25 0 1 0 479240077 56836096 12827 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13876 12827 603 41 0 13835 0
vsize: 55504
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13308 0 0 0 27959 43 0 0 25 0 1 0 479240077 58716160 13286 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14335 13286 603 41 0 14294 0
vsize: 57340
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13771 0 0 0 28957 45 0 0 25 0 1 0 479240077 60579840 13749 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14790 13749 603 41 0 14749 0
vsize: 59160
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 29956 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 30957 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 31957 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 32957 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 33957 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 34957 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 35957 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 36957 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 37958 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13947 0 0 0 38958 46 0 0 25 0 1 0 479240077 61198336 13925 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13925 603 41 0 14900 0
vsize: 59764
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13948 0 0 0 39958 46 0 0 25 0 1 0 479240077 61198336 13926 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13926 603 41 0 14900 0
vsize: 59764
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13948 0 0 0 40958 46 0 0 25 0 1 0 479240077 61198336 13926 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13926 603 41 0 14900 0
vsize: 59764
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 13948 0 0 0 41958 46 0 0 25 0 1 0 479240077 61198336 13926 4294967295 134512640 134672761 3221224624 3221223728 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14941 13926 603 41 0 14900 0
vsize: 59764
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 14295 0 0 0 42957 47 0 0 25 0 1 0 479240077 62676992 14273 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15302 14273 603 41 0 15261 0
vsize: 61208
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 14626 0 0 0 43956 49 0 0 25 0 1 0 479240077 64020480 14604 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15630 14604 603 41 0 15589 0
vsize: 62520
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 15063 0 0 0 44955 50 0 0 25 0 1 0 479240077 65761280 15041 4294967295 134512640 134672761 3221224624 3221223760 134560606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16055 15041 603 41 0 16014 0
vsize: 64220
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 15382 0 0 0 45955 50 0 0 25 0 1 0 479240077 67096576 15360 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16381 15360 603 41 0 16340 0
vsize: 65524
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 15715 0 0 0 46954 52 0 0 25 0 1 0 479240077 68427776 15693 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16706 15693 603 41 0 16665 0
vsize: 66824
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 16049 0 0 0 47953 53 0 0 25 0 1 0 479240077 69894144 16027 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17064 16027 603 41 0 17023 0
vsize: 68256
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 16415 0 0 0 48952 54 0 0 25 0 1 0 479240077 71360512 16393 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17422 16393 603 41 0 17381 0
vsize: 69688
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 16776 0 0 0 49951 55 0 0 25 0 1 0 479240077 72839168 16754 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17783 16754 603 41 0 17742 0
vsize: 71132
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 17206 0 0 0 50949 57 0 0 25 0 1 0 479240077 74571776 17184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18206 17184 603 41 0 18165 0
vsize: 72824
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 17619 0 0 0 51949 58 0 0 25 0 1 0 479240077 76288000 17597 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18625 17597 603 41 0 18584 0
vsize: 74500
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 17977 0 0 0 52948 58 0 0 25 0 1 0 479240077 77770752 17955 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18987 17955 603 41 0 18946 0
vsize: 75948
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 18344 0 0 0 53947 60 0 0 25 0 1 0 479240077 79237120 18322 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19345 18322 603 41 0 19304 0
vsize: 77380
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 18714 0 0 0 54946 61 0 0 25 0 1 0 479240077 80711680 18692 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19705 18692 603 41 0 19664 0
vsize: 78820
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 19032 0 0 0 55946 62 0 0 25 0 1 0 479240077 82038784 19010 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20029 19010 603 41 0 19988 0
vsize: 80116
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 19347 0 0 0 56945 62 0 0 25 0 1 0 479240077 83238912 19325 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20322 19325 603 41 0 20281 0
vsize: 81288
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 19697 0 0 0 57944 63 0 0 25 0 1 0 479240077 84697088 19675 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20678 19675 603 41 0 20637 0
vsize: 82712
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 20013 0 0 0 58943 65 0 0 25 0 1 0 479240077 86044672 19991 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21007 19991 603 41 0 20966 0
vsize: 84028
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 20318 0 0 0 59943 66 0 0 25 0 1 0 479240077 87240704 20296 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21299 20296 603 41 0 21258 0
vsize: 85196
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 20636 0 0 0 60942 67 0 0 25 0 1 0 479240077 88580096 20614 4294967295 134512640 134672761 3221224624 3221223728 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21626 20614 603 41 0 21585 0
vsize: 86504
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 20939 0 0 0 61940 68 0 0 25 0 1 0 479240077 89780224 20917 4294967295 134512640 134672761 3221224624 3221223808 134559033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21919 20917 603 41 0 21878 0
vsize: 87676
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 21249 0 0 0 62940 69 0 0 25 0 1 0 479240077 90976256 21227 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22211 21227 603 41 0 22170 0
vsize: 88844
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 21535 0 0 0 63939 70 0 0 25 0 1 0 479240077 92168192 21513 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22502 21513 603 41 0 22461 0
vsize: 90008
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 21815 0 0 0 64939 71 0 0 25 0 1 0 479240077 93364224 21793 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22794 21793 603 41 0 22753 0
vsize: 91176
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 22119 0 0 0 65938 71 0 0 25 0 1 0 479240077 94576640 22097 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23090 22097 603 41 0 23049 0
vsize: 92360
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 22465 0 0 0 66936 73 0 0 25 0 1 0 479240077 96034816 22443 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23446 22443 603 41 0 23405 0
vsize: 93784
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 22793 0 0 0 67936 74 0 0 25 0 1 0 479240077 97378304 22771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23774 22771 603 41 0 23733 0
vsize: 95096
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23071 0 0 0 68935 75 0 0 25 0 1 0 479240077 98443264 23049 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24034 23049 603 41 0 23993 0
vsize: 96136
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23397 0 0 0 69934 75 0 0 25 0 1 0 479240077 99778560 23375 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24360 23375 603 41 0 24319 0
vsize: 97440
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 70934 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 71934 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 72934 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 73934 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223808 134558671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 74934 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 75935 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 76935 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 77935 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 78935 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134559670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 79935 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 80935 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 81936 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 82936 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 83936 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 84936 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 85936 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 86937 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 87937 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 88937 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 89937 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 90937 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 91938 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 92938 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 93938 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 94938 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 95938 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 96938 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 97939 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 98939 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 99939 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 100939 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 101939 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 102940 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 103940 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 104940 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 105940 76 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 106939 77 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 107940 77 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 108940 77 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 109940 77 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 110940 77 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 111940 77 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23633 0 0 0 112941 77 0 0 25 0 1 0 479240077 100687872 23611 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24582 23611 603 41 0 24541 0
vsize: 98328
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 23846 0 0 0 113940 77 0 0 25 0 1 0 479240077 101625856 23824 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24811 23824 603 41 0 24770 0
vsize: 99244
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 24122 0 0 0 114940 78 0 0 25 0 1 0 479240077 102694912 24100 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25072 24100 603 41 0 25031 0
vsize: 100288
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 24363 0 0 0 115939 78 0 0 25 0 1 0 479240077 103763968 24341 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25333 24341 603 41 0 25292 0
vsize: 101332
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 24615 0 0 0 116939 79 0 0 25 0 1 0 479240077 104828928 24593 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25593 24593 603 41 0 25552 0
vsize: 102372
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 24870 0 0 0 117938 80 0 0 25 0 1 0 479240077 105762816 24848 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25821 24848 603 41 0 25780 0
vsize: 103284
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 25087 0 0 0 118938 81 0 0 25 0 1 0 479240077 106700800 25065 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26050 25065 603 41 0 26009 0
vsize: 104200
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14380
Raw data (stat): 14380 (minisat+) R 14379 10614 10613 0 -1 0 25297 0 0 0 119937 81 0 0 25 0 1 0 479240077 107499520 25275 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26245 25275 603 41 0 26204 0
vsize: 104980
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 14380
Raw data (stat): 14380 (minisat+) Z 14379 10614 10613 0 -1 12 25300 0 0 0 119938 86 0 0 25 0 1 0 479240077 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.08
CPU time (s): 1200.24
CPU user time (s): 1199.38
CPU system time (s): 0.862868
CPU usage (%): 100.014
Max. virtual memory (Kb): 104980
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####