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/frb59-26-opb/normalized-frb59-26-5.opb
MD5SUM	a5354df485c2b6c1695d0d26c0cdb212
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-42
Optimality of the best value was proved	NO
Number of terms in the objective function	1534
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	1534
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	1534
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.13
Number of variables	1534
Total number of constraints	125982
Number of constraints which are clauses	125982
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 5063

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        856184 kB
Buffers:         40032 kB
Cached:         113920 kB
SwapCached:          0 kB
Active:         109384 kB
Inactive:        47688 kB
HighTotal:      131008 kB
HighFree:        24388 kB
LowTotal:       903652 kB
LowFree:        831796 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           7196 kB
Slab:            15720 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:12:00 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 3173 7 1200.28 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 125982 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 |  125982   251964 |   41994       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:85954     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  216721   464825 |   72240       0        0     nan |  0.000 % |
c |       100 |  215959   463222 |   79464      65      492     7.6 |  0.688 % |
c |       250 |  215163   461534 |   87410     185     1565     8.5 |  1.408 % |
c |       475 |  214472   460051 |   96151     367     3201     8.7 |  2.048 % |
c |       812 |  213299   457504 |  105766     663     6213     9.4 |  3.198 % |
c |      1318 |  210803   452048 |  116343    1052    10471    10.0 |  5.545 % |
c |      2078 |  206899   443392 |  127977    1632    16581    10.2 |  9.378 % |
c |      3217 |  199960   427819 |  140775    2503    25519    10.2 | 16.335 % |
c |      4925 |  192015   409778 |  154852    3695    39888    10.8 | 24.503 % |
c |      7488 |  180386   383175 |  170338    5442    62629    11.5 | 36.510 % |
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 |      9101 |  174218   369045 |   58072    6524    77488    11.9 | 36.510 % |
c |      9201 |  173612   367663 |   63879    6598    78260    11.9 | 43.746 % |
c |      9352 |  172254   364438 |   70267    6634    78701    11.9 | 45.220 % |
c |      9577 |  171126   361800 |   77293    6770    80672    11.9 | 46.408 % |
c |      9915 |  170107   359398 |   85023    7035    83170    11.8 | 47.468 % |
c |     10421 |  168416   355375 |   93525    7369    86547    11.7 | 49.288 % |
c |     11180 |  166329   350476 |  102878    7889    92417    11.7 | 51.500 % |
c |     12319 |  162134   340596 |  113165    8719   103213    11.8 | 56.044 % |
c |     14027 |  157622   329892 |  124482    9863   120023    12.2 | 60.978 % |
c |     16590 |  154141   321594 |  136930   11740   143012    12.2 | 64.795 % |
c |     20434 |  148827   308955 |  150623   14218   196223    13.8 | 70.642 % |
c |     26201 |  143510   296212 |  165686   18448   300139    16.3 | 76.485 % |
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 |     26706 |  143396   295898 |   47798   18911   307260    16.2 | 76.485 % |
c |     26807 |  143365   295823 |   52577   19010   309012    16.3 | 76.650 % |
c |     26957 |  143346   295776 |   57835   19153   311224    16.2 | 76.673 % |
c |     27182 |  143346   295776 |   63619   19378   315135    16.3 | 76.673 % |
c |     27519 |  143147   295303 |   69981   19597   320396    16.3 | 76.894 % |
c |     28026 |  143091   295163 |   76979   20091   335810    16.7 | 76.962 % |
c |     28786 |  142405   293484 |   84677   20635   354173    17.2 | 77.752 % |
c |     29925 |  142052   292643 |   93144   21385   377394    17.6 | 78.191 % |
c |     31633 |  141301   290830 |  102459   22900   434457    19.0 | 78.986 % |
c ==============================================================================
c [1mFound solution: -45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32831 |  141162   290523 |   47054   23957   491822    20.5 | 78.986 % |
c |     32932 |  140811   289673 |   51759   23932   490747    20.5 | 79.557 % |
c |     33082 |  140811   289673 |   56935   24082   494759    20.5 | 79.557 % |
c |     33307 |  140758   289546 |   62628   24212   497422    20.5 | 79.617 % |
c |     33644 |  140708   289438 |   68891   24539   505279    20.6 | 79.664 % |
c |     34150 |  140708   289438 |   75780   25045   526109    21.0 | 79.664 % |
c ==============================================================================
c [1mFound solution: -47[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 |     34585 |  140706   289496 |   46902   25409   545666    21.5 | 79.664 % |
c |     34685 |  140631   289325 |   51592   25488   547741    21.5 | 79.790 % |
c |     34835 |  140502   289012 |   56751   25504   551262    21.6 | 79.937 % |
c |     35060 |  140402   288768 |   62426   25617   555828    21.7 | 80.050 % |
c |     35397 |  140196   288258 |   68669   25847   566341    21.9 | 80.291 % |
c |     35903 |  139974   287726 |   75536   26221   579362    22.1 | 80.531 % |
c |     36662 |  139868   287454 |   83089   26872   608330    22.6 | 80.663 % |
c |     37801 |  139004   285361 |   91398   27413   642062    23.4 | 81.628 % |
c |     39510 |  138731   284704 |  100538   28798   697757    24.2 | 81.934 % |
c |     42072 |  138129   283247 |  110592   30903   807101    26.1 | 82.604 % |
c |     45917 |  137418   281505 |  121651   33977   991265    29.2 | 83.419 % |
c ==============================================================================
c [1mFound solution: -48[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 |     50963 |  136707   279714 |   45569   38071  1355297    35.6 | 83.419 % |
c |     51064 |  136665   279612 |   50125   38151  1356275    35.6 | 84.305 % |
c |     51214 |  136633   279530 |   55138   38260  1360588    35.6 | 84.344 % |
c |     51440 |  136573   279388 |   60652   38306  1366438    35.7 | 84.410 % |
c |     51777 |  136483   279176 |   66717   38425  1384832    36.0 | 84.508 % |
c |     52284 |  136441   279076 |   73389   38870  1410855    36.3 | 84.555 % |
c |     53044 |  136283   278706 |   80728   39261  1464008    37.3 | 84.726 % |
c |     54183 |  136243   278610 |   88801   40352  1545061    38.3 | 84.771 % |
c |     55891 |  136190   278485 |   97681   41887  1699101    40.6 | 84.827 % |
c |     58453 |  136091   278234 |  107449   44175  1922681    43.5 | 84.946 % |
c |     62297 |  136041   278108 |  118194   47904  2464514    51.4 | 85.006 % |
c |     68063 |  135763   277417 |  130013   53108  3155017    59.4 | 85.333 % |
c ==============================================================================
c [1mFound solution: -49[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 |     72442 |  135783   277482 |   45261   57408  3652183    63.6 | 85.333 % |
c |     72542 |  135783   277482 |   49787   57508  3657004    63.6 | 85.319 % |
c |     72693 |  135749   277402 |   54765   57629  3661230    63.5 | 85.356 % |
c |     72918 |  135744   277391 |   60242   57848  3671369    63.5 | 85.361 % |
c |     73256 |  135732   277365 |   66266   58171  3703940    63.7 | 85.372 % |
c |     73763 |  135695   277274 |   72893   58562  3756826    64.2 | 85.416 % |
c |     74522 |  135611   277064 |   80182   59191  3786127    64.0 | 85.514 % |
c |     75662 |  135611   277064 |   88200   60331  3934420    65.2 | 85.514 % |
c |     77370 |  135597   277030 |   97020   62037  4154789    67.0 | 85.530 % |
c ==============================================================================
c [1mFound solution: -50[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 |     78950 |  135575   276913 |   45191   62522  4231397    67.7 | 85.530 % |
c |     79050 |  135532   276799 |   49710   62546  4231449    67.7 | 85.609 % |
c |     79200 |  135532   276799 |   54681   62696  4238985    67.6 | 85.609 % |
c |     79425 |  135529   276792 |   60149   62920  4255939    67.6 | 85.613 % |
c |     79762 |  135529   276792 |   66164   63257  4304084    68.0 | 85.613 % |
c |     80270 |  135529   276792 |   72780   63765  4359392    68.4 | 85.613 % |
c |     81029 |  135444   276590 |   80058   64283  4405638    68.5 | 85.704 % |
c |     82168 |  135444   276590 |   88064   65422  4514282    69.0 | 85.704 % |
c ==============================================================================
c [1mFound solution: -51[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 |     82761 |  135475   276684 |   45158   66015  4553481    69.0 | 85.704 % |
c |     82861 |  135465   276660 |   49673   66081  4556332    69.0 | 85.710 % |
c |     83011 |  135465   276660 |   54641   66231  4565254    68.9 | 85.710 % |
c |     83236 |  135465   276660 |   60105   66456  4570299    68.8 | 85.710 % |
c |     83573 |  135465   276660 |   66115   66793  4594919    68.8 | 85.710 % |
c |     84079 |  135342   276354 |   72727   67152  4631108    69.0 | 85.848 % |
c |     84839 |  135228   276086 |   80000   67812  4691309    69.2 | 85.972 % |
c |     85979 |  135203   276023 |   88000   68603  4777095    69.6 | 86.003 % |
c |     87687 |  135029   275598 |   96800   69732  4907965    70.4 | 86.203 % |
c |     90249 |  135029   275598 |  106480   72294  5274639    73.0 | 86.203 % |
c |     94093 |  134944   275390 |  117128   75951  5693190    75.0 | 86.301 % |
c |     99859 |  134883   275249 |  128841   81592  6421159    78.7 | 86.366 % |
c |    108508 |  134835   275135 |  141725   90163  7860535    87.2 | 86.419 % |
c |    121482 |  134799   275042 |  155897  102952  9664105    93.9 | 86.462 % |
c |    140943 |  134747   274910 |  171487  122344 13291931   108.6 | 86.526 % |
c |    170136 |  134672   274727 |  188636  151088 19209599   127.1 | 86.613 % |
c ==============================================================================
c [1mFound solution: -52[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 |    186163 |  134612   274561 |   44870  165904 21520868   129.7 | 86.613 % |
c |    186263 |  134612   274561 |   49357   25515  2207333    86.5 | 86.684 % |
c |    186414 |  134601   274534 |   54292   25642  2217650    86.5 | 86.697 % |
c |    186639 |  134601   274534 |   59721   25867  2241685    86.7 | 86.697 % |
c |    186976 |  134524   274345 |   65694   26124  2249912    86.1 | 86.787 % |
c |    187482 |  134420   274095 |   72263   26616  2278339    85.6 | 86.903 % |
c |    188241 |  134420   274095 |   79489   27375  2319156    84.7 | 86.903 % |
c |    189380 |  134420   274095 |   87438   28514  2435373    85.4 | 86.903 % |
c |    191088 |  134420   274095 |   96182   30222  2600030    86.0 | 86.903 % |
c |    193650 |  134417   274088 |  105801   32781  3007387    91.7 | 86.906 % |
c |    197495 |  134364   273965 |  116381   36616  3563866    97.3 | 86.962 % |
c |    203261 |  134364   273965 |  128019   42382  4293921   101.3 | 86.962 % |
c |    211910 |  134328   273873 |  140821   51012  5544856   108.7 | 87.005 % |
c |    224884 |  134328   273873 |  154903   63986  7907749   123.6 | 87.005 % |
c |    244345 |  134328   273873 |  170393   83447 11620820   139.3 | 87.005 % |
c ==============================================================================
c [1mFound solution: -53[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 |    251911 |  134341   273909 |   44780   90983 12874260   141.5 | 87.005 % |
c |    252011 |  134341   273909 |   49258   91083 12879997   141.4 | 87.002 % |
c |    252162 |  134341   273909 |   54183   91234 12893752   141.3 | 87.002 % |
c |    252387 |  134341   273909 |   59602   91459 12918345   141.2 | 87.002 % |
c |    252725 |  134341   273909 |   65562   91797 12950424   141.1 | 87.002 % |
c |    253231 |  134337   273899 |   72118   92302 12995661   140.8 | 87.007 % |
c |    253991 |  134323   273863 |   79330   93028 13081442   140.6 | 87.025 % |
c |    255130 |  134323   273863 |   87263   94167 13274461   141.0 | 87.025 % |
c |    256838 |  134323   273863 |   95989   95875 13445425   140.2 | 87.025 % |
c |    259400 |  134283   273763 |  105588   98400 13873992   141.0 | 87.073 % |
c |    263244 |  134283   273763 |  116147  102244 14537960   142.2 | 87.073 % |
c |    269010 |  134283   273763 |  127762  108010 15238191   141.1 | 87.073 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1534 -C1533 -C1532 -C1531 -C1530 -C1529 -C1528 -C1527 -C1526 -C1525 -C1524 -C1523 -C1522 -C1521 -C1520 -C1519 C1518 -C1517 -C1516 -C1515 -C1514 -C1513 -C1512 -C1511 -C1510 -C1509 -C1508 -C1507 -C1506 C1505 -C1504 -C1503 -C1502 -C1501 -C1500 -C1499 -C1498 -C1497 -C1496 -C1495 -C1494 -C1493 -C1492 -C1491 -C1490 -C1489 -C1488 -C1487 -C1486 -C1485 -C1484 -C1483 -C1482 -C1481 -C1480 -C1479 -C1478 -C1477 -C1476 -C1475 -C1474 -C1473 -C1472 -C1471 -C1470 -C1469 -C1468 -C1467 -C1466 -C1465 -C1464 -C1463 -C1462 -C1461 -C1460 -C1459 C1458 -C1457 -C1456 -C1455 -C1454 -C1453 -C1452 -C1451 -C1450 -C1449 -C1448 -C1447 -C1446 -C1445 -C1444 C1443 -C1442 -C1441 -C1440 -C1439 -C1438 -C1437 -C1436 -C1435 -C1434 -C1433 -C1432 -C1431 -C1430 -C1429 -C1428 -C1427 -C1426 -C1425 -C1424 -C1423 -C1422 -C1421 -C1420 -C1419 -C1418 -C1417 -C1416 -C1415 C1414 -C1413 -C1412 -C1411 -C1410 -C1409 -C1408 -C1407 -C1406 -C1405 -C1404 -C1403 -C1402 -C1401 -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 -C1386 -C1385 -C1384 C1383 -C1382 -C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 -C1361 -C1360 -C1359 -C1358 -C1357 C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 C1338 -C1337 -C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 -C1327 -C1326 -C1325 -C1324 -C1323 -C1322 C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 C1292 -C1291 -C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 -C1280 -C1279 -C1278 -C1277 -C1276 -C1275 -C1274 -C1273 C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -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 -C495 -C494 -C493 -C492 -C491 C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 C264 -C263 -C262 -C261 -C260 -C259 -C258#### 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.95 0.90 2/56 15564
Raw data (stat): 15564 (runsolver) R 15563 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 364257199 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9999 s]
Raw data (loadavg): 0.93 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 6916 0 0 0 977 22 0 0 25 0 1 0 364257199 30363648 6894 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7413 6894 603 41 0 7372 0
vsize: 29652
[startup+19.9996 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 6926 0 0 0 1977 22 0 0 25 0 1 0 364257199 30502912 6904 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7447 6904 603 41 0 7406 0
vsize: 29788
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 6931 0 0 0 2977 22 0 0 25 0 1 0 364257199 30502912 6909 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7447 6909 603 41 0 7406 0
vsize: 29788
[startup+40.0006 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 6937 0 0 0 3976 22 0 0 25 0 1 0 364257199 30502912 6915 4294967295 134512640 134672761 3221224640 3221223820 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7447 6915 603 41 0 7406 0
vsize: 29788
[startup+50.001 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 6942 0 0 0 4976 22 0 0 25 0 1 0 364257199 30502912 6920 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7447 6920 603 41 0 7406 0
vsize: 29788
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 6948 0 0 0 5976 22 0 0 25 0 1 0 364257199 30502912 6926 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7447 6926 603 41 0 7406 0
vsize: 29788
[startup+70.0004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 6956 0 0 0 6976 23 0 0 25 0 1 0 364257199 30638080 6934 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7480 6934 603 41 0 7439 0
vsize: 29920
[startup+80.0014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 6962 0 0 0 7976 23 0 0 25 0 1 0 364257199 30638080 6940 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7480 6940 603 41 0 7439 0
vsize: 29920
[startup+90.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 6969 0 0 0 8976 23 0 0 25 0 1 0 364257199 30638080 6947 4294967295 134512640 134672761 3221224640 3221223832 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7480 6947 603 41 0 7439 0
vsize: 29920
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7211 0 0 0 9975 24 0 0 25 0 1 0 364257199 32071680 7189 4294967295 134512640 134672761 3221224640 3221223812 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7830 7189 603 41 0 7789 0
vsize: 31320
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7212 0 0 0 10975 24 0 0 25 0 1 0 364257199 32071680 7190 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7830 7190 603 41 0 7789 0
vsize: 31320
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7212 0 0 0 11976 24 0 0 25 0 1 0 364257199 32071680 7190 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7830 7190 603 41 0 7789 0
vsize: 31320
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7212 0 0 0 12976 24 0 0 25 0 1 0 364257199 32071680 7190 4294967295 134512640 134672761 3221224640 3221223812 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7830 7190 603 41 0 7789 0
vsize: 31320
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7212 0 0 0 13976 24 0 0 25 0 1 0 364257199 32071680 7190 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7830 7190 603 41 0 7789 0
vsize: 31320
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7212 0 0 0 14976 24 0 0 25 0 1 0 364257199 32071680 7190 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7830 7190 603 41 0 7789 0
vsize: 31320
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7212 0 0 0 15976 24 0 0 25 0 1 0 364257199 32071680 7190 4294967295 134512640 134672761 3221224640 3221223812 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7830 7190 603 41 0 7789 0
vsize: 31320
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7266 0 0 0 16976 24 0 0 25 0 1 0 364257199 32342016 7244 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7896 7244 603 41 0 7855 0
vsize: 31584
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7402 0 0 0 17975 25 0 0 25 0 1 0 364257199 32833536 7347 4294967295 134512640 134672761 3221224640 3221223840 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8016 7347 603 41 0 7975 0
vsize: 32064
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7624 0 0 0 18975 25 0 0 25 0 1 0 364257199 33566720 7537 4294967295 134512640 134672761 3221224640 3221223812 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8195 7537 603 41 0 8154 0
vsize: 32780
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 7796 0 0 0 19975 26 0 0 25 0 1 0 364257199 34107392 7677 4294967295 134512640 134672761 3221224640 3221223812 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8327 7677 603 41 0 8286 0
vsize: 33308
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 8029 0 0 0 20974 27 0 0 25 0 1 0 364257199 35053568 7910 4294967295 134512640 134672761 3221224640 3221223836 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8558 7910 603 41 0 8517 0
vsize: 34232
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 8287 0 0 0 21973 28 0 0 25 0 1 0 364257199 36257792 8168 4294967295 134512640 134672761 3221224640 3221223828 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8852 8168 603 41 0 8811 0
vsize: 35408
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 8694 0 0 0 22971 29 0 0 25 0 1 0 364257199 37670912 8542 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9197 8542 603 41 0 9156 0
vsize: 36788
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 8991 0 0 0 23970 31 0 0 25 0 1 0 364257199 38883328 8839 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9493 8839 603 41 0 9452 0
vsize: 37972
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15564
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 9495 0 0 0 24969 32 0 0 25 0 1 0 364257199 41029632 9343 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10017 9343 603 41 0 9976 0
vsize: 40068
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 10068 0 0 0 25968 34 0 0 25 0 1 0 364257199 43319296 9916 4294967295 134512640 134672761 3221224640 3221223812 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10576 9916 603 41 0 10535 0
vsize: 42304
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 10485 0 0 0 26967 35 0 0 25 0 1 0 364257199 45068288 10333 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11003 10333 603 41 0 10962 0
vsize: 44012
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 10976 0 0 0 27966 36 0 0 25 0 1 0 364257199 47075328 10824 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11493 10824 603 41 0 11452 0
vsize: 45972
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 11325 0 0 0 28965 37 0 0 25 0 1 0 364257199 48271360 11140 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11785 11140 603 41 0 11744 0
vsize: 47140
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 11761 0 0 0 29964 38 0 0 25 0 1 0 364257199 50016256 11576 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12211 11576 603 41 0 12170 0
vsize: 48844
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 12108 0 0 0 30963 39 0 0 25 0 1 0 364257199 51286016 11891 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12521 11891 603 41 0 12480 0
vsize: 50084
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 12296 0 0 0 31963 39 0 0 25 0 1 0 364257199 52236288 12046 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12753 12046 603 41 0 12712 0
vsize: 51012
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 12524 0 0 0 32962 40 0 0 25 0 1 0 364257199 53170176 12274 4294967295 134512640 134672761 3221224640 3221223824 134559609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12981 12274 603 41 0 12940 0
vsize: 51924
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 12856 0 0 0 33961 41 0 0 25 0 1 0 364257199 54509568 12606 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13308 12606 603 41 0 13267 0
vsize: 53232
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 13247 0 0 0 34961 42 0 0 25 0 1 0 364257199 56119296 12997 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13701 12997 603 41 0 13660 0
vsize: 54804
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 13611 0 0 0 35960 43 0 0 25 0 1 0 364257199 57597952 13361 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14062 13361 603 41 0 14021 0
vsize: 56248
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 13974 0 0 0 36959 44 0 0 25 0 1 0 364257199 59064320 13724 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14420 13724 603 41 0 14379 0
vsize: 57680
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 14348 0 0 0 37958 45 0 0 25 0 1 0 364257199 60534784 14098 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14779 14098 603 41 0 14738 0
vsize: 59116
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 14704 0 0 0 38957 46 0 0 25 0 1 0 364257199 62017536 14454 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15141 14454 603 41 0 15100 0
vsize: 60564
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 15164 0 0 0 39956 48 0 0 25 0 1 0 364257199 63889408 14914 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15598 14914 603 41 0 15557 0
vsize: 62392
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 15674 0 0 0 40954 50 0 0 25 0 1 0 364257199 66011136 15424 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16116 15424 603 41 0 16075 0
vsize: 64464
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 16083 0 0 0 41953 51 0 0 25 0 1 0 364257199 67620864 15833 4294967295 134512640 134672761 3221224640 3221223808 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16509 15833 603 41 0 16468 0
vsize: 66036
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 16469 0 0 0 42951 53 0 0 25 0 1 0 364257199 69230592 16219 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16902 16219 603 41 0 16861 0
vsize: 67608
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 16783 0 0 0 43950 54 0 0 25 0 1 0 364257199 70443008 16533 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17198 16533 603 41 0 17157 0
vsize: 68792
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 17086 0 0 0 44949 56 0 0 25 0 1 0 364257199 71786496 16836 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17526 16836 603 41 0 17485 0
vsize: 70104
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 17488 0 0 0 45948 57 0 0 25 0 1 0 364257199 73400320 17238 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17920 17239 603 41 0 17879 0
vsize: 71680
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 17831 0 0 0 46947 58 0 0 25 0 1 0 364257199 74739712 17581 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18247 17581 603 41 0 18206 0
vsize: 72988
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15566
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 18238 0 0 0 47946 59 0 0 25 0 1 0 364257199 76480512 17988 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18672 17988 603 41 0 18631 0
vsize: 74688
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15619
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 18676 0 0 0 48945 60 0 0 25 0 1 0 364257199 78217216 18426 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18426 603 41 0 19055 0
vsize: 76384
[startup+500.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15619
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 19142 0 0 0 49949 61 0 0 25 0 1 0 364257199 80089088 18892 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19553 18892 603 41 0 19512 0
vsize: 78212
[startup+510.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15619
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 19417 0 0 0 50948 62 0 0 25 0 1 0 364257199 81166336 19167 4294967295 134512640 134672761 3221224640 3221223812 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19816 19167 603 41 0 19775 0
vsize: 79264
[startup+520.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15619
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 19746 0 0 0 51948 62 0 0 25 0 1 0 364257199 82505728 19496 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20143 19496 603 41 0 20102 0
vsize: 80572
[startup+530.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15619
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 20131 0 0 0 52947 63 0 0 25 0 1 0 364257199 84123648 19881 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20538 19881 603 41 0 20497 0
vsize: 82152
[startup+540.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15619
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 20503 0 0 0 53947 64 0 0 25 0 1 0 364257199 85598208 20253 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20898 20253 603 41 0 20857 0
vsize: 83592
[startup+550.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15621
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 20871 0 0 0 54945 66 0 0 25 0 1 0 364257199 87203840 20621 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21290 20621 603 41 0 21249 0
vsize: 85160
[startup+560.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 21231 0 0 0 55944 66 0 0 25 0 1 0 364257199 88666112 20981 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21647 20981 603 41 0 21606 0
vsize: 86588
[startup+570.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 21549 0 0 0 56943 68 0 0 25 0 1 0 364257199 89874432 21299 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21942 21299 603 41 0 21901 0
vsize: 87768
[startup+580.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 21800 0 0 0 57943 68 0 0 25 0 1 0 364257199 90935296 21550 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22201 21550 603 41 0 22160 0
vsize: 88804
[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 22169 0 0 0 58942 69 0 0 25 0 1 0 364257199 92401664 21919 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22559 21919 603 41 0 22518 0
vsize: 90236
[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 22542 0 0 0 59941 70 0 0 25 0 1 0 364257199 93999104 22292 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22949 22292 603 41 0 22908 0
vsize: 91796
[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 22956 0 0 0 60941 71 0 0 25 0 1 0 364257199 95600640 22706 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23340 22706 603 41 0 23299 0
vsize: 93360
[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 23309 0 0 0 61940 71 0 0 25 0 1 0 364257199 97583104 23059 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23824 23059 603 41 0 23783 0
vsize: 95296
[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 23675 0 0 0 62939 73 0 0 25 0 1 0 364257199 99172352 23425 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24212 23425 603 41 0 24171 0
vsize: 96848
[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 24042 0 0 0 63938 74 0 0 25 0 1 0 364257199 100634624 23792 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24569 23792 603 41 0 24528 0
vsize: 98276
[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 24392 0 0 0 64938 75 0 0 25 0 1 0 364257199 101974016 24142 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24896 24142 603 41 0 24855 0
vsize: 99584
[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 24686 0 0 0 65937 76 0 0 25 0 1 0 364257199 103174144 24436 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25189 24436 603 41 0 25148 0
vsize: 100756
[startup+670.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 24995 0 0 0 66936 77 0 0 25 0 1 0 364257199 104513536 24745 4294967295 134512640 134672761 3221224640 3221223744 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25516 24745 603 41 0 25475 0
vsize: 102064
[startup+680.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 25328 0 0 0 67935 77 0 0 25 0 1 0 364257199 105848832 25078 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25842 25078 603 41 0 25801 0
vsize: 103368
[startup+690.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 25599 0 0 0 68935 78 0 0 25 0 1 0 364257199 106913792 25349 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26102 25349 603 41 0 26061 0
vsize: 104408
[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 25914 0 0 0 69935 78 0 0 25 0 1 0 364257199 108240896 25664 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26426 25664 603 41 0 26385 0
vsize: 105704
[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 26247 0 0 0 70934 79 0 0 25 0 1 0 364257199 109572096 25997 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26751 25997 603 41 0 26710 0
vsize: 107004
[startup+720.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 26586 0 0 0 71933 80 0 0 25 0 1 0 364257199 111026176 26336 4294967295 134512640 134672761 3221224640 3221223824 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27106 26336 603 41 0 27065 0
vsize: 108424
[startup+730.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 26833 0 0 0 72933 81 0 0 25 0 1 0 364257199 111960064 26583 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27334 26583 603 41 0 27293 0
vsize: 109336
[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 27021 0 0 0 73932 82 0 0 25 0 1 0 364257199 112754688 26771 4294967295 134512640 134672761 3221224640 3221223812 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27528 26771 603 41 0 27487 0
vsize: 110112
[startup+750.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 27228 0 0 0 74932 82 0 0 25 0 1 0 364257199 113561600 26978 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27725 26978 603 41 0 27684 0
vsize: 110900
[startup+760.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 27485 0 0 0 75931 83 0 0 25 0 1 0 364257199 114626560 27235 4294967295 134512640 134672761 3221224640 3221223708 1075346562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27985 27235 603 41 0 27944 0
vsize: 111940
[startup+770.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 27750 0 0 0 76930 84 0 0 25 0 1 0 364257199 115695616 27500 4294967295 134512640 134672761 3221224640 3221223744 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28246 27500 603 41 0 28205 0
vsize: 112984
[startup+780.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 28020 0 0 0 77929 85 0 0 25 0 1 0 364257199 116764672 27770 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28507 27770 603 41 0 28466 0
vsize: 114028
[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 28192 0 0 0 78929 85 0 0 25 0 1 0 364257199 117575680 27942 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28705 27942 603 41 0 28664 0
vsize: 114820
[startup+800.056 s]
Raw data (loadavg): 0.99 0.97 0.91 3/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 28460 0 0 0 79928 86 0 0 25 0 1 0 364257199 118657024 28210 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28969 28210 603 41 0 28928 0
vsize: 115876
[startup+810.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 28699 0 0 0 80928 87 0 0 25 0 1 0 364257199 119595008 28449 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29198 28449 603 41 0 29157 0
vsize: 116792
[startup+820.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 28964 0 0 0 81927 87 0 0 25 0 1 0 364257199 120680448 28714 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29463 28714 603 41 0 29422 0
vsize: 117852
[startup+830.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 29259 0 0 0 82927 88 0 0 25 0 1 0 364257199 121892864 29009 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29759 29009 603 41 0 29718 0
vsize: 119036
[startup+840.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 29597 0 0 0 83926 89 0 0 25 0 1 0 364257199 123228160 29347 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30085 29347 603 41 0 30044 0
vsize: 120340
[startup+850.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15625
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 29931 0 0 0 84925 90 0 0 25 0 1 0 364257199 124571648 29681 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30413 29681 603 41 0 30372 0
vsize: 121652
[startup+860.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30188 0 0 0 85925 91 0 0 25 0 1 0 364257199 125640704 29938 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30674 29938 603 41 0 30633 0
vsize: 122696
[startup+870.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 86924 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+880.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 87924 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+890.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 88924 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+900.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 89924 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+910.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 90924 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+920.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 91925 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223744 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+930.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 92925 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+940.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 93925 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+950.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 94925 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+960.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 95925 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+970.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 96925 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+980.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 97926 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+990.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 98926 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 99926 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 100926 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 101926 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 102926 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 103927 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 104927 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 105927 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 106927 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 107927 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 108927 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 109928 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 110928 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 111928 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 112928 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223812 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 113928 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15627
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 114928 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15629
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 115929 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223776 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15629
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 116929 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15629
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 117929 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15629
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 118929 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 15629
Raw data (stat): 15564 (minisat+) R 15563 12452 12451 0 -1 0 30364 0 0 0 119929 92 0 0 25 0 1 0 364257199 126189568 30083 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 30083 603 41 0 30767 0
vsize: 123232
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 15629
Raw data (stat): 15564 (minisat+) Z 15563 12452 12451 0 -1 12 30367 0 0 0 119930 98 0 0 25 0 1 0 364257199 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.12
CPU time (s): 1200.28
CPU user time (s): 1199.3
CPU system time (s): 0.98085
CPU usage (%): 100.014
Max. virtual memory (Kb): 123232
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####