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-5.opb
MD5SUM	54f6acf3ab92bda8abb11350f74de20e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-37
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.08
Number of variables	1150
Total number of constraints	80035
Number of constraints which are clauses	80035
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 5047

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        850932 kB
Buffers:         33764 kB
Cached:         107112 kB
SwapCached:       3828 kB
Active:          50288 kB
Inactive:        97312 kB
HighTotal:      131008 kB
HighFree:        21588 kB
LowTotal:       903652 kB
LowFree:        829344 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30536 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:58:20 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 3038 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80035 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 |   80035   160070 |   26678       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -37[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 |  147951   319392 |   49317       0        0     nan |  0.000 % |
c |       100 |  147312   318040 |   54248      57     1282    22.5 |  0.772 % |
c |       251 |  146773   316900 |   59673     187     2917    15.6 |  1.422 % |
c |       476 |  145213   313544 |   65640     368     5352    14.5 |  3.429 % |
c |       813 |  143505   309796 |   72205     621     8354    13.5 |  5.644 % |
c |      1320 |  139677   301273 |   79425    1008    13306    13.2 | 10.638 % |
c |      2079 |  135693   292365 |   87368    1543    19391    12.6 | 15.964 % |
c |      3218 |  129784   278974 |   96104    2359    29829    12.6 | 24.035 % |
c |      4926 |  122432   262085 |  105715    3616    48944    13.5 | 34.279 % |
c |      7488 |  111938   237654 |  116286    5258    69109    13.1 | 49.006 % |
c |     11332 |  101310   212553 |  127915    7785   111547    14.3 | 64.438 % |
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 |     14084 |   96816   201835 |   32272    9412   143299    15.2 | 64.438 % |
c |     14184 |   96772   201727 |   35499    9499   144028    15.2 | 71.052 % |
c |     14334 |   96570   201231 |   39049    9550   144833    15.2 | 71.359 % |
c |     14560 |   96295   200569 |   42954    9703   147277    15.2 | 71.772 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14788 |   96036   200007 |   32012    9819   147145    15.0 | 71.772 % |
c |     14888 |   96036   200007 |   35213    9919   148330    15.0 | 72.243 % |
c |     15038 |   96036   200007 |   38734   10069   149721    14.9 | 72.243 % |
c |     15263 |   96036   200007 |   42607   10294   154570    15.0 | 72.243 % |
c |     15600 |   95761   199378 |   46868   10569   160536    15.2 | 72.625 % |
c |     16106 |   95153   197892 |   51555   10886   169202    15.5 | 73.553 % |
c |     16865 |   94758   196946 |   56711   11525   181628    15.8 | 74.144 % |
c |     18004 |   94310   195868 |   62382   12430   205545    16.5 | 74.813 % |
c |     19713 |   94001   195126 |   68620   13894   265668    19.1 | 75.275 % |
c |     22276 |   92381   191245 |   75482   15687   319719    20.4 | 77.691 % |
c |     26120 |   91522   189173 |   83030   19074   495885    26.0 | 78.980 % |
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 |     27853 |   91077   188149 |   30359   20461   588458    28.8 | 78.980 % |
c |     27953 |   91077   188149 |   33394   20561   590686    28.7 | 79.629 % |
c |     28103 |   91026   188021 |   36734   20631   592469    28.7 | 79.706 % |
c |     28328 |   91026   188021 |   40407   20856   599678    28.8 | 79.706 % |
c |     28665 |   91026   188021 |   44448   21193   622260    29.4 | 79.706 % |
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 |     28969 |   90731   187263 |   30243   21322   628608    29.5 | 79.706 % |
c |     29069 |   90722   187240 |   33267   21414   632006    29.5 | 80.173 % |
c |     29219 |   90593   186934 |   36594   21396   633325    29.6 | 80.358 % |
c |     29445 |   90536   186795 |   40253   21617   652375    30.2 | 80.447 % |
c |     29782 |   90499   186706 |   44278   21904   668251    30.5 | 80.503 % |
c |     30289 |   90299   186216 |   48706   22108   682253    30.9 | 80.809 % |
c |     31048 |   90231   186060 |   53577   22782   711877    31.2 | 80.904 % |
c |     32187 |   89778   184940 |   58935   23599   766824    32.5 | 81.598 % |
c |     33896 |   89773   184929 |   64828   25280   869667    34.4 | 81.605 % |
c |     36458 |   89601   184511 |   71311   27781  1104154    39.7 | 81.868 % |
c |     40303 |   89001   183057 |   78442   30883  1452224    47.0 | 82.782 % |
c |     46069 |   88653   182193 |   86286   36261  1909440    52.7 | 83.326 % |
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 |     53577 |   88651   182222 |   29550   43705  2561808    58.6 | 83.326 % |
c |     53677 |   88651   182222 |   32505   43805  2563789    58.5 | 83.359 % |
c |     53827 |   88622   182151 |   35755   43811  2568576    58.6 | 83.404 % |
c |     54052 |   88622   182151 |   39331   44036  2589935    58.8 | 83.404 % |
c |     54389 |   88537   181938 |   43264   44316  2602581    58.7 | 83.542 % |
c |     54895 |   88502   181851 |   47590   44743  2640960    59.0 | 83.598 % |
c |     55654 |   88489   181818 |   52349   45410  2688658    59.2 | 83.620 % |
c |     56795 |   88255   181245 |   57584   46245  2798146    60.5 | 83.970 % |
c |     58504 |   88255   181245 |   63343   47954  2931810    61.1 | 83.970 % |
c |     61066 |   88117   180910 |   69677   50021  3189748    63.8 | 84.181 % |
c |     64910 |   88088   180842 |   76645   53834  3616238    67.2 | 84.220 % |
c |     70676 |   88083   180831 |   84309   59598  4123646    69.2 | 84.226 % |
c ==============================================================================
c [1mFound solution: -45[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 |     76602 |   87920   180446 |   29306   64994  4731142    72.8 | 84.226 % |
c |     76704 |   87920   180446 |   32236   65096  4739491    72.8 | 84.488 % |
c |     76855 |   87920   180446 |   35460   65247  4745429    72.7 | 84.488 % |
c |     77080 |   87920   180446 |   39006   65472  4759519    72.7 | 84.488 % |
c |     77417 |   87920   180446 |   42906   65809  4783089    72.7 | 84.488 % |
c |     77924 |   87920   180446 |   47197   66316  4834519    72.9 | 84.488 % |
c |     78684 |   87915   180435 |   51917   67073  4915209    73.3 | 84.494 % |
c |     79823 |   87782   180128 |   57109   67701  5020176    74.2 | 84.681 % |
c |     81531 |   87629   179763 |   62820   69363  5207979    75.1 | 84.907 % |
c |     84093 |   87629   179763 |   69102   71925  5462668    75.9 | 84.907 % |
c |     87937 |   87629   179763 |   76012   75769  5852613    77.2 | 84.907 % |
c |     93703 |   87615   179727 |   83613   81487  6335995    77.8 | 84.931 % |
c |    102352 |   87615   179727 |   91974   90136  7289858    80.9 | 84.931 % |
c |    115328 |   87613   179723 |  101172  103111  8798918    85.3 | 84.933 % |
c |    134790 |   87540   179550 |  111289  122522 11000809    89.8 | 85.040 % |
c |    163982 |   87270   178893 |  122418  150898 14231492    94.3 | 85.455 % |
c |    207771 |   87197   178706 |  134660   54694  5876777   107.4 | 85.578 % |
c |    273455 |   87182   178671 |  148126  120376 10322069    85.7 | 85.599 % |
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.94 0.90 2/54 32004
Raw data (stat): 32004 (runsolver) R 32003 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479247682 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 4929 0 0 0 984 14 0 0 25 0 1 0 479247682 23248896 4907 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5676 4907 603 41 0 5635 0
vsize: 22704
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 4938 0 0 0 1984 14 0 0 25 0 1 0 479247682 23248896 4916 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5676 4916 603 41 0 5635 0
vsize: 22704
[startup+30.0008 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 4949 0 0 0 2984 14 0 0 25 0 1 0 479247682 23384064 4927 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5709 4927 603 41 0 5668 0
vsize: 22836
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 4959 0 0 0 3984 14 0 0 25 0 1 0 479247682 23384064 4937 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5709 4937 603 41 0 5668 0
vsize: 22836
[startup+50.0005 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 4969 0 0 0 4984 14 0 0 25 0 1 0 479247682 23384064 4947 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5709 4947 603 41 0 5668 0
vsize: 22836
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 4980 0 0 0 5984 14 0 0 25 0 1 0 479247682 23523328 4958 4294967295 134512640 134672761 3221224624 3221223796 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 4958 603 41 0 5702 0
vsize: 22972
[startup+70.0016 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 4994 0 0 0 6984 14 0 0 25 0 1 0 479247682 23523328 4972 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 4972 603 41 0 5702 0
vsize: 22972
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 5018 0 0 0 7984 14 0 0 25 0 1 0 479247682 23658496 4996 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5776 4996 603 41 0 5735 0
vsize: 23104
[startup+90.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 5318 0 0 0 8984 15 0 0 25 0 1 0 479247682 25800704 5296 4294967295 134512640 134672761 3221224624 3221223776 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6299 5296 603 41 0 6258 0
vsize: 25196
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 5334 0 0 0 9984 15 0 0 25 0 1 0 479247682 25800704 5312 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6299 5312 603 41 0 6258 0
vsize: 25196
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 5621 0 0 0 10982 16 0 0 25 0 1 0 479247682 27009024 5599 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6594 5599 603 41 0 6553 0
vsize: 26376
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 5884 0 0 0 11981 17 0 0 25 0 1 0 479247682 28028928 5862 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6843 5862 603 41 0 6802 0
vsize: 27372
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 6424 0 0 0 12980 19 0 0 25 0 1 0 479247682 30314496 6402 4294967295 134512640 134672761 3221224624 3221223632 1075349729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7401 6402 603 41 0 7360 0
vsize: 29604
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 6791 0 0 0 13979 20 0 0 25 0 1 0 479247682 31793152 6769 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7762 6769 603 41 0 7721 0
vsize: 31048
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 7192 0 0 0 14978 21 0 0 25 0 1 0 479247682 33538048 7170 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8188 7170 603 41 0 8147 0
vsize: 32752
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 7647 0 0 0 15976 23 0 0 25 0 1 0 479247682 35287040 7625 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8615 7625 603 41 0 8574 0
vsize: 34460
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 8034 0 0 0 16976 24 0 0 25 0 1 0 479247682 36917248 8012 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9013 8012 603 41 0 8972 0
vsize: 36052
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 8400 0 0 0 17975 25 0 0 25 0 1 0 479247682 38391808 8378 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9373 8378 603 41 0 9332 0
vsize: 37492
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 8814 0 0 0 18975 25 0 0 25 0 1 0 479247682 40140800 8792 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8792 603 41 0 9759 0
vsize: 39200
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 9254 0 0 0 19973 27 0 0 25 0 1 0 479247682 41873408 9232 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10223 9232 603 41 0 10182 0
vsize: 40892
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 9666 0 0 0 20973 28 0 0 25 0 1 0 479247682 43474944 9644 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10614 9644 603 41 0 10573 0
vsize: 42456
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 10045 0 0 0 21971 30 0 0 25 0 1 0 479247682 45084672 10023 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11007 10023 603 41 0 10966 0
vsize: 44028
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 10339 0 0 0 22971 30 0 0 25 0 1 0 479247682 46530560 10317 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11360 10317 603 41 0 11319 0
vsize: 45440
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 10612 0 0 0 23970 31 0 0 25 0 1 0 479247682 47607808 10590 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11623 10590 603 41 0 11582 0
vsize: 46492
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 10942 0 0 0 24970 32 0 0 25 0 1 0 479247682 48947200 10920 4294967295 134512640 134672761 3221224624 3221223760 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11950 10920 603 41 0 11909 0
vsize: 47800
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 11266 0 0 0 25969 33 0 0 25 0 1 0 479247682 50290688 11244 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12278 11244 603 41 0 12237 0
vsize: 49112
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 11567 0 0 0 26968 34 0 0 25 0 1 0 479247682 51478528 11545 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12568 11545 603 41 0 12527 0
vsize: 50272
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 11850 0 0 0 27967 34 0 0 25 0 1 0 479247682 52674560 11828 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12860 11828 603 41 0 12819 0
vsize: 51440
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 12149 0 0 0 28966 36 0 0 25 0 1 0 479247682 53870592 12127 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13152 12127 603 41 0 13111 0
vsize: 52608
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 12428 0 0 0 29966 37 0 0 25 0 1 0 479247682 55062528 12406 4294967295 134512640 134672761 3221224624 3221223760 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13443 12406 603 41 0 13402 0
vsize: 53772
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 12769 0 0 0 30965 38 0 0 25 0 1 0 479247682 56397824 12747 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13769 12747 603 41 0 13728 0
vsize: 55076
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 13132 0 0 0 31964 38 0 0 25 0 1 0 479247682 57851904 13110 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14124 13110 603 41 0 14083 0
vsize: 56496
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 13443 0 0 0 32963 39 0 0 25 0 1 0 479247682 59199488 13421 4294967295 134512640 134672761 3221224624 3221223792 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14453 13421 603 41 0 14412 0
vsize: 57812
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 13821 0 0 0 33962 41 0 0 25 0 1 0 479247682 60665856 13799 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14811 13799 603 41 0 14770 0
vsize: 59244
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 14105 0 0 0 34961 42 0 0 25 0 1 0 479247682 61865984 14083 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15104 14083 603 41 0 15063 0
vsize: 60416
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 14378 0 0 0 35960 43 0 0 25 0 1 0 479247682 62926848 14356 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15363 14356 603 41 0 15322 0
vsize: 61452
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 14650 0 0 0 36960 43 0 0 25 0 1 0 479247682 63991808 14628 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15623 14628 603 41 0 15582 0
vsize: 62492
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 14865 0 0 0 37960 44 0 0 25 0 1 0 479247682 64929792 14843 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15852 14843 603 41 0 15811 0
vsize: 63408
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 15195 0 0 0 38959 45 0 0 25 0 1 0 479247682 66260992 15173 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16177 15173 603 41 0 16136 0
vsize: 64708
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 15449 0 0 0 39958 46 0 0 25 0 1 0 479247682 67325952 15427 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16437 15427 603 41 0 16396 0
vsize: 65748
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 15771 0 0 0 40958 47 0 0 25 0 1 0 479247682 68669440 15749 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16765 15749 603 41 0 16724 0
vsize: 67060
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 16080 0 0 0 41957 47 0 0 25 0 1 0 479247682 69873664 16058 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17059 16058 603 41 0 17018 0
vsize: 68236
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 16350 0 0 0 42956 49 0 0 25 0 1 0 479247682 70942720 16328 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17320 16328 603 41 0 17279 0
vsize: 69280
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 16579 0 0 0 43955 50 0 0 25 0 1 0 479247682 71872512 16557 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17547 16557 603 41 0 17506 0
vsize: 70188
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 16823 0 0 0 44954 51 0 0 25 0 1 0 479247682 72933376 16801 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17806 16801 603 41 0 17765 0
vsize: 71224
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 17056 0 0 0 45954 52 0 0 25 0 1 0 479247682 73867264 17034 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18034 17034 603 41 0 17993 0
vsize: 72136
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 17312 0 0 0 46953 52 0 0 25 0 1 0 479247682 74801152 17290 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18262 17290 603 41 0 18221 0
vsize: 73048
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 17493 0 0 0 47953 53 0 0 25 0 1 0 479247682 75595776 17471 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18456 17471 603 41 0 18415 0
vsize: 73824
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 17641 0 0 0 48952 54 0 0 25 0 1 0 479247682 76263424 17619 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18619 17619 603 41 0 18578 0
vsize: 74476
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 17878 0 0 0 49952 54 0 0 25 0 1 0 479247682 77197312 17856 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18847 17856 603 41 0 18806 0
vsize: 75388
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 18207 0 0 0 50951 55 0 0 25 0 1 0 479247682 79073280 18185 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19305 18185 603 41 0 19264 0
vsize: 77220
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 18503 0 0 0 51950 56 0 0 25 0 1 0 479247682 80277504 18481 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19599 18481 603 41 0 19558 0
vsize: 78396
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 18782 0 0 0 52950 57 0 0 25 0 1 0 479247682 81346560 18760 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19860 18760 603 41 0 19819 0
vsize: 79440
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 19058 0 0 0 53949 58 0 0 25 0 1 0 479247682 82550784 19036 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20154 19036 603 41 0 20113 0
vsize: 80616
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 19335 0 0 0 54948 59 0 0 25 0 1 0 479247682 83611648 19313 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20413 19313 603 41 0 20372 0
vsize: 81652
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 19626 0 0 0 55948 59 0 0 25 0 1 0 479247682 84807680 19604 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20705 19604 603 41 0 20664 0
vsize: 82820
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 19812 0 0 0 56947 60 0 0 25 0 1 0 479247682 85606400 19790 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20900 19790 603 41 0 20859 0
vsize: 83600
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 19973 0 0 0 57947 61 0 0 25 0 1 0 479247682 86282240 19951 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21065 19951 603 41 0 21024 0
vsize: 84260
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 20145 0 0 0 58947 61 0 0 25 0 1 0 479247682 86945792 20123 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21227 20123 603 41 0 21186 0
vsize: 84908
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 20329 0 0 0 59946 62 0 0 25 0 1 0 479247682 87617536 20307 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21391 20307 603 41 0 21350 0
vsize: 85564
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 20535 0 0 0 60945 63 0 0 25 0 1 0 479247682 88563712 20513 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21622 20513 603 41 0 21581 0
vsize: 86488
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 20732 0 0 0 61944 64 0 0 25 0 1 0 479247682 89370624 20710 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21819 20710 603 41 0 21778 0
vsize: 87276
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 20932 0 0 0 62943 65 0 0 25 0 1 0 479247682 90173440 20910 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22015 20910 603 41 0 21974 0
vsize: 88060
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 21119 0 0 0 63942 66 0 0 25 0 1 0 479247682 90841088 21097 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22178 21097 603 41 0 22137 0
vsize: 88712
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 21328 0 0 0 64942 66 0 0 25 0 1 0 479247682 91774976 21306 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22406 21306 603 41 0 22365 0
vsize: 89624
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 21548 0 0 0 65941 67 0 0 25 0 1 0 479247682 92573696 21526 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22601 21526 603 41 0 22560 0
vsize: 90404
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 21837 0 0 0 66940 69 0 0 25 0 1 0 479247682 93777920 21815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22895 21815 603 41 0 22854 0
vsize: 91580
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22079 0 0 0 67940 70 0 0 25 0 1 0 479247682 94851072 22057 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23157 22057 603 41 0 23116 0
vsize: 92628
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 68940 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 69940 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 70940 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 71940 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 72940 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 73940 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 74941 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 75941 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 76941 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 77940 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 78941 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 79941 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 80941 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 81941 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223808 134559663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 82941 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 83942 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 84942 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 85942 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 86942 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 87943 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 88943 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+900.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 89943 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 90943 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 91943 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 92943 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+940.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 93944 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 94944 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 95944 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 96944 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+980.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 97945 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+990.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 98945 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223728 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 99945 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 100945 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 101945 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223728 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 102945 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 103945 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 104946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 105946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 106946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 107946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 108946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 109946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 110946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 111946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 112946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 113946 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 114947 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 115947 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 116947 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 117947 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 118947 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32004
Raw data (stat): 32004 (minisat+) R 32003 28546 28545 0 -1 0 22274 0 0 0 119947 70 0 0 25 0 1 0 479247682 95518720 22252 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23320 22252 603 41 0 23279 0
vsize: 93280
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 32004
Raw data (stat): 32004 (minisat+) Z 32003 28546 28545 0 -1 12 22277 0 0 0 119948 74 0 0 25 0 1 0 479247682 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.07
CPU time (s): 1200.23
CPU user time (s): 1199.48
CPU system time (s): 0.748886
CPU usage (%): 100.014
Max. virtual memory (Kb): 93280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####