PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 02:54:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4472 boxname=wulflinc24 idbench=336 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  140696e76e8ed6af142b84a22a9a8f01  /oldhome/oroussel/tmp/wulflinc24/normalized-frb50-23-3.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-frb50-23-3.opb /oldhome/oroussel/tmp/wulflinc24/normalized-frb50-23-3.opb
IDLAUNCH: 4472
/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:        831080 kB
Buffers:         35188 kB
Cached:         125476 kB
SwapCached:       3828 kB
Active:          56076 kB
Inactive:       111284 kB
HighTotal:      131008 kB
HighFree:         3192 kB
LowTotal:       903652 kB
LowFree:        827888 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30400 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:14:19 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 4472 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 81068 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   81068   162136 |   27022       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  148824   321085 |   49608       0        0     nan |  0.000 % |
c |       100 |  148525   320464 |   54568      89      647     7.3 |  0.364 % |
c |       250 |  147550   318365 |   60025     172     1582     9.2 |  1.583 % |
c |       475 |  146282   315603 |   66028     352     3233     9.2 |  3.202 % |
c |       813 |  144245   311162 |   72631     579     5643     9.7 |  5.871 % |
c |      1319 |  142081   306384 |   79894     969     9530     9.8 |  8.642 % |
c |      2078 |  137736   296703 |   87883    1563    16664    10.7 | 14.500 % |
c |      3217 |  131537   282628 |   96671    2418    27257    11.3 | 23.018 % |
c |      4925 |  123620   264611 |  106339    3613    42907    11.9 | 33.844 % |
c |      7487 |  113550   241172 |  116973    5356    67950    12.7 | 47.966 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8942 |  109479   231646 |   36493    6398    83738    13.1 | 47.966 % |
c |      9042 |  109425   231526 |   40142    6488    84756    13.1 | 54.101 % |
c |      9192 |  108817   230122 |   44156    6542    85696    13.1 | 54.940 % |
c |      9417 |  108742   229957 |   48572    6753    88958    13.2 | 55.038 % |
c |      9754 |  107510   227021 |   53429    6943    92761    13.4 | 56.846 % |
c |     10260 |  105913   223216 |   58772    7155    97498    13.6 | 59.215 % |
c |     11020 |  105175   221476 |   64649    7673   105317    13.7 | 60.288 % |
c |     12159 |  103203   216846 |   71114    8489   120338    14.2 | 63.131 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13203 |  100733   210967 |   33577    9056   136886    15.1 | 63.131 % |
c |     13303 |  100611   210685 |   36934    9131   139212    15.2 | 66.860 % |
c |     13453 |  100325   210019 |   40628    9181   139747    15.2 | 67.265 % |
c |     13678 |  100059   209371 |   44690    9352   142290    15.2 | 67.665 % |
c |     14015 |   99707   208499 |   49160    9535   150995    15.8 | 68.219 % |
c |     14522 |   99276   207440 |   54076   10000   163255    16.3 | 68.874 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14905 |   99017   206836 |   33005   10349   176652    17.1 | 68.874 % |
c |     15005 |   98880   206528 |   36305   10433   177386    17.0 | 69.468 % |
c |     15156 |   98646   205978 |   39936   10557   180672    17.1 | 69.807 % |
c |     15381 |   98366   205323 |   43929   10660   183391    17.2 | 70.205 % |
c |     15718 |   97960   204346 |   48322   10906   188208    17.3 | 70.808 % |
c |     16224 |   97329   202834 |   53154   11259   197451    17.5 | 71.755 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16609 |   97142   202333 |   32380   11543   200782    17.4 | 71.755 % |
c |     16709 |   97045   202091 |   35618   11621   201582    17.3 | 72.198 % |
c |     16860 |   96950   201864 |   39179   11735   204990    17.5 | 72.347 % |
c |     17088 |   96889   201715 |   43097   11909   209728    17.6 | 72.433 % |
c |     17425 |   96380   200482 |   47407   12147   216033    17.8 | 73.196 % |
c |     17932 |   96079   199749 |   52148   12412   237148    19.1 | 73.650 % |
c |     18692 |   95763   198984 |   57363   13024   253885    19.5 | 74.133 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19374 |   95715   198918 |   31905   13669   272269    19.9 | 74.133 % |
c |     19474 |   95715   198918 |   35095   13769   274839    20.0 | 74.287 % |
c |     19624 |   95609   198662 |   38605   13853   276879    20.0 | 74.444 % |
c |     19849 |   95504   198406 |   42465   14055   280648    20.0 | 74.608 % |
c |     20186 |   95321   197961 |   46712   14273   290024    20.3 | 74.888 % |
c |     20692 |   95154   197572 |   51383   14648   305122    20.8 | 75.121 % |
c |     21451 |   94801   196722 |   56521   15251   327192    21.5 | 75.643 % |
c |     22590 |   93726   194151 |   62173   16066   352985    22.0 | 77.246 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23429 |   93460   193538 |   31153   16809   378976    22.5 | 77.246 % |
c |     23529 |   93460   193538 |   34268   16909   381017    22.5 | 77.671 % |
c |     23679 |   93460   193538 |   37695   17059   388758    22.8 | 77.671 % |
c |     23904 |   93460   193538 |   41464   17284   395681    22.9 | 77.671 % |
c |     24241 |   93370   193322 |   45611   17561   402866    22.9 | 77.805 % |
c |     24748 |   93155   192800 |   50172   17880   419682    23.5 | 78.132 % |
c |     25507 |   92786   191894 |   55189   18335   435938    23.8 | 78.691 % |
c |     26646 |   92029   190018 |   60708   19085   465968    24.4 | 79.853 % |
c |     28354 |   91911   189738 |   66779   20687   567048    27.4 | 80.025 % |
c |     30918 |   91718   189266 |   73457   23148   724187    31.3 | 80.312 % |
c |     34763 |   91541   188853 |   80802   26821  1007077    37.5 | 80.553 % |
c |     40529 |   91425   188555 |   88883   32336  1405077    43.5 | 80.745 % |
c |     49178 |   90591   186576 |   97771   40058  2307923    57.6 | 81.963 % |
c |     62152 |   90053   185258 |  107548   52252  3904159    74.7 | 82.791 % |
c |     81614 |   89718   184449 |  118303   70757  6817442    96.4 | 83.299 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     92949 |   89145   183005 |   29715   81197  8186868   100.8 | 83.299 % |
c |     93050 |   89145   183005 |   32686   22034  1602261    72.7 | 84.175 % |
c |     93200 |   89036   182740 |   35955   22132  1607001    72.6 | 84.341 % |
c |     93426 |   88996   182646 |   39550   22127  1611092    72.8 | 84.397 % |
c |     93763 |   88996   182646 |   43505   22464  1641209    73.1 | 84.397 % |
c |     94269 |   88996   182646 |   47856   22970  1706790    74.3 | 84.397 % |
c |     95028 |   88949   182534 |   52641   23714  1783041    75.2 | 84.460 % |
c |     96167 |   88941   182514 |   57906   24846  1915727    77.1 | 84.472 % |
c |     97876 |   88901   182419 |   63696   26515  2138859    80.7 | 84.529 % |
c |    100438 |   88795   182161 |   70066   29050  2363631    81.4 | 84.692 % |
c |    104282 |   88753   182051 |   77073   32854  2852036    86.8 | 84.766 % |
c |    110048 |   88753   182051 |   84780   38620  3734405    96.7 | 84.766 % |
c |    118697 |   88753   182051 |   93258   47269  5406231   114.4 | 84.766 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    129419 |   88785   182147 |   29595   57991  7188448   124.0 | 84.766 % |
c |    129519 |   88747   182048 |   32554   58060  7189895   123.8 | 84.813 % |
c |    129669 |   88747   182048 |   35809   58210  7203645   123.8 | 84.813 % |
c |    129894 |   88747   182048 |   39390   58435  7222308   123.6 | 84.813 % |
c |    130231 |   88747   182048 |   43330   58772  7240654   123.2 | 84.813 % |
c |    130737 |   88747   182048 |   47663   59278  7308626   123.3 | 84.813 % |
c |    131496 |   88747   182048 |   52429   60037  7397997   123.2 | 84.813 % |
c |    132635 |   88747   182048 |   57672   61176  7525501   123.0 | 84.813 % |
c |    134344 |   88747   182048 |   63439   62885  7690787   122.3 | 84.813 % |
c |    136908 |   88747   182048 |   69783   65449  7984177   122.0 | 84.813 % |
c |    140752 |   88734   182017 |   76761   69270  8519695   123.0 | 84.832 % |
c |    146518 |   88734   182017 |   84437   75036  9316076   124.2 | 84.832 % |
c |    155169 |   88734   182017 |   92881   83687 10482862   125.3 | 84.832 % |
c |    168144 |   88731   182010 |  102169   96657 12423900   128.5 | 84.837 % |
c |    187605 |   88731   182010 |  112386  116118 15556343   134.0 | 84.837 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    200502 |   88705   181922 |   29568  127023 16926154   133.3 | 84.837 % |
c |    200602 |   88705   181922 |   32524   23397  1923533    82.2 | 84.876 % |
c |    200752 |   88705   181922 |   35777   23547  1936394    82.2 | 84.876 % |
c |    200977 |   88705   181922 |   39355   23772  1958482    82.4 | 84.876 % |
c |    201315 |   88705   181922 |   43290   24110  1985133    82.3 | 84.876 % |
c |    201821 |   88705   181922 |   47619   24616  2015838    81.9 | 84.876 % |
c |    202582 |   88689   181882 |   52381   25361  2086362    82.3 | 84.902 % |
c |    203721 |   88689   181882 |   57619   26500  2187127    82.5 | 84.902 % |
c |    205432 |   88689   181882 |   63381   28211  2387337    84.6 | 84.902 % |
c |    207994 |   88689   181882 |   69719   30773  2779868    90.3 | 84.902 % |
c |    211839 |   88689   181882 |   76691   34618  3316548    95.8 | 84.902 % |
c |    217605 |   88689   181882 |   84360   40384  4220056   104.5 | 84.902 % |
c |    226255 |   88679   181858 |   92797   49031  5387721   109.9 | 84.917 % |
c |    239230 |   88669   181834 |  102076   61996  7218396   116.4 | 84.932 % |
c |    258691 |   88669   181834 |  112284   81457 11453565   140.6 | 84.932 % |
c |    287884 |   88657   181806 |  123512  110646 15171541   137.1 | 84.949 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 2918
Raw data (stat): 2918 (runsolver) R 2917 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481143802 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99994 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 4926 0 0 0 986 12 0 0 25 0 1 0 481143802 23293952 4904 4294967295 134512640 134672761 3221224560 3221223568 1075349878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5687 4904 603 41 0 5646 0
vsize: 22748
[startup+20.0001 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 4934 0 0 0 1985 12 0 0 25 0 1 0 481143802 23293952 4912 4294967295 134512640 134672761 3221224560 3221223776 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5687 4912 603 41 0 5646 0
vsize: 22748
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 4945 0 0 0 2985 12 0 0 25 0 1 0 481143802 23293952 4923 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5687 4923 603 41 0 5646 0
vsize: 22748
[startup+40 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 4952 0 0 0 3984 13 0 0 25 0 1 0 481143802 23293952 4930 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5687 4930 603 41 0 5646 0
vsize: 22748
[startup+50 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 4966 0 0 0 4983 13 0 0 25 0 1 0 481143802 23429120 4944 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5720 4944 603 41 0 5679 0
vsize: 22880
[startup+60.0004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 4976 0 0 0 5983 13 0 0 25 0 1 0 481143802 23429120 4954 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5720 4954 603 41 0 5679 0
vsize: 22880
[startup+70.0001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 5114 0 0 0 6983 14 0 0 25 0 1 0 481143802 24342528 5092 4294967295 134512640 134672761 3221224560 3221223684 134566151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5943 5092 603 41 0 5902 0
vsize: 23772
[startup+80.0011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 5114 0 0 0 7983 14 0 0 25 0 1 0 481143802 24342528 5092 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5943 5092 603 41 0 5902 0
vsize: 23772
[startup+90.0005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 5152 0 0 0 8983 14 0 0 25 0 1 0 481143802 24477696 5130 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5976 5130 603 41 0 5935 0
vsize: 23904
[startup+100 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 5292 0 0 0 9983 14 0 0 25 0 1 0 481143802 25067520 5270 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6120 5270 603 41 0 6079 0
vsize: 24480
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 5466 0 0 0 10982 15 0 0 25 0 1 0 481143802 25882624 5444 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6319 5444 603 41 0 6278 0
vsize: 25276
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 5921 0 0 0 11981 16 0 0 25 0 1 0 481143802 27627520 5899 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6745 5899 603 41 0 6704 0
vsize: 26980
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 6406 0 0 0 12979 19 0 0 25 0 1 0 481143802 29646848 6384 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7238 6384 603 41 0 7197 0
vsize: 28952
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 6788 0 0 0 13978 19 0 0 25 0 1 0 481143802 31387648 6766 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 6766 603 41 0 7622 0
vsize: 30652
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 7386 0 0 0 14977 21 0 0 25 0 1 0 481143802 33792000 7364 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8250 7364 603 41 0 8209 0
vsize: 33000
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 7825 0 0 0 15976 22 0 0 25 0 1 0 481143802 35540992 7803 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8677 7803 603 41 0 8636 0
vsize: 34708
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 8431 0 0 0 16975 24 0 0 25 0 1 0 481143802 38080512 8409 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9297 8409 603 41 0 9256 0
vsize: 37188
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 8892 0 0 0 17973 25 0 0 25 0 1 0 481143802 39952384 8870 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9754 8870 603 41 0 9713 0
vsize: 39016
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 9322 0 0 0 18973 26 0 0 25 0 1 0 481143802 41676800 9300 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 9300 603 41 0 10134 0
vsize: 40700
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 9884 0 0 0 19971 28 0 0 25 0 1 0 481143802 43950080 9862 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9862 603 41 0 10689 0
vsize: 42920
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 10405 0 0 0 20969 30 0 0 25 0 1 0 481143802 46096384 10383 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11254 10383 603 41 0 11213 0
vsize: 45016
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 10890 0 0 0 21968 32 0 0 25 0 1 0 481143802 47972352 10868 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11712 10868 603 41 0 11671 0
vsize: 46848
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 11562 0 0 0 22966 34 0 0 25 0 1 0 481143802 51060736 11540 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12466 11540 603 41 0 12425 0
vsize: 49864
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 11988 0 0 0 23966 34 0 0 25 0 1 0 481143802 52805632 11966 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12892 11966 603 41 0 12851 0
vsize: 51568
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 12313 0 0 0 24965 35 0 0 25 0 1 0 481143802 54022144 12291 4294967295 134512640 134672761 3221224560 3221223776 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13189 12291 603 41 0 13148 0
vsize: 52756
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 12427 0 0 0 25965 36 0 0 25 0 1 0 481143802 54562816 12405 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13321 12405 603 41 0 13280 0
vsize: 53284
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 12714 0 0 0 26964 36 0 0 25 0 1 0 481143802 55779328 12692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13618 12692 603 41 0 13577 0
vsize: 54472
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13152 0 0 0 27963 38 0 0 25 0 1 0 481143802 57532416 13130 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14046 13130 603 41 0 14005 0
vsize: 56184
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13610 0 0 0 28961 39 0 0 25 0 1 0 481143802 59396096 13588 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14501 13588 603 41 0 14460 0
vsize: 58004
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 29961 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 30961 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 31961 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 32961 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223664 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2918
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 33962 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 2955
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 34962 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+360.012 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 2971
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 35962 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+370.011 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 2971
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 36957 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+380.012 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 2971
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 37958 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+390.012 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 2971
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13828 0 0 0 38958 40 0 0 25 0 1 0 481143802 60203008 13806 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13806 603 41 0 14657 0
vsize: 58792
[startup+400.012 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 2971
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13829 0 0 0 39958 40 0 0 25 0 1 0 481143802 60203008 13807 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13807 603 41 0 14657 0
vsize: 58792
[startup+410.012 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 2971
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13829 0 0 0 40958 40 0 0 25 0 1 0 481143802 60203008 13807 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13807 603 41 0 14657 0
vsize: 58792
[startup+420.012 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 2971
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 13829 0 0 0 41958 40 0 0 25 0 1 0 481143802 60203008 13807 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14698 13807 603 41 0 14657 0
vsize: 58792
[startup+430.013 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 14071 0 0 0 42958 41 0 0 25 0 1 0 481143802 61263872 14049 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14957 14049 603 41 0 14916 0
vsize: 59828
[startup+440.013 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 14431 0 0 0 43958 42 0 0 25 0 1 0 481143802 62738432 14409 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15317 14409 603 41 0 15276 0
vsize: 61268
[startup+450.013 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 14841 0 0 0 44956 43 0 0 25 0 1 0 481143802 64339968 14819 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15708 14819 603 41 0 15667 0
vsize: 62832
[startup+460.014 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 15191 0 0 0 45955 45 0 0 25 0 1 0 481143802 65814528 15169 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16068 15169 603 41 0 16027 0
vsize: 64272
[startup+470.013 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 15493 0 0 0 46954 46 0 0 25 0 1 0 481143802 67014656 15471 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16361 15471 603 41 0 16320 0
vsize: 65444
[startup+480.014 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 15826 0 0 0 47953 47 0 0 25 0 1 0 481143802 68476928 15804 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16718 15804 603 41 0 16677 0
vsize: 66872
[startup+490.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 16173 0 0 0 48952 48 0 0 25 0 1 0 481143802 69799936 16151 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17041 16151 603 41 0 17000 0
vsize: 68164
[startup+500.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 16521 0 0 0 49952 49 0 0 25 0 1 0 481143802 71262208 16499 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17398 16499 603 41 0 17357 0
vsize: 69592
[startup+510.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 16914 0 0 0 50950 50 0 0 25 0 1 0 481143802 72871936 16892 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17791 16892 603 41 0 17750 0
vsize: 71164
[startup+520.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 17323 0 0 0 51949 52 0 0 25 0 1 0 481143802 74477568 17301 4294967295 134512640 134672761 3221224560 3221223720 134561240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18183 17301 603 41 0 18142 0
vsize: 72732
[startup+530.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 17724 0 0 0 52948 53 0 0 25 0 1 0 481143802 76201984 17702 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18604 17702 603 41 0 18563 0
vsize: 74416
[startup+540.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 18037 0 0 0 53948 53 0 0 25 0 1 0 481143802 77402112 18015 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18897 18015 603 41 0 18856 0
vsize: 75588
[startup+550.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 18411 0 0 0 54947 54 0 0 25 0 1 0 481143802 79003648 18389 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19288 18389 603 41 0 19247 0
vsize: 77152
[startup+560.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 18764 0 0 0 55946 55 0 0 25 0 1 0 481143802 80334848 18742 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19613 18742 603 41 0 19572 0
vsize: 78452
[startup+570.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 19070 0 0 0 56945 57 0 0 25 0 1 0 481143802 81670144 19048 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19939 19048 603 41 0 19898 0
vsize: 79756
[startup+580.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 19384 0 0 0 57944 58 0 0 25 0 1 0 481143802 82874368 19362 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20233 19362 603 41 0 20192 0
vsize: 80932
[startup+590.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 19714 0 0 0 58944 58 0 0 25 0 1 0 481143802 84201472 19692 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20557 19692 603 41 0 20516 0
vsize: 82228
[startup+600.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 20006 0 0 0 59943 60 0 0 25 0 1 0 481143802 85401600 19984 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20850 19984 603 41 0 20809 0
vsize: 83400
[startup+610.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 20303 0 0 0 60942 61 0 0 25 0 1 0 481143802 86716416 20281 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21171 20281 603 41 0 21130 0
vsize: 84684
[startup+620.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 20600 0 0 0 61941 62 0 0 25 0 1 0 481143802 87916544 20578 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21464 20578 603 41 0 21423 0
vsize: 85856
[startup+630.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 20895 0 0 0 62940 63 0 0 25 0 1 0 481143802 89124864 20873 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21759 20873 603 41 0 21718 0
vsize: 87036
[startup+640.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 21185 0 0 0 63939 64 0 0 25 0 1 0 481143802 90193920 21163 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22020 21163 603 41 0 21979 0
vsize: 88080
[startup+650.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 21465 0 0 0 64939 64 0 0 25 0 1 0 481143802 91402240 21443 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22315 21443 603 41 0 22274 0
vsize: 89260
[startup+660.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 21734 0 0 0 65938 65 0 0 25 0 1 0 481143802 92459008 21712 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22573 21712 603 41 0 22532 0
vsize: 90292
[startup+670.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 22027 0 0 0 66937 66 0 0 25 0 1 0 481143802 93667328 22005 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22868 22005 603 41 0 22827 0
vsize: 91472
[startup+680.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 22358 0 0 0 67937 67 0 0 25 0 1 0 481143802 95006720 22336 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23195 22336 603 41 0 23154 0
vsize: 92780
[startup+690.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 22677 0 0 0 68936 68 0 0 25 0 1 0 481143802 96350208 22655 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23523 22655 603 41 0 23482 0
vsize: 94092
[startup+700.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 22940 0 0 0 69935 69 0 0 25 0 1 0 481143802 97419264 22918 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23784 22918 603 41 0 23743 0
vsize: 95136
[startup+710.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23250 0 0 0 70935 69 0 0 25 0 1 0 481143802 98623488 23228 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24078 23228 603 41 0 24037 0
vsize: 96312
[startup+720.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2973
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 71934 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+730.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 72935 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+740.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 73935 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+750.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 74935 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+760.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 75935 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+770.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 76935 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+780.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 77935 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223684 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+790.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 78936 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+800.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 79936 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+810.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 80936 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+820.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 81936 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+830.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 82936 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+840.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 83937 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+850.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 84936 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+860.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 85937 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223744 134559601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+870.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 86937 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+880.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 87937 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+890.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 88937 70 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+900.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 89937 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+910.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 90937 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+920.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 91937 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+930.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 92938 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+940.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 93938 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+950.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 94938 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+960.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 95938 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+970.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 96938 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+980.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 97939 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+990.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 98939 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 99939 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 100939 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 101939 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 102939 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 103940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 104940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 105940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 106940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 107940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 108940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 109939 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 110940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 111940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223664 134560139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 112940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 113940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23515 0 0 0 114940 71 0 0 25 0 1 0 481143802 99680256 23493 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24336 23493 603 41 0 24295 0
vsize: 97344
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23632 0 0 0 115940 72 0 0 25 0 1 0 481143802 100208640 23610 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24465 23610 603 41 0 24424 0
vsize: 97860
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 23887 0 0 0 116939 73 0 0 25 0 1 0 481143802 101277696 23865 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24726 23865 603 41 0 24685 0
vsize: 98904
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 24140 0 0 0 117939 73 0 0 25 0 1 0 481143802 102346752 24118 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24987 24118 603 41 0 24946 0
vsize: 99948
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 24371 0 0 0 118938 74 0 0 25 0 1 0 481143802 103272448 24349 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25213 24349 603 41 0 25172 0
vsize: 100852
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2975
Raw data (stat): 2918 (minisat+) R 2917 28546 28545 0 -1 0 24621 0 0 0 119938 75 0 0 25 0 1 0 481143802 104333312 24599 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25472 24599 603 41 0 25431 0
vsize: 101888
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 2975
Raw data (stat): 2918 (minisat+) Z 2917 28546 28545 0 -1 12 24624 0 0 0 119938 79 0 0 25 0 1 0 481143802 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.18
CPU user time (s): 1199.38
CPU system time (s): 0.798878
CPU usage (%): 100.009
Max. virtual memory (Kb): 101888
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####