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-5.opb
MD5SUM	7850e0b228f4ef5ee038a9c3595683ab
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.08
Number of variables	945
Total number of constraints	58579
Number of constraints which are clauses	58579
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 5041

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        901784 kB
Buffers:         32904 kB
Cached:          65048 kB
SwapCached:         36 kB
Active:          46292 kB
Inactive:        54524 kB
HighTotal:      131008 kB
HighFree:        62300 kB
LowTotal:       903652 kB
LowFree:        839484 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26492 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:54:50 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 2993 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58579 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 |   58579   117158 |   19526       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 |  104196   224283 |   34732       0        0     nan |  0.000 % |
c |       100 |  103520   222871 |   38205      71      845    11.9 |  1.183 % |
c |       250 |  102504   220679 |   42025     183     4767    26.0 |  3.068 % |
c |       475 |  101590   218699 |   46228     350     8146    23.3 |  4.776 % |
c |       813 |  100165   215558 |   50851     632    11243    17.8 |  7.527 % |
c |      1320 |   98462   211789 |   55936    1027    17710    17.2 | 10.838 % |
c |      2079 |   95481   205142 |   61529    1566    24481    15.6 | 16.713 % |
c |      3218 |   90546   193957 |   67682    2295    35299    15.4 | 26.714 % |
c |      4926 |   84660   180407 |   74451    3424    47764    13.9 | 38.683 % |
c |      7488 |   77958   164680 |   81896    5317    75539    14.2 | 52.819 % |
c |     11332 |   72480   151676 |   90085    7993   127336    15.9 | 64.644 % |
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 |     11631 |   72262   151156 |   24087    8188   132126    16.1 | 64.644 % |
c |     11731 |   71790   150037 |   26495    8190   132316    16.2 | 66.159 % |
c |     11881 |   71669   149766 |   29145    8301   134293    16.2 | 66.400 % |
c |     12106 |   71556   149491 |   32059    8486   137274    16.2 | 66.650 % |
c |     12444 |   71318   148917 |   35265    8727   141189    16.2 | 67.179 % |
c |     12950 |   71120   148440 |   38792    9155   154159    16.8 | 67.618 % |
c |     13709 |   70835   147758 |   42671    9738   167491    17.2 | 68.239 % |
c |     14848 |   70356   146641 |   46938   10734   199805    18.6 | 69.236 % |
c |     16556 |   69392   144296 |   51632   12131   261545    21.6 | 71.384 % |
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 |     18254 |   68786   142907 |   22928   13556   396919    29.3 | 71.384 % |
c |     18354 |   68786   142907 |   25220   13656   397935    29.1 | 72.836 % |
c |     18505 |   68746   142819 |   27742   13744   400828    29.2 | 72.913 % |
c |     18730 |   68746   142819 |   30517   13969   414502    29.7 | 72.913 % |
c |     19067 |   68440   142073 |   33568   14192   420207    29.6 | 73.606 % |
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 |     19471 |   68221   141542 |   22740   14460   433715    30.0 | 73.606 % |
c |     19571 |   68218   141535 |   25014   14558   436494    30.0 | 74.099 % |
c |     19721 |   68215   141528 |   27515   14705   441753    30.0 | 74.106 % |
c |     19946 |   68209   141514 |   30266   14866   447573    30.1 | 74.119 % |
c |     20284 |   68096   141240 |   33293   15135   454576    30.0 | 74.374 % |
c |     20790 |   67967   140930 |   36622   15584   471882    30.3 | 74.655 % |
c |     21550 |   67737   140372 |   40285   16262   499377    30.7 | 75.169 % |
c |     22689 |   67420   139604 |   44313   17090   536134    31.4 | 75.875 % |
c |     24397 |   67334   139396 |   48745   18762   638169    34.0 | 76.070 % |
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 |     25824 |   66748   138007 |   22249   19773   713991    36.1 | 76.070 % |
c |     25926 |   66748   138007 |   24473   19875   721526    36.3 | 77.398 % |
c |     26076 |   66701   137889 |   26921   19988   725709    36.3 | 77.500 % |
c |     26304 |   66691   137865 |   29613   20188   742795    36.8 | 77.522 % |
c |     26641 |   66684   137848 |   32574   20505   764659    37.3 | 77.538 % |
c |     27147 |   66610   137670 |   35832   20966   795602    37.9 | 77.701 % |
c |     27906 |   66557   137538 |   39415   21695   840079    38.7 | 77.822 % |
c |     29045 |   66377   137118 |   43357   22659   906159    40.0 | 78.202 % |
c |     30753 |   66179   136641 |   47692   24049   979559    40.7 | 78.626 % |
c |     33315 |   66156   136582 |   52461   26592  1256078    47.2 | 78.684 % |
c |     37159 |   66080   136394 |   57708   30405  1639687    53.9 | 78.862 % |
c |     42926 |   65943   136061 |   63478   36065  2387802    66.2 | 79.169 % |
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 |     49021 |   65679   135390 |   21893   41853  3046899    72.8 | 79.169 % |
c |     49121 |   65630   135269 |   24082   41903  3047090    72.7 | 79.865 % |
c |     49274 |   65630   135269 |   26490   42056  3057594    72.7 | 79.865 % |
c |     49499 |   65629   135266 |   29139   42276  3063604    72.5 | 79.869 % |
c |     49837 |   65629   135266 |   32053   42614  3083440    72.4 | 79.869 % |
c |     50343 |   65606   135209 |   35258   43116  3115471    72.3 | 79.920 % |
c |     51103 |   65606   135209 |   38784   43876  3179341    72.5 | 79.920 % |
c |     52243 |   65603   135202 |   42663   45015  3258321    72.4 | 79.926 % |
c |     53951 |   65539   135048 |   46929   46676  3413313    73.1 | 80.070 % |
c |     56513 |   65539   135048 |   51622   49238  3666917    74.5 | 80.070 % |
c |     60357 |   65472   134879 |   56784   52868  4089603    77.4 | 80.232 % |
c |     66123 |   65472   134879 |   62463   58634  4702227    80.2 | 80.232 % |
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 |     74242 |   65424   134793 |   21808   66575  5682677    85.4 | 80.232 % |
c |     74342 |   65424   134793 |   23988   20814  1496451    71.9 | 80.407 % |
c |     74492 |   65424   134793 |   26387   20964  1504397    71.8 | 80.407 % |
c |     74717 |   65424   134793 |   29026   21189  1515936    71.5 | 80.407 % |
c |     75054 |   65424   134793 |   31929   21526  1554455    72.2 | 80.407 % |
c |     75560 |   65424   134793 |   35122   22032  1597367    72.5 | 80.407 % |
c |     76319 |   65401   134738 |   38634   22787  1659051    72.8 | 80.458 % |
c |     77458 |   65316   134534 |   42497   23897  1771616    74.1 | 80.645 % |
c |     79166 |   65306   134512 |   46747   25597  1907763    74.5 | 80.664 % |
c |     81728 |   65202   134254 |   51422   28146  2157205    76.6 | 80.903 % |
c |     85572 |   65193   134233 |   56564   31985  2530523    79.1 | 80.922 % |
c |     91338 |   65193   134233 |   62220   37751  3122150    82.7 | 80.922 % |
c |     99987 |   65123   134064 |   68442   46388  4220348    91.0 | 81.078 % |
c |    112962 |   65112   134039 |   75287   59336  5908485    99.6 | 81.100 % |
c |    132424 |   65098   134005 |   82815   78794  8817211   111.9 | 81.132 % |
c |    161617 |   65022   133819 |   91097  107974 12083003   111.9 | 81.297 % |
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 |    180293 |   64927   133578 |   21642   31533  3240241   102.8 | 81.297 % |
c |    180393 |   64927   133578 |   23806   31633  3247194   102.7 | 81.511 % |
c |    180543 |   64927   133578 |   26186   31783  3252928   102.3 | 81.511 % |
c |    180768 |   64897   133504 |   28805   32002  3271201   102.2 | 81.581 % |
c |    181105 |   64897   133504 |   31686   32339  3303052   102.1 | 81.581 % |
c |    181611 |   64870   133439 |   34854   32828  3344803   101.9 | 81.641 % |
c |    182370 |   64870   133439 |   38340   33587  3402298   101.3 | 81.641 % |
c |    183510 |   64831   133342 |   42174   34709  3497246   100.8 | 81.734 % |
c |    185218 |   64831   133342 |   46391   36417  3743711   102.8 | 81.734 % |
c |    187780 |   64831   133342 |   51030   38979  4036614   103.6 | 81.734 % |
c |    191624 |   64795   133255 |   56133   42814  4428110   103.4 | 81.813 % |
c |    197390 |   64795   133255 |   61747   48580  5334245   109.8 | 81.813 % |
c |    206042 |   64693   133013 |   67921   57199  6439905   112.6 | 82.035 % |
c |    219017 |   64610   132809 |   74714   70080  7853073   112.1 | 82.226 % |
c |    238478 |   64559   132679 |   82185   89486  9966107   111.4 | 82.347 % |
c |    267670 |   64534   132616 |   90404   31903  2477608    77.7 | 82.407 % |
c |    311459 |   64455   132423 |   99444   75666  9108779   120.4 | 82.589 % |
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.91 0.95 0.90 2/54 30502
Raw data (stat): 30502 (runsolver) R 30501 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479239918 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99992 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 3647 0 0 0 986 11 0 0 25 0 1 0 479239918 16572416 3625 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3625 603 41 0 4005 0
vsize: 16184
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 3664 0 0 0 1986 12 0 0 25 0 1 0 479239918 16707584 3642 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4079 3642 603 41 0 4038 0
vsize: 16316
[startup+30.001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 3675 0 0 0 2986 12 0 0 25 0 1 0 479239918 16707584 3653 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4079 3653 603 41 0 4038 0
vsize: 16316
[startup+40.0006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 3697 0 0 0 3984 12 0 0 25 0 1 0 479239918 16842752 3675 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4112 3675 603 41 0 4071 0
vsize: 16448
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 3747 0 0 0 4984 13 0 0 25 0 1 0 479239918 16973824 3725 4294967295 134512640 134672761 3221224624 3221223888 134562485 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4144 3725 603 41 0 4103 0
vsize: 16576
[startup+60.0009 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 3984 0 0 0 5983 14 0 0 25 0 1 0 479239918 18305024 3962 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4469 3962 603 41 0 4428 0
vsize: 17876
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 4308 0 0 0 6981 15 0 0 25 0 1 0 479239918 19632128 4286 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4793 4286 603 41 0 4752 0
vsize: 19172
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 4716 0 0 0 7979 18 0 0 25 0 1 0 479239918 21352448 4694 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5213 4694 603 41 0 5172 0
vsize: 20852
[startup+90.0017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 5374 0 0 0 8977 20 0 0 25 0 1 0 479239918 24018944 5352 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5864 5352 603 41 0 5823 0
vsize: 23456
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 6039 0 0 0 9974 23 0 0 25 0 1 0 479239918 26841088 6017 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6553 6017 603 41 0 6512 0
vsize: 26212
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 6509 0 0 0 10971 26 0 0 25 0 1 0 479239918 28721152 6487 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7012 6487 603 41 0 6971 0
vsize: 28048
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 7069 0 0 0 11968 29 0 0 25 0 1 0 479239918 31047680 7047 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7580 7047 603 41 0 7539 0
vsize: 30320
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 7464 0 0 0 12967 30 0 0 25 0 1 0 479239918 32657408 7442 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7973 7442 603 41 0 7932 0
vsize: 31892
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 7948 0 0 0 13966 31 0 0 25 0 1 0 479239918 34541568 7926 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8433 7926 603 41 0 8392 0
vsize: 33732
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 8383 0 0 0 14964 33 0 0 25 0 1 0 479239918 36286464 8361 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8859 8361 603 41 0 8818 0
vsize: 35436
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 8842 0 0 0 15962 35 0 0 25 0 1 0 479239918 38170624 8820 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9319 8820 603 41 0 9278 0
vsize: 37276
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9224 0 0 0 16960 38 0 0 25 0 1 0 479239918 39772160 9202 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9710 9202 603 41 0 9669 0
vsize: 38840
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9689 0 0 0 17958 40 0 0 25 0 1 0 479239918 41652224 9667 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10169 9667 603 41 0 10128 0
vsize: 40676
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9924 0 0 0 18957 41 0 0 25 0 1 0 479239918 42815488 9902 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9902 603 41 0 10412 0
vsize: 41812
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9924 0 0 0 19957 41 0 0 25 0 1 0 479239918 42815488 9902 4294967295 134512640 134672761 3221224624 3221223728 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9902 603 41 0 10412 0
vsize: 41812
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9924 0 0 0 20957 41 0 0 25 0 1 0 479239918 42815488 9902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9902 603 41 0 10412 0
vsize: 41812
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9924 0 0 0 21956 42 0 0 25 0 1 0 479239918 42815488 9902 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9902 603 41 0 10412 0
vsize: 41812
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9924 0 0 0 22956 42 0 0 25 0 1 0 479239918 42815488 9902 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9902 603 41 0 10412 0
vsize: 41812
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9924 0 0 0 23956 42 0 0 25 0 1 0 479239918 42815488 9902 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9902 603 41 0 10412 0
vsize: 41812
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9924 0 0 0 24956 43 0 0 25 0 1 0 479239918 42815488 9902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9902 603 41 0 10412 0
vsize: 41812
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9924 0 0 0 25956 43 0 0 25 0 1 0 479239918 42815488 9902 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9902 603 41 0 10412 0
vsize: 41812
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 9924 0 0 0 26956 43 0 0 25 0 1 0 479239918 42815488 9902 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10453 9902 603 41 0 10412 0
vsize: 41812
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 10081 0 0 0 27955 44 0 0 25 0 1 0 479239918 43483136 10059 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10616 10059 603 41 0 10575 0
vsize: 42464
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 10468 0 0 0 28952 46 0 0 25 0 1 0 479239918 45088768 10446 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11008 10446 603 41 0 10967 0
vsize: 44032
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 11061 0 0 0 29951 48 0 0 25 0 1 0 479239918 47489024 11039 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11594 11039 603 41 0 11553 0
vsize: 46376
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 11595 0 0 0 30948 50 0 0 25 0 1 0 479239918 49745920 11573 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12145 11573 603 41 0 12104 0
vsize: 48580
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 12032 0 0 0 31947 52 0 0 25 0 1 0 479239918 51482624 12010 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12569 12010 603 41 0 12528 0
vsize: 50276
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 12371 0 0 0 32945 54 0 0 25 0 1 0 479239918 52817920 12349 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12895 12349 603 41 0 12854 0
vsize: 51580
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 12765 0 0 0 33943 56 0 0 25 0 1 0 479239918 54423552 12743 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13287 12743 603 41 0 13246 0
vsize: 53148
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 13138 0 0 0 34942 58 0 0 25 0 1 0 479239918 56037376 13116 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13681 13116 603 41 0 13640 0
vsize: 54724
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 13444 0 0 0 35941 59 0 0 25 0 1 0 479239918 57241600 13422 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13975 13422 603 41 0 13934 0
vsize: 55900
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 13798 0 0 0 36939 60 0 0 25 0 1 0 479239918 58707968 13776 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14333 13776 603 41 0 14292 0
vsize: 57332
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 14119 0 0 0 37939 61 0 0 25 0 1 0 479239918 59920384 14097 4294967295 134512640 134672761 3221224624 3221223808 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14097 603 41 0 14588 0
vsize: 58516
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 14422 0 0 0 38937 63 0 0 25 0 1 0 479239918 61255680 14400 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14955 14400 603 41 0 14914 0
vsize: 59820
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 14720 0 0 0 39936 65 0 0 25 0 1 0 479239918 62459904 14698 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15249 14698 603 41 0 15208 0
vsize: 60996
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 15005 0 0 0 40934 66 0 0 25 0 1 0 479239918 63520768 14983 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15508 14983 603 41 0 15467 0
vsize: 62032
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 15293 0 0 0 41932 68 0 0 25 0 1 0 479239918 64716800 15271 4294967295 134512640 134672761 3221224624 3221223544 1075351106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15800 15271 603 41 0 15759 0
vsize: 63200
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 15571 0 0 0 42931 70 0 0 25 0 1 0 479239918 65916928 15549 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16093 15549 603 41 0 16052 0
vsize: 64372
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 15806 0 0 0 43931 70 0 0 25 0 1 0 479239918 66846720 15784 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16320 15784 603 41 0 16279 0
vsize: 65280
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 16036 0 0 0 44930 72 0 0 25 0 1 0 479239918 67776512 16014 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16547 16014 603 41 0 16506 0
vsize: 66188
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 16257 0 0 0 45929 73 0 0 25 0 1 0 479239918 68702208 16235 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16773 16235 603 41 0 16732 0
vsize: 67092
[startup+470.008 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 16502 0 0 0 46928 74 0 0 25 0 1 0 479239918 69636096 16480 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17001 16480 603 41 0 16960 0
vsize: 68004
[startup+480.008 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 16747 0 0 0 47927 75 0 0 25 0 1 0 479239918 70696960 16725 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17260 16725 603 41 0 17219 0
vsize: 69040
[startup+490.008 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 17063 0 0 0 48926 76 0 0 25 0 1 0 479239918 71905280 17041 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17555 17041 603 41 0 17514 0
vsize: 70220
[startup+500.008 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 17424 0 0 0 49924 78 0 0 25 0 1 0 479239918 73383936 17402 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17916 17402 603 41 0 17875 0
vsize: 71664
[startup+510.007 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 17726 0 0 0 50923 79 0 0 25 0 1 0 479239918 74579968 17704 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18208 17704 603 41 0 18167 0
vsize: 72832
[startup+520.008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18067 0 0 0 51922 80 0 0 25 0 1 0 479239918 76046336 18045 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18566 18045 603 41 0 18525 0
vsize: 74264
[startup+530.008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18390 0 0 0 52921 81 0 0 25 0 1 0 479239918 77369344 18368 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18368 603 41 0 18848 0
vsize: 75556
[startup+540.007 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 53921 81 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+550.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 54921 81 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+560.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 55921 82 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+570.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 56921 82 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+580.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 57921 82 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+590.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 58920 83 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+600.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 59920 83 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+610.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 60920 83 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+620.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 61920 83 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+630.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 62920 84 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+640.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 63919 84 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+650.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 64918 85 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223760 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+660.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 65918 85 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+670.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 66918 85 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+680.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 67918 86 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+690.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 68918 86 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+700.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 69918 86 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+710.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 70918 86 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+720.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 71917 87 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+730.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 72917 87 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+740.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 73917 88 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223808 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+750.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 74916 88 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+760.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 75916 88 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+770.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 76916 89 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+780.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 77916 89 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223760 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+790.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 78916 89 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+800.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 79916 89 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+810.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 80916 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+820.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 81916 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+830.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 82916 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+840.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 83916 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+850.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 84916 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+860.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 85917 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+870.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 86917 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+880.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 87917 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+890.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 88917 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+900.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 89917 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+910.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 90918 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223760 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+920.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 91918 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+930.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 92918 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+940.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 93918 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223808 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+950.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 94918 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+960.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 95918 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+970.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 96919 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+980.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 97919 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+990.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 98919 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 99919 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 100919 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223808 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 101919 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 102920 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 103920 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 104920 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 105920 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 106920 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 107920 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 108921 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18406 0 0 0 109921 90 0 0 25 0 1 0 479239918 77369344 18384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18889 18384 603 41 0 18848 0
vsize: 75556
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18466 0 0 0 110921 90 0 0 25 0 1 0 479239918 77635584 18444 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18954 18444 603 41 0 18913 0
vsize: 75816
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 18787 0 0 0 111920 91 0 0 25 0 1 0 479239918 78979072 18765 4294967295 134512640 134672761 3221224624 3221223808 134558875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19282 18765 603 41 0 19241 0
vsize: 77128
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 19151 0 0 0 112919 92 0 0 25 0 1 0 479239918 80445440 19129 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19640 19129 603 41 0 19599 0
vsize: 78560
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 19439 0 0 0 113918 93 0 0 25 0 1 0 479239918 81657856 19417 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19936 19417 603 41 0 19895 0
vsize: 79744
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 19786 0 0 0 114918 94 0 0 25 0 1 0 479239918 83136512 19764 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20297 19764 603 41 0 20256 0
vsize: 81188
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 20136 0 0 0 115917 95 0 0 25 0 1 0 479239918 84471808 20114 4294967295 134512640 134672761 3221224624 3221223728 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20623 20114 603 41 0 20582 0
vsize: 82492
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 20492 0 0 0 116915 97 0 0 25 0 1 0 479239918 85934080 20470 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20980 20470 603 41 0 20939 0
vsize: 83920
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 20828 0 0 0 117915 97 0 0 25 0 1 0 479239918 87396352 20806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21337 20806 603 41 0 21296 0
vsize: 85348
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 21153 0 0 0 118914 98 0 0 25 0 1 0 479239918 88727552 21131 4294967295 134512640 134672761 3221224624 3221223760 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21662 21131 603 41 0 21621 0
vsize: 86648
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 28099 28098 0 -1 0 21478 0 0 0 119913 99 0 0 25 0 1 0 479239918 89939968 21456 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21958 21456 603 41 0 21917 0
vsize: 87832
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 30502
Raw data (stat): 30502 (minisat+) Z 30501 28099 28098 0 -1 12 21481 0 0 0 119913 103 0 0 25 0 1 0 479239918 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.06
CPU time (s): 1200.18
CPU user time (s): 1199.14
CPU system time (s): 1.03784
CPU usage (%): 100.01
Max. virtual memory (Kb): 87832
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####