PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-4.opb
MD5SUM	b85a90571dde4fe12541342d5605d680
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-37
Optimality of the best value was proved	NO
Number of terms in the objective function	1150
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1150
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1150
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.1
Number of variables	1150
Total number of constraints	80258
Number of constraints which are clauses	80258
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 5046

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-13 21:36:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3029 boxname=wulflinc13 idbench=337 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b85a90571dde4fe12541342d5605d680  /oldhome/oroussel/tmp/wulflinc13/normalized-frb50-23-4.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-frb50-23-4.opb
IDLAUNCH: 3029
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        919084 kB
Buffers:         34208 kB
Cached:          61280 kB
SwapCached:        392 kB
Active:          53088 kB
Inactive:        45708 kB
HighTotal:      131008 kB
HighFree:        65744 kB
LowTotal:       903652 kB
LowFree:        853340 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11220 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:56:13 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3029 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80258 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 |   80258   160516 |   26752       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  148144   319772 |   49381       0        0     nan |  0.000 % |
c |       100 |  147820   319103 |   54319      84      567     6.8 |  0.388 % |
c |       250 |  147145   317664 |   59751     188     1432     7.6 |  1.214 % |
c |       476 |  146024   315267 |   65726     361     3068     8.5 |  2.595 % |
c |       813 |  143729   310234 |   72298     619     5841     9.4 |  5.557 % |
c |      1319 |  140833   303816 |   79528     968     9121     9.4 |  9.437 % |
c |      2079 |  136692   294527 |   87481    1586    15869    10.0 | 15.004 % |
c |      3218 |  131314   282313 |   96229    2417    27902    11.5 | 22.323 % |
c |      4926 |  122752   262701 |  105852    3528    39936    11.3 | 34.222 % |
c |      7488 |  112044   237857 |  116437    5289    62605    11.8 | 49.090 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7928 |  111198   235994 |   37066    5633    66805    11.9 | 49.090 % |
c |      8028 |  110897   235287 |   40772    5710    67536    11.8 | 50.901 % |
c |      8178 |  110452   234225 |   44849    5792    68387    11.8 | 51.548 % |
c |      8403 |  109585   232234 |   49334    5952    71118    11.9 | 52.759 % |
c |      8741 |  108728   230226 |   54268    6208    74433    12.0 | 53.995 % |
c |      9247 |  107763   227961 |   59695    6556    79030    12.1 | 55.393 % |
c |     10006 |  106198   224277 |   65664    7058    87476    12.4 | 57.665 % |
c |     11146 |  103552   218006 |   72231    7914   103965    13.1 | 61.514 % |
c |     12854 |  100400   210497 |   79454    9088   124554    13.7 | 66.138 % |
c |     15416 |   97019   202392 |   87399   10804   161729    15.0 | 71.090 % |
c |     19260 |   94852   197144 |   96139   14054   253306    18.0 | 74.363 % |
c |     25026 |   93592   194098 |  105753   19178   576284    30.0 | 76.268 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29121 |   92780   192183 |   30926   22895   940622    41.1 | 76.268 % |
c |     29221 |   92677   191930 |   34018   22961   941837    41.0 | 77.647 % |
c |     29371 |   92612   191776 |   37420   23105   945249    40.9 | 77.742 % |
c |     29597 |   92612   191776 |   41162   23331   954744    40.9 | 77.742 % |
c |     29934 |   92495   191494 |   45278   23662   962311    40.7 | 77.917 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30329 |   92131   190575 |   30710   23891   984433    41.2 | 77.917 % |
c |     30429 |   92064   190426 |   33781   23974   986115    41.1 | 78.509 % |
c |     30579 |   91949   190146 |   37159   24115   994438    41.2 | 78.683 % |
c |     30804 |   91850   189911 |   40875   24280  1003798    41.3 | 78.828 % |
c |     31141 |   91766   189701 |   44962   24546  1013462    41.3 | 78.962 % |
c |     31647 |   91650   189414 |   49458   25021  1032977    41.3 | 79.143 % |
c |     32406 |   91601   189300 |   54404   25733  1089814    42.4 | 79.212 % |
c |     33545 |   91498   189059 |   59845   26813  1189985    44.4 | 79.358 % |
c |     35253 |   91064   187999 |   65829   28271  1265964    44.8 | 80.005 % |
c |     37817 |   90592   186879 |   72412   30523  1417125    46.4 | 80.691 % |
c |     41661 |   90247   186028 |   79653   34043  1688146    49.6 | 81.219 % |
c |     47427 |   89873   185101 |   87619   39490  2309222    58.5 | 81.806 % |
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 |     55522 |   89822   185003 |   29940   47545  3314007    69.7 | 81.806 % |
c |     55622 |   89822   185003 |   32934   47645  3321718    69.7 | 81.930 % |
c |     55772 |   89822   185003 |   36227   47795  3326427    69.6 | 81.931 % |
c |     55998 |   89822   185003 |   39850   48021  3341366    69.6 | 81.930 % |
c |     56336 |   89822   185003 |   43835   48359  3370021    69.7 | 81.931 % |
c |     56842 |   89822   185003 |   48218   48865  3409651    69.8 | 81.930 % |
c |     57601 |   89177   183450 |   53040   48863  3434237    70.3 | 82.894 % |
c |     58740 |   89177   183450 |   58344   50002  3579676    71.6 | 82.894 % |
c |     60448 |   89117   183296 |   64179   51669  3732132    72.2 | 82.996 % |
c |     63011 |   89039   183106 |   70596   54124  3965144    73.3 | 83.114 % |
c |     66855 |   89039   183106 |   77656   57968  4599226    79.3 | 83.114 % |
c |     72622 |   88752   182402 |   85422   63069  5112366    81.1 | 83.557 % |
c |     81271 |   88748   182392 |   93964   71717  6426102    89.6 | 83.564 % |
c |     94245 |   88748   182392 |  103361   84691  8009047    94.6 | 83.564 % |
c |    113707 |   88741   182375 |  113697  104135 11319413   108.7 | 83.574 % |
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 |    140871 |   88488   181720 |   29496  130980 15028721   114.7 | 83.574 % |
c |    140971 |   88488   181720 |   32445   23657  1604034    67.8 | 83.975 % |
c |    141121 |   88488   181720 |   35690   23807  1613264    67.8 | 83.975 % |
c |    141346 |   88488   181720 |   39259   24032  1631251    67.9 | 83.975 % |
c |    141683 |   88328   181322 |   43185   24359  1642586    67.4 | 84.221 % |
c |    142189 |   88328   181322 |   47503   24865  1700627    68.4 | 84.221 % |
c |    142948 |   88328   181322 |   52253   25624  1787151    69.7 | 84.221 % |
c |    144087 |   88328   181322 |   57479   26763  1947089    72.8 | 84.221 % |
c |    145797 |   88226   181078 |   63227   28458  2159705    75.9 | 84.369 % |
c |    148359 |   88221   181067 |   69550   31016  2379812    76.7 | 84.375 % |
c |    152203 |   88221   181067 |   76505   34860  2924276    83.9 | 84.375 % |
c |    157969 |   88221   181067 |   84155   40626  3769186    92.8 | 84.375 % |
c |    166618 |   88180   180970 |   92571   49077  4992109   101.7 | 84.436 % |
c |    179592 |   88139   180873 |  101828   61925  6663510   107.6 | 84.496 % |
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 |    193053 |   88160   180935 |   29386   75386  9039640   119.9 | 84.496 % |
c |    193153 |   88154   180921 |   32324   20076  2226072   110.9 | 84.484 % |
c |    193303 |   88149   180908 |   35557   20222  2233119   110.4 | 84.492 % |
c |    193528 |   88149   180908 |   39112   20447  2240695   109.6 | 84.492 % |
c |    193865 |   87960   180457 |   43024   20704  2251356   108.7 | 84.765 % |
c |    194373 |   87960   180457 |   47326   21212  2285864   107.8 | 84.765 % |
c |    195133 |   87928   180387 |   52059   21969  2317828   105.5 | 84.806 % |
c |    196272 |   87928   180387 |   57265   23108  2390481   103.4 | 84.806 % |
c |    197981 |   87877   180262 |   62991   24808  2557155   103.1 | 84.886 % |
c |    200543 |   87877   180262 |   69290   27370  2839758   103.8 | 84.886 % |
c |    204387 |   87859   180218 |   76219   31206  3310018   106.1 | 84.914 % |
c |    210154 |   87728   179913 |   83841   36956  3914827   105.9 | 85.101 % |
c |    218803 |   87618   179642 |   92225   45444  4968749   109.3 | 85.273 % |
c |    231778 |   87612   179628 |  101448   58416  6873546   117.7 | 85.281 % |
c |    251240 |   87602   179602 |  111593   77876  9366492   120.3 | 85.299 % |
c |    280433 |   87500   179360 |  122752  106975 13247285   123.8 | 85.449 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 C4#### 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.84 0.94 0.90 2/54 1478
Raw data (stat): 1478 (runsolver) R 1477 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421020860 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 4931 0 0 0 985 14 0 0 25 0 1 0 421020860 23306240 4909 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5690 4909 603 41 0 5649 0
vsize: 22760
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 4939 0 0 0 1984 14 0 0 25 0 1 0 421020860 23306240 4917 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5690 4917 603 41 0 5649 0
vsize: 22760
[startup+30.0018 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 4953 0 0 0 2984 14 0 0 25 0 1 0 421020860 23306240 4931 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5690 4931 603 41 0 5649 0
vsize: 22760
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 4959 0 0 0 3983 15 0 0 25 0 1 0 421020860 23441408 4937 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5723 4937 603 41 0 5682 0
vsize: 22892
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 4971 0 0 0 4983 15 0 0 25 0 1 0 421020860 23441408 4949 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5723 4949 603 41 0 5682 0
vsize: 22892
[startup+60.0017 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 4979 0 0 0 5983 16 0 0 25 0 1 0 421020860 23441408 4957 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5723 4957 603 41 0 5682 0
vsize: 22892
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 5256 0 0 0 6982 17 0 0 25 0 1 0 421020860 25407488 5234 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6203 5234 603 41 0 6162 0
vsize: 24812
[startup+80.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 5256 0 0 0 7981 17 0 0 25 0 1 0 421020860 25407488 5234 4294967295 134512640 134672761 3221224624 3221223808 134559599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6203 5234 603 41 0 6162 0
vsize: 24812
[startup+90.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 5256 0 0 0 8981 17 0 0 25 0 1 0 421020860 25407488 5234 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6203 5234 603 41 0 6162 0
vsize: 24812
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 5560 0 0 0 9981 18 0 0 25 0 1 0 421020860 26755072 5538 4294967295 134512640 134672761 3221224624 3221223760 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6532 5538 603 41 0 6491 0
vsize: 26128
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 6075 0 0 0 10979 19 0 0 25 0 1 0 421020860 28782592 6053 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7027 6053 603 41 0 6986 0
vsize: 28108
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 6366 0 0 0 11978 20 0 0 25 0 1 0 421020860 29990912 6344 4294967295 134512640 134672761 3221224624 3221223816 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7322 6344 603 41 0 7281 0
vsize: 29288
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 6682 0 0 0 12977 22 0 0 25 0 1 0 421020860 31338496 6660 4294967295 134512640 134672761 3221224624 3221223792 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7651 6660 603 41 0 7610 0
vsize: 30604
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 7067 0 0 0 13975 24 0 0 25 0 1 0 421020860 32944128 7045 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8043 7045 603 41 0 8002 0
vsize: 32172
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 7568 0 0 0 14974 26 0 0 25 0 1 0 421020860 35090432 7546 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8567 7547 603 41 0 8526 0
vsize: 34268
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 8046 0 0 0 15972 28 0 0 25 0 1 0 421020860 36970496 8024 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9026 8024 603 41 0 8985 0
vsize: 36104
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 8566 0 0 0 16970 30 0 0 25 0 1 0 421020860 39096320 8544 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9545 8544 603 41 0 9504 0
vsize: 38180
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 8827 0 0 0 17969 31 0 0 25 0 1 0 421020860 40116224 8805 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9794 8805 603 41 0 9753 0
vsize: 39176
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 9189 0 0 0 18968 32 0 0 25 0 1 0 421020860 41586688 9167 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10153 9167 603 41 0 10112 0
vsize: 40612
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 9701 0 0 0 19967 33 0 0 25 0 1 0 421020860 43732992 9679 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10677 9679 603 41 0 10636 0
vsize: 42708
[startup+210 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 10107 0 0 0 20965 35 0 0 25 0 1 0 421020860 45334528 10085 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11068 10085 603 41 0 11027 0
vsize: 44272
[startup+220 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 10506 0 0 0 21964 36 0 0 25 0 1 0 421020860 46940160 10484 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11460 10484 603 41 0 11419 0
vsize: 45840
[startup+230.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 10919 0 0 0 22963 37 0 0 25 0 1 0 421020860 48680960 10897 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11885 10897 603 41 0 11844 0
vsize: 47540
[startup+240 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 11404 0 0 0 23961 39 0 0 25 0 1 0 421020860 50954240 11382 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12440 11382 603 41 0 12399 0
vsize: 49760
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 11850 0 0 0 24960 41 0 0 25 0 1 0 421020860 52707328 11828 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12868 11828 603 41 0 12827 0
vsize: 51472
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 12275 0 0 0 25958 42 0 0 25 0 1 0 421020860 54448128 12253 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13293 12253 603 41 0 13252 0
vsize: 53172
[startup+270 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 12659 0 0 0 26958 43 0 0 25 0 1 0 421020860 55934976 12637 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13656 12637 603 41 0 13615 0
vsize: 54624
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 13004 0 0 0 27957 44 0 0 25 0 1 0 421020860 57417728 12982 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14018 12982 603 41 0 13977 0
vsize: 56072
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 13367 0 0 0 28956 45 0 0 25 0 1 0 421020860 58888192 13345 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13345 603 41 0 14336 0
vsize: 57508
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 13733 0 0 0 29955 46 0 0 25 0 1 0 421020860 60358656 13711 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14736 13711 603 41 0 14695 0
vsize: 58944
[startup+310 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 14096 0 0 0 30954 47 0 0 25 0 1 0 421020860 61833216 14074 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15096 14074 603 41 0 15055 0
vsize: 60384
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 14476 0 0 0 31953 48 0 0 25 0 1 0 421020860 63442944 14454 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15489 14454 603 41 0 15448 0
vsize: 61956
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 14831 0 0 0 32952 50 0 0 25 0 1 0 421020860 64774144 14809 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15814 14809 603 41 0 15773 0
vsize: 63256
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 15195 0 0 0 33952 51 0 0 25 0 1 0 421020860 66367488 15173 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16203 15173 603 41 0 16162 0
vsize: 64812
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 15565 0 0 0 34950 52 0 0 25 0 1 0 421020860 67829760 15543 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16560 15543 603 41 0 16519 0
vsize: 66240
[startup+360.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 15983 0 0 0 35949 53 0 0 25 0 1 0 421020860 69558272 15961 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16982 15961 603 41 0 16941 0
vsize: 67928
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 16361 0 0 0 36948 54 0 0 25 0 1 0 421020860 71016448 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17338 16339 603 41 0 17297 0
vsize: 69352
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 16738 0 0 0 37947 55 0 0 25 0 1 0 421020860 72609792 16716 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17727 16716 603 41 0 17686 0
vsize: 70908
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 17095 0 0 0 38947 56 0 0 25 0 1 0 421020860 74080256 17073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18086 17073 603 41 0 18045 0
vsize: 72344
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 17399 0 0 0 39945 58 0 0 25 0 1 0 421020860 75292672 17377 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18382 17377 603 41 0 18341 0
vsize: 73528
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 17704 0 0 0 40944 59 0 0 25 0 1 0 421020860 76496896 17682 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18676 17682 603 41 0 18635 0
vsize: 74704
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 18037 0 0 0 41942 61 0 0 25 0 1 0 421020860 77840384 18015 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19004 18015 603 41 0 18963 0
vsize: 76016
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 18391 0 0 0 42942 62 0 0 25 0 1 0 421020860 79302656 18369 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19361 18369 603 41 0 19320 0
vsize: 77444
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 18788 0 0 0 43941 62 0 0 25 0 1 0 421020860 80916480 18766 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19755 18766 603 41 0 19714 0
vsize: 79020
[startup+450 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 19153 0 0 0 44940 63 0 0 25 0 1 0 421020860 82378752 19131 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20112 19131 603 41 0 20071 0
vsize: 80448
[startup+460 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 19461 0 0 0 45939 64 0 0 25 0 1 0 421020860 83714048 19439 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20438 19439 603 41 0 20397 0
vsize: 81752
[startup+470 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 19702 0 0 0 46938 65 0 0 25 0 1 0 421020860 84656128 19680 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20668 19681 603 41 0 20627 0
vsize: 82672
[startup+480 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 19948 0 0 0 47938 66 0 0 25 0 1 0 421020860 85725184 19926 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20929 19926 603 41 0 20888 0
vsize: 83716
[startup+490 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 20209 0 0 0 48937 67 0 0 25 0 1 0 421020860 86786048 20187 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21188 20187 603 41 0 21147 0
vsize: 84752
[startup+500 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 20461 0 0 0 49937 68 0 0 25 0 1 0 421020860 87715840 20439 4294967295 134512640 134672761 3221224624 3221223760 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21415 20439 603 41 0 21374 0
vsize: 85660
[startup+510 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 20715 0 0 0 50936 69 0 0 25 0 1 0 421020860 88780800 20693 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21675 20693 603 41 0 21634 0
vsize: 86700
[startup+520 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 20881 0 0 0 51936 69 0 0 25 0 1 0 421020860 89444352 20859 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21837 20859 603 41 0 21796 0
vsize: 87348
[startup+530 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21131 0 0 0 52935 70 0 0 25 0 1 0 421020860 90505216 21109 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22096 21109 603 41 0 22055 0
vsize: 88384
[startup+540 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 53934 70 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+550 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 54934 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+560.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 55934 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+570 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 56934 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+580 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 57934 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+590 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 58935 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+599.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 59935 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+609.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 60935 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+619.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 61935 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+629.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 62935 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+639.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 63935 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+649.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 64936 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+659.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 65936 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+669.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 66936 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+680 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 67936 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+689.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 68936 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+699.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 69936 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+709.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 70937 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+719.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 71937 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+729.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 72937 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+739.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 73937 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+749.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 74937 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223808 134558918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+759.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 75937 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+769.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 76937 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+779.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 77938 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+789.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 78938 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+799.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 79938 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+809.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 80938 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+819.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 81938 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+829.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 82938 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+839.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 83939 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+849.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 84939 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+859.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 85939 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+869.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 86939 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+879.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 87939 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+889.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 88940 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+899.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 89940 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+909.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 90940 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+919.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 91940 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+929.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 92940 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+939.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 93941 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+949.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 94941 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+959.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 95941 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+969.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 96941 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+979.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 97941 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+989.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 98941 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+999.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 99942 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 100941 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 101941 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21211 0 0 0 102941 71 0 0 25 0 1 0 421020860 90771456 21189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21189 603 41 0 22120 0
vsize: 88644
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21212 0 0 0 103942 71 0 0 25 0 1 0 421020860 90771456 21190 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21190 603 41 0 22120 0
vsize: 88644
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21212 0 0 0 104942 71 0 0 25 0 1 0 421020860 90771456 21190 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21190 603 41 0 22120 0
vsize: 88644
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21212 0 0 0 105942 71 0 0 25 0 1 0 421020860 90771456 21190 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21190 603 41 0 22120 0
vsize: 88644
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21212 0 0 0 106942 71 0 0 25 0 1 0 421020860 90771456 21190 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22161 21190 603 41 0 22120 0
vsize: 88644
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21407 0 0 0 107942 72 0 0 25 0 1 0 421020860 91574272 21385 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22357 21385 603 41 0 22316 0
vsize: 89428
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21645 0 0 0 108941 72 0 0 25 0 1 0 421020860 92639232 21623 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22617 21623 603 41 0 22576 0
vsize: 90468
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 21835 0 0 0 109941 72 0 0 25 0 1 0 421020860 93437952 21813 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22812 21813 603 41 0 22771 0
vsize: 91248
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 22034 0 0 0 110941 73 0 0 25 0 1 0 421020860 94236672 22012 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23007 22012 603 41 0 22966 0
vsize: 92028
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 22272 0 0 0 111940 73 0 0 25 0 1 0 421020860 95170560 22250 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23235 22250 603 41 0 23194 0
vsize: 92940
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 22492 0 0 0 112940 74 0 0 25 0 1 0 421020860 96092160 22470 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23460 22470 603 41 0 23419 0
vsize: 93840
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 22707 0 0 0 113939 75 0 0 25 0 1 0 421020860 97411072 22685 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23782 22685 603 41 0 23741 0
vsize: 95128
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 22912 0 0 0 114939 76 0 0 25 0 1 0 421020860 98344960 22890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24010 22890 603 41 0 23969 0
vsize: 96040
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 23116 0 0 0 115938 77 0 0 25 0 1 0 421020860 99135488 23094 4294967295 134512640 134672761 3221224624 3221223808 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24203 23094 603 41 0 24162 0
vsize: 96812
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 23314 0 0 0 116938 77 0 0 25 0 1 0 421020860 99930112 23292 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24397 23292 603 41 0 24356 0
vsize: 97588
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 23482 0 0 0 117937 78 0 0 25 0 1 0 421020860 100597760 23460 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24560 23460 603 41 0 24519 0
vsize: 98240
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 23672 0 0 0 118937 79 0 0 25 0 1 0 421020860 101392384 23650 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24754 23650 603 41 0 24713 0
vsize: 99016
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1478
Raw data (stat): 1478 (minisat+) R 1477 30701 30700 0 -1 0 23810 0 0 0 119936 79 0 0 25 0 1 0 421020860 101924864 23788 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24884 23788 603 41 0 24843 0
vsize: 99536
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1478
Raw data (stat): 1478 (minisat+) Z 1477 30701 30700 0 -1 12 23813 0 0 0 119936 84 0 0 25 0 1 0 421020860 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.21
CPU user time (s): 1199.37
CPU system time (s): 0.842871
CPU usage (%): 100.014
Max. virtual memory (Kb): 99536
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####