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/frb45-21-opb/normalized-frb45-21-4.opb
MD5SUM	2b591d1b24a201f365bc505135aa0578
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-33
Optimality of the best value was proved	NO
Number of terms in the objective function	945
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	945
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	945
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.07
Number of variables	945
Total number of constraints	58549
Number of constraints which are clauses	58549
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 6377

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 04:44:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4844 boxname=wulflinc15 idbench=332 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2b591d1b24a201f365bc505135aa0578  /oldhome/oroussel/tmp/wulflinc15/normalized-frb45-21-4.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc15/normalized-frb45-21-4.opb /oldhome/oroussel/tmp/wulflinc15/normalized-frb45-21-4.opb
IDLAUNCH: 4844
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        889848 kB
Buffers:         36752 kB
Cached:          85816 kB
SwapCached:       2144 kB
Active:          65936 kB
Inactive:        61700 kB
HighTotal:      131008 kB
HighFree:        41244 kB
LowTotal:       903652 kB
LowFree:        848604 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11620 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:04:09 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 4844 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58549 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 |   58549   117098 |   19516       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  150295   331846 |   50098       0        0     nan |  0.000 % |
c |       101 |  150295   331846 |   55107     101      987     9.8 |  0.004 % |
c |       251 |  150272   331795 |   60618     250     1988     8.0 |  0.022 % |
c |       476 |  149917   330992 |   66680     457     3005     6.6 |  0.337 % |
c |       813 |  145622   321182 |   73348     696     4325     6.2 |  4.500 % |
c |      1319 |  141309   311322 |   80683    1103     8691     7.9 |  8.556 % |
c |      2078 |  132662   291410 |   88751    1596    14150     8.9 | 17.258 % |
c |      3219 |  122408   267731 |   97626    2364    21094     8.9 | 27.801 % |
c |      4928 |  108151   234451 |  107389    3402    34034    10.0 | 42.466 % |
c ==============================================================================
c [1mFound solution: -34[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 |      6389 |   97615   209852 |   32538    4100    41174    10.0 | 42.466 % |
c |      6491 |   97321   209169 |   35791    4184    42290    10.1 | 54.063 % |
c |      6641 |   96328   206830 |   39370    4229    42753    10.1 | 55.165 % |
c |      6866 |   95718   205411 |   43308    4396    43915    10.0 | 55.822 % |
c |      7203 |   93271   199706 |   47638    4517    45007    10.0 | 58.473 % |
c |      7710 |   91203   194840 |   52402    4677    47360    10.1 | 60.794 % |
c |      8469 |   88499   188524 |   57643    5150    54787    10.6 | 63.746 % |
c |      9608 |   85340   181085 |   63407    5805    67210    11.6 | 67.297 % |
c |     11319 |   80137   168820 |   69748    6690    95564    14.3 | 73.076 % |
c |     13881 |   75447   157813 |   76722    8164   126779    15.5 | 78.329 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14827 |   75580   158164 |   25193    9096   143040    15.7 | 78.329 % |
c |     14927 |   75423   157797 |   27712    9158   144065    15.7 | 78.473 % |
c |     15077 |   74717   156129 |   30483    9076   144188    15.9 | 79.285 % |
c |     15302 |   74243   155015 |   33531    9173   147321    16.1 | 79.821 % |
c |     15639 |   73083   152287 |   36885    9046   147449    16.3 | 81.147 % |
c |     16145 |   72647   151260 |   40573    9397   161747    17.2 | 81.613 % |
c |     16904 |   72364   150584 |   44630   10080   178798    17.7 | 81.948 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17371 |   72254   150321 |   24084   10477   207583    19.8 | 81.948 % |
c |     17471 |   72193   150176 |   26492   10551   207730    19.7 | 82.131 % |
c |     17621 |   72089   149931 |   29141   10687   209296    19.6 | 82.246 % |
c |     17846 |   71915   149511 |   32055   10802   213069    19.7 | 82.467 % |
c |     18183 |   71879   149425 |   35261   11125   223688    20.1 | 82.512 % |
c |     18689 |   71503   148544 |   38787   11432   237412    20.8 | 82.939 % |
c |     19448 |   71423   148355 |   42666   12146   265328    21.8 | 83.032 % |
c |     20588 |   71313   148095 |   46932   13129   322678    24.6 | 83.160 % |
c |     22296 |   71313   148095 |   51626   14837   408739    27.5 | 83.160 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24435 |   71118   147648 |   23706   16882   534082    31.6 | 83.160 % |
c |     24535 |   71108   147625 |   26076   16981   535709    31.5 | 83.425 % |
c |     24686 |   71108   147625 |   28684   17132   547391    32.0 | 83.425 % |
c |     24912 |   71082   147564 |   31552   17352   554506    32.0 | 83.454 % |
c |     25249 |   71082   147564 |   34707   17689   568337    32.1 | 83.454 % |
c |     25755 |   71034   147454 |   38178   18172   595454    32.8 | 83.501 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26202 |   70988   147323 |   23662   18583   626155    33.7 | 83.501 % |
c |     26302 |   70841   146969 |   26028   18443   625996    33.9 | 83.707 % |
c |     26452 |   70835   146955 |   28631   18590   632821    34.0 | 83.713 % |
c |     26677 |   70835   146955 |   31494   18815   644977    34.3 | 83.713 % |
c |     27014 |   70655   146529 |   34643   19040   655335    34.4 | 83.924 % |
c |     27520 |   70655   146529 |   38107   19546   693907    35.5 | 83.924 % |
c |     28280 |   70655   146529 |   41918   20306   763857    37.6 | 83.924 % |
c |     29419 |   70655   146529 |   46110   21445   847714    39.5 | 83.924 % |
c |     31127 |   70655   146529 |   50721   23153  1020105    44.1 | 83.924 % |
c |     33690 |   70621   146448 |   55793   25653  1234902    48.1 | 83.965 % |
c |     37534 |   70171   145398 |   61373   29068  1622284    55.8 | 84.453 % |
c |     43300 |   70143   145332 |   67510   34807  2301561    66.1 | 84.485 % |
c |     51950 |   70143   145332 |   74261   43457  3447846    79.3 | 84.485 % |
c |     64926 |   69974   144934 |   81687   56288  5758487   102.3 | 84.683 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70876 |   70034   145086 |   23344   62238  6462354   103.8 | 84.683 % |
c |     70976 |   70034   145086 |   25678   18182  2027438   111.5 | 84.689 % |
c |     71127 |   70034   145086 |   28246   18333  2034025   110.9 | 84.689 % |
c |     71353 |   70034   145086 |   31070   18559  2039532   109.9 | 84.689 % |
c |     71690 |   69891   144749 |   34177   18875  2058813   109.1 | 84.854 % |
c |     72197 |   69891   144749 |   37595   19382  2076099   107.1 | 84.854 % |
c |     72956 |   69761   144441 |   41355   20094  2152427   107.1 | 85.003 % |
c |     74096 |   69755   144427 |   45490   21233  2253239   106.1 | 85.010 % |
c |     75804 |   69745   144404 |   50039   22931  2379007   103.7 | 85.019 % |
c |     78367 |   69729   144367 |   55043   25479  2585451   101.5 | 85.035 % |
c |     82211 |   69639   144154 |   60548   29243  2918077    99.8 | 85.140 % |
c |     87977 |   69635   144145 |   66603   35006  3627932   103.6 | 85.143 % |
c |     96626 |   69542   143930 |   73263   43630  4717086   108.1 | 85.238 % |
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 |    104972 |   69447   143697 |   23149   51958  5688374   109.5 | 85.238 % |
c |    105072 |   69403   143593 |   25463   19037  1466884    77.1 | 85.398 % |
c |    105222 |   69403   143593 |   28010   19187  1476614    77.0 | 85.398 % |
c |    105447 |   69403   143593 |   30811   19412  1488922    76.7 | 85.398 % |
c |    105784 |   69403   143593 |   33892   19749  1517200    76.8 | 85.398 % |
c |    106291 |   69403   143593 |   37281   20256  1542995    76.2 | 85.398 % |
c |    107050 |   69156   143022 |   41009   20956  1583163    75.5 | 85.656 % |
c |    108189 |   69156   143022 |   45110   22095  1725867    78.1 | 85.656 % |
c |    109897 |   69156   143022 |   49621   23803  1923119    80.8 | 85.656 % |
c |    112459 |   69156   143022 |   54584   26365  2165480    82.1 | 85.656 % |
c |    116303 |   69156   143022 |   60042   30209  2575410    85.3 | 85.656 % |
c |    122069 |   69132   142965 |   66046   35970  3187941    88.6 | 85.684 % |
c |    130719 |   69104   142898 |   72651   44595  4188862    93.9 | 85.719 % |
c |    143695 |   69104   142898 |   79916   57571  5601913    97.3 | 85.719 % |
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 |    147302 |   69113   142924 |   23037   61171  5974756    97.7 | 85.719 % |
c |    147402 |   69113   142924 |   25340   19343  1386997    71.7 | 85.727 % |
c |    147553 |   69113   142924 |   27874   19494  1396532    71.6 | 85.727 % |
c |    147778 |   69113   142924 |   30662   19719  1409079    71.5 | 85.727 % |
c |    148115 |   69113   142924 |   33728   20056  1427758    71.2 | 85.727 % |
c |    148621 |   68975   142601 |   37101   20531  1461902    71.2 | 85.882 % |
c |    149381 |   68975   142601 |   40811   21291  1533183    72.0 | 85.882 % |
c |    150520 |   68763   142095 |   44892   22076  1572843    71.2 | 86.152 % |
c |    152228 |   68753   142072 |   49381   23780  1653185    69.5 | 86.162 % |
c |    154790 |   68654   141843 |   54320   25785  1920179    74.5 | 86.270 % |
c |    158634 |   68550   141598 |   59752   29579  2237110    75.6 | 86.393 % |
c |    164400 |   68550   141598 |   65727   35345  2915686    82.5 | 86.393 % |
c |    173049 |   68522   141531 |   72299   43972  3833422    87.2 | 86.428 % |
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 |    178621 |   68488   141428 |   22829   49541  4540315    91.6 | 86.428 % |
c |    178721 |   68488   141428 |   25111   49641  4550380    91.7 | 86.458 % |
c |    178871 |   68488   141428 |   27623   49791  4560580    91.6 | 86.458 % |
c |    179096 |   68488   141428 |   30385   50016  4579538    91.6 | 86.458 % |
c |    179434 |   68433   141298 |   33423   50331  4604770    91.5 | 86.524 % |
c |    179940 |   68433   141298 |   36766   50837  4648179    91.4 | 86.524 % |
c |    180699 |   68433   141298 |   40442   51596  4667820    90.5 | 86.524 % |
c |    181838 |   68433   141298 |   44487   52735  4781303    90.7 | 86.524 % |
c |    183546 |   68409   141242 |   48935   54404  4968976    91.3 | 86.550 % |
c |    186109 |   68409   141242 |   53829   56967  5150335    90.4 | 86.550 % |
c |    189953 |   68337   141072 |   59212   60765  5512566    90.7 | 86.636 % |
c |    195721 |   68337   141072 |   65133   66533  6239149    93.8 | 86.636 % |
c |    204370 |   68337   141072 |   71647   75182  6889625    91.6 | 86.636 % |
c |    217344 |   68331   141058 |   78811   88147  7988285    90.6 | 86.642 % |
c |    236805 |   68331   141058 |   86693  107608  9675852    89.9 | 86.642 % |
c |    265997 |   68331   141058 |   95362   44298  3289825    74.3 | 86.642 % |
c |    309788 |   68331   141058 |  104898   88089  6787729    77.1 | 86.642 % |
c |    375472 |   68315   141021 |  115388   41709  2135377    51.2 | 86.658 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 C358 C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.95 2/54 5045
Raw data (stat): 5045 (runsolver) R 5044 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423582228 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99945 s]
Raw data (loadavg): 0.93 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 3822 0 0 0 987 10 0 0 25 0 1 0 423582228 17625088 3800 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4303 3800 603 41 0 4262 0
vsize: 17212
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 3825 0 0 0 1987 11 0 0 25 0 1 0 423582228 17625088 3803 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4303 3803 603 41 0 4262 0
vsize: 17212
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 3831 0 0 0 2987 11 0 0 25 0 1 0 423582228 17768448 3809 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4338 3809 603 41 0 4297 0
vsize: 17352
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 3954 0 0 0 3987 11 0 0 25 0 1 0 423582228 18501632 3932 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4517 3932 603 41 0 4476 0
vsize: 18068
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 3956 0 0 0 4987 11 0 0 25 0 1 0 423582228 18501632 3934 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4517 3934 603 41 0 4476 0
vsize: 18068
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 4059 0 0 0 5986 11 0 0 25 0 1 0 423582228 18903040 4037 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4615 4037 603 41 0 4574 0
vsize: 18460
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 4526 0 0 0 6985 13 0 0 25 0 1 0 423582228 20856832 4504 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5092 4504 603 41 0 5051 0
vsize: 20368
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 5152 0 0 0 7983 14 0 0 25 0 1 0 423582228 23408640 5130 4294967295 134512640 134672761 3221224560 3221223744 134558923 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5715 5130 603 41 0 5674 0
vsize: 22860
[startup+90.004 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 5736 0 0 0 8982 16 0 0 25 0 1 0 423582228 25833472 5714 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6307 5714 603 41 0 6266 0
vsize: 25228
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 6324 0 0 0 9980 18 0 0 25 0 1 0 423582228 28368896 6302 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6926 6302 603 41 0 6885 0
vsize: 27704
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 6929 0 0 0 10978 20 0 0 25 0 1 0 423582228 30785536 6907 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7516 6907 603 41 0 7475 0
vsize: 30064
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 7585 0 0 0 11975 22 0 0 25 0 1 0 423582228 33456128 7563 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8168 7564 603 41 0 8127 0
vsize: 32672
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 8222 0 0 0 12973 25 0 0 25 0 1 0 423582228 36003840 8200 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8790 8200 603 41 0 8749 0
vsize: 35160
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 8903 0 0 0 13970 27 0 0 25 0 1 0 423582228 38793216 8881 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9471 8882 603 41 0 9430 0
vsize: 37884
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 9532 0 0 0 14969 28 0 0 25 0 1 0 423582228 41447424 9510 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10119 9510 603 41 0 10078 0
vsize: 40476
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10107 0 0 0 15968 30 0 0 25 0 1 0 423582228 43720704 10085 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10674 10085 603 41 0 10633 0
vsize: 42696
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10525 0 0 0 16967 31 0 0 25 0 1 0 423582228 45449216 10503 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11096 10503 603 41 0 11055 0
vsize: 44384
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 17967 32 0 0 25 0 1 0 423582228 46252032 10714 4294967295 134512640 134672761 3221224560 3221223716 134559752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11292 10714 603 41 0 11251 0
vsize: 45168
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 18967 32 0 0 25 0 1 0 423582228 46252032 10714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11292 10714 603 41 0 11251 0
vsize: 45168
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 19967 32 0 0 25 0 1 0 423582228 46252032 10714 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11292 10714 603 41 0 11251 0
vsize: 45168
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 20967 32 0 0 25 0 1 0 423582228 46252032 10714 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11292 10714 603 41 0 11251 0
vsize: 45168
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 21967 32 0 0 25 0 1 0 423582228 46252032 10714 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11292 10714 603 41 0 11251 0
vsize: 45168
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 22967 32 0 0 25 0 1 0 423582228 46252032 10714 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11292 10714 603 41 0 11251 0
vsize: 45168
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 23968 32 0 0 25 0 1 0 423582228 46252032 10714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11292 10714 603 41 0 11251 0
vsize: 45168
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 24968 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 25968 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 26968 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 27968 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 28968 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 29969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 30969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 31969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 32969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 33969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 34970 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 35969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 36969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 37969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 38969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223696 134560579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 39969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 40969 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 41970 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 42970 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10736 0 0 0 43970 32 0 0 25 0 1 0 423582228 46247936 10714 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10714 603 41 0 11250 0
vsize: 45164
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 10739 0 0 0 44970 32 0 0 25 0 1 0 423582228 46247936 10717 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10717 603 41 0 11250 0
vsize: 45164
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 11059 0 0 0 45969 33 0 0 25 0 1 0 423582228 47845376 11037 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11681 11037 603 41 0 11640 0
vsize: 46724
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 11352 0 0 0 46969 34 0 0 25 0 1 0 423582228 49045504 11330 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11974 11330 603 41 0 11933 0
vsize: 47896
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 11594 0 0 0 47968 35 0 0 25 0 1 0 423582228 49975296 11572 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12201 11572 603 41 0 12160 0
vsize: 48804
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 11820 0 0 0 48968 35 0 0 25 0 1 0 423582228 50933760 11798 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12435 11798 603 41 0 12394 0
vsize: 49740
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 12106 0 0 0 49967 37 0 0 25 0 1 0 423582228 52137984 12084 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12729 12084 603 41 0 12688 0
vsize: 50916
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 12364 0 0 0 50966 37 0 0 25 0 1 0 423582228 53207040 12342 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12990 12342 603 41 0 12949 0
vsize: 51960
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 12681 0 0 0 51965 38 0 0 25 0 1 0 423582228 54411264 12659 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13284 12659 603 41 0 13243 0
vsize: 53136
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 12958 0 0 0 52964 40 0 0 25 0 1 0 423582228 55607296 12936 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13576 12936 603 41 0 13535 0
vsize: 54304
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 13223 0 0 0 53964 40 0 0 25 0 1 0 423582228 56672256 13201 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13836 13201 603 41 0 13795 0
vsize: 55344
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 13420 0 0 0 54963 41 0 0 25 0 1 0 423582228 57466880 13398 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14030 13398 603 41 0 13989 0
vsize: 56120
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 13631 0 0 0 55963 42 0 0 25 0 1 0 423582228 58261504 13609 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14224 13609 603 41 0 14183 0
vsize: 56896
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 13851 0 0 0 56962 42 0 0 25 0 1 0 423582228 59195392 13829 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14452 13829 603 41 0 14411 0
vsize: 57808
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 14031 0 0 0 57962 43 0 0 25 0 1 0 423582228 59863040 14009 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14615 14009 603 41 0 14574 0
vsize: 58460
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 14294 0 0 0 58961 44 0 0 25 0 1 0 423582228 60932096 14272 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14876 14272 603 41 0 14835 0
vsize: 59504
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.95 3/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 14524 0 0 0 59960 45 0 0 25 0 1 0 423582228 61874176 14502 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15106 14502 603 41 0 15065 0
vsize: 60424
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 14742 0 0 0 60960 45 0 0 25 0 1 0 423582228 62803968 14720 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15333 14720 603 41 0 15292 0
vsize: 61332
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 14966 0 0 0 61960 46 0 0 25 0 1 0 423582228 63746048 14944 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15563 14944 603 41 0 15522 0
vsize: 62252
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15168 0 0 0 62960 46 0 0 25 0 1 0 423582228 64544768 15146 4294967295 134512640 134672761 3221224560 3221223664 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15758 15146 603 41 0 15717 0
vsize: 63032
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 63959 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 64960 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223744 134558923 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 65960 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 66960 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 67960 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 68960 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 69961 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 70961 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 71961 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223664 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 72961 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 73961 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 74962 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 75962 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 76962 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223744 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15270 0 0 0 77962 47 0 0 25 0 1 0 423582228 64942080 15248 4294967295 134512640 134672761 3221224560 3221223724 134542656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15248 603 41 0 15814 0
vsize: 63420
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 78962 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 79962 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 80963 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 81962 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 82962 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 83962 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 84962 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 85962 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 86962 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 87963 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 88963 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 89963 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 90963 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15271 0 0 0 91963 47 0 0 25 0 1 0 423582228 64942080 15249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15249 603 41 0 15814 0
vsize: 63420
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15273 0 0 0 92963 47 0 0 25 0 1 0 423582228 64942080 15251 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15251 603 41 0 15814 0
vsize: 63420
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15275 0 0 0 93964 47 0 0 25 0 1 0 423582228 64942080 15253 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15253 603 41 0 15814 0
vsize: 63420
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 5045
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15277 0 0 0 94964 47 0 0 25 0 1 0 423582228 64942080 15255 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15255 603 41 0 15814 0
vsize: 63420
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.95 3/58 5077
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15279 0 0 0 95962 49 0 0 25 0 1 0 423582228 64942080 15257 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15257 603 41 0 15814 0
vsize: 63420
[startup+970.102 s]
Raw data (loadavg): 1.15 1.00 0.96 4/59 5097
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15281 0 0 0 96970 49 0 0 25 0 1 0 423582228 64942080 15259 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 15259 603 41 0 15814 0
vsize: 63420
[startup+980.103 s]
Raw data (loadavg): 1.12 1.00 0.96 2/54 5098
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15298 0 0 0 97970 49 0 0 25 0 1 0 423582228 65073152 15276 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15887 15276 603 41 0 15846 0
vsize: 63548
[startup+990.103 s]
Raw data (loadavg): 1.10 1.00 0.96 2/54 5098
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15462 0 0 0 98969 49 0 0 25 0 1 0 423582228 65736704 15440 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16049 15440 603 41 0 16008 0
vsize: 64196
[startup+1000.1 s]
Raw data (loadavg): 1.09 1.00 0.96 2/54 5098
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15658 0 0 0 99969 50 0 0 25 0 1 0 423582228 67055616 15636 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16371 15636 603 41 0 16330 0
vsize: 65484
[startup+1010.1 s]
Raw data (loadavg): 1.07 1.00 0.96 2/54 5098
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15809 0 0 0 100969 50 0 0 25 0 1 0 423582228 67584000 15787 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16500 15787 603 41 0 16459 0
vsize: 66000
[startup+1020.1 s]
Raw data (loadavg): 1.06 1.00 0.96 2/54 5098
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 101969 50 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1030.1 s]
Raw data (loadavg): 1.05 1.00 0.96 2/54 5098
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 102969 50 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1040.1 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 103969 50 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1050.11 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 104970 50 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1060.1 s]
Raw data (loadavg): 1.03 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 105970 50 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223744 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1070.1 s]
Raw data (loadavg): 1.03 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 106969 50 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1080.1 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 107969 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1090.11 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 108969 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1100.11 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 109969 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1110.11 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 110969 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223664 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1120.11 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 111970 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1130.11 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 112970 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1140.11 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 113970 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 114970 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 115970 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 116971 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 117971 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 118971 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 5100
Raw data (stat): 5045 (minisat+) R 5044 29151 29150 0 -1 0 15884 0 0 0 119971 51 0 0 25 0 1 0 423582228 67981312 15862 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16597 15862 603 41 0 16556 0
vsize: 66388
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 5100
Raw data (stat): 5045 (minisat+) Z 5044 29151 29150 0 -1 12 15887 0 0 0 119971 54 0 0 25 0 1 0 423582228 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.14
CPU time (s): 1200.26
CPU user time (s): 1199.72
CPU system time (s): 0.541917
CPU usage (%): 100.01
Max. virtual memory (Kb): 66388
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####