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-2.opb
MD5SUM	a931f7e9a55cb6836807387327525e8b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-35
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	58624
Number of constraints which are clauses	58624
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 5037

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-13 21:33:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2966 boxname=wulflinc30 idbench=330 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  a931f7e9a55cb6836807387327525e8b  /oldhome/oroussel/tmp/wulflinc30/normalized-frb45-21-2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc30/normalized-frb45-21-2.opb
IDLAUNCH: 2966
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        739424 kB
Buffers:         37208 kB
Cached:         216976 kB
SwapCached:          0 kB
Active:          80508 kB
Inactive:       176592 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        739172 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32576 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:53:50 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 2966 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58624 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 |   58624   117248 |   19541       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[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 |  104213   224311 |   34737       0        0     nan |  0.000 % |
c |       100 |  103753   223355 |   38210      63      352     5.6 |  0.799 % |
c |       250 |  103075   221899 |   42031     184     1699     9.2 |  2.046 % |
c |       475 |  101685   218869 |   46234     359     3428     9.5 |  4.676 % |
c |       813 |   99941   215027 |   50858     624     5935     9.5 |  8.041 % |
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 |      1145 |   98367   211607 |   32789     875     9453    10.8 |  8.041 % |
c |      1246 |   97670   210062 |   36067     936    10041    10.7 | 12.509 % |
c |      1396 |   97202   209006 |   39674    1031    10925    10.6 | 13.452 % |
c |      1621 |   95987   206277 |   43642    1161    12048    10.4 | 15.877 % |
c |      1958 |   94801   203593 |   48006    1411    15086    10.7 | 18.255 % |
c |      2464 |   92142   197582 |   52807    1692    17509    10.3 | 23.612 % |
c |      3223 |   89622   191786 |   58087    2260    23288    10.3 | 28.835 % |
c |      4362 |   85515   182365 |   63896    3094    31899    10.3 | 37.082 % |
c |      6070 |   81641   173405 |   70286    4400    47324    10.8 | 45.054 % |
c |      8632 |   76140   160465 |   77314    6222    77175    12.4 | 56.811 % |
c |     12476 |   71881   150330 |   85046    9255   155440    16.8 | 66.013 % |
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 |     14307 |   70810   147891 |   23603   10753   201061    18.7 | 66.013 % |
c |     14407 |   70765   147784 |   25963   10841   202522    18.7 | 68.509 % |
c |     14557 |   70765   147784 |   28559   10991   207402    18.9 | 68.509 % |
c |     14783 |   70691   147602 |   31415   11185   216078    19.3 | 68.675 % |
c |     15120 |   70586   147358 |   34557   11507   227319    19.8 | 68.886 % |
c |     15626 |   70348   146787 |   38012   11951   241938    20.2 | 69.400 % |
c |     16385 |   70089   146154 |   41814   12648   271863    21.5 | 69.975 % |
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 |     16815 |   69891   145672 |   23297   13020   282802    21.7 | 69.975 % |
c |     16915 |   69891   145672 |   25626   13120   284893    21.7 | 70.395 % |
c |     17065 |   69891   145672 |   28189   13270   286399    21.6 | 70.395 % |
c |     17290 |   69827   145517 |   31008   13475   295467    21.9 | 70.532 % |
c |     17627 |   69734   145292 |   34109   13799   310942    22.5 | 70.743 % |
c |     18133 |   69371   144409 |   37520   14192   322561    22.7 | 71.538 % |
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 |     18277 |   69362   144430 |   23120   14335   325818    22.7 | 71.538 % |
c |     18377 |   69362   144430 |   25432   14435   332585    23.0 | 71.584 % |
c |     18527 |   69277   144233 |   27975   14556   347362    23.9 | 71.763 % |
c |     18752 |   69277   144233 |   30772   14781   367844    24.9 | 71.763 % |
c |     19089 |   69030   143626 |   33849   14950   374080    25.0 | 72.327 % |
c |     19596 |   68741   142905 |   37234   15398   392392    25.5 | 73.016 % |
c |     20355 |   68660   142718 |   40958   16081   432831    26.9 | 73.185 % |
c |     21494 |   68513   142365 |   45054   17165   509426    29.7 | 73.511 % |
c |     23202 |   68154   141510 |   49559   18653   641562    34.4 | 74.298 % |
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 |     23824 |   67852   140729 |   22617   19046   663777    34.9 | 74.298 % |
c |     23924 |   67766   140515 |   24878   19123   665280    34.8 | 75.183 % |
c |     24074 |   67714   140393 |   27366   19252   669804    34.8 | 75.292 % |
c |     24299 |   67714   140393 |   30103   19477   677322    34.8 | 75.292 % |
c |     24636 |   67714   140393 |   33113   19814   696585    35.2 | 75.292 % |
c |     25142 |   67678   140303 |   36424   20309   716491    35.3 | 75.375 % |
c |     25902 |   67425   139703 |   40067   20929   797034    38.1 | 75.917 % |
c |     27042 |   67212   139192 |   44074   21947   872312    39.7 | 76.383 % |
c |     28750 |   67142   139014 |   48481   23609  1034815    43.8 | 76.548 % |
c |     31312 |   67092   138893 |   53329   26102  1245314    47.7 | 76.657 % |
c |     35156 |   66477   137377 |   58662   29648  1507713    50.9 | 78.057 % |
c |     40922 |   66357   137092 |   64528   35234  2003265    56.9 | 78.315 % |
c |     49572 |   66165   136632 |   70981   43618  2849495    65.3 | 78.733 % |
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 |     53102 |   66131   136585 |   22043   46964  3239093    69.0 | 78.733 % |
c |     53203 |   66092   136494 |   24247   19870  1267667    63.8 | 78.977 % |
c |     53353 |   66092   136494 |   26672   20020  1277625    63.8 | 78.977 % |
c |     53578 |   66092   136494 |   29339   20245  1297647    64.1 | 78.977 % |
c |     53917 |   66083   136473 |   32273   20580  1329003    64.6 | 78.996 % |
c |     54424 |   66083   136473 |   35500   21087  1371465    65.0 | 78.996 % |
c |     55183 |   66081   136469 |   39050   21844  1449488    66.4 | 78.999 % |
c |     56322 |   66081   136469 |   42955   22983  1576964    68.6 | 78.999 % |
c |     58030 |   66081   136469 |   47251   24691  1727745    70.0 | 78.999 % |
c |     60592 |   65903   136032 |   51976   27218  1994366    73.3 | 79.390 % |
c |     64436 |   65748   135667 |   57173   31008  2368011    76.4 | 79.714 % |
c |     70202 |   65748   135667 |   62891   36774  3054028    83.0 | 79.714 % |
c |     78851 |   65630   135370 |   69180   45415  4281369    94.3 | 79.987 % |
c |     91825 |   65630   135370 |   76098   58389  6085540   104.2 | 79.987 % |
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 |     97446 |   65617   135317 |   21872   63942  6734885   105.3 | 79.987 % |
c |     97546 |   65521   135083 |   24059   19913  1776166    89.2 | 80.240 % |
c |     97696 |   65511   135059 |   26465   20062  1785837    89.0 | 80.262 % |
c |     97921 |   65485   134999 |   29111   20286  1798820    88.7 | 80.316 % |
c |     98258 |   65485   134999 |   32022   20623  1818617    88.2 | 80.316 % |
c |     98765 |   65485   134999 |   35225   21130  1863451    88.2 | 80.316 % |
c |     99525 |   65485   134999 |   38747   21890  1943719    88.8 | 80.316 % |
c |    100667 |   65432   134870 |   42622   23023  2052223    89.1 | 80.433 % |
c |    102376 |   65237   134387 |   46884   24634  2215179    89.9 | 80.881 % |
c |    104938 |   65233   134377 |   51573   27193  2439838    89.7 | 80.891 % |
c |    108784 |   65114   134084 |   56730   31017  2904470    93.6 | 81.164 % |
c |    114550 |   64872   133502 |   62403   36617  3619951    98.9 | 81.689 % |
c |    123199 |   64872   133502 |   68643   45266  4649642   102.7 | 81.689 % |
c |    136175 |   64810   133346 |   75508   58227  6774965   116.4 | 81.838 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150026 |   64829   133402 |   21609   72073  8627626   119.7 | 81.838 % |
c |    150126 |   64829   133402 |   23769   20486  1739332    84.9 | 81.817 % |
c |    150276 |   64829   133402 |   26146   20636  1744519    84.5 | 81.817 % |
c |    150501 |   64829   133402 |   28761   20861  1763472    84.5 | 81.817 % |
c |    150839 |   64720   133135 |   31637   21184  1776192    83.8 | 82.068 % |
c |    151345 |   64720   133135 |   34801   21690  1809498    83.4 | 82.068 % |
c |    152104 |   64667   133003 |   38281   22431  1868161    83.3 | 82.192 % |
c |    153244 |   64576   132788 |   42109   23332  1921393    82.4 | 82.385 % |
c |    154952 |   64519   132644 |   46320   25032  2128460    85.0 | 82.515 % |
c |    157514 |   64514   132633 |   50952   27592  2413144    87.5 | 82.525 % |
c |    161359 |   64514   132633 |   56048   31437  2830357    90.0 | 82.525 % |
c |    167125 |   64508   132619 |   61652   37198  3592888    96.6 | 82.538 % |
c |    175774 |   64484   132559 |   67818   45837  4744404   103.5 | 82.595 % |
c |    188750 |   64443   132458 |   74600   58799  6135883   104.4 | 82.690 % |
c |    208211 |   64435   132438 |   82060   78258  8346917   106.7 | 82.709 % |
c |    237404 |   64428   132421 |   90266  107448 11304159   105.2 | 82.725 % |
c |    281193 |   64313   132144 |   99292   56003  5085663    90.8 | 82.979 % |
c |    346877 |   64154   131750 |  109222  121446 12746175   105.0 | 83.347 % |
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 -C26#### 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.85 0.94 0.90 2/54 14520
Raw data (stat): 14520 (runsolver) R 14519 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479221676 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+10.0004 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 3631 0 0 0 988 9 0 0 25 0 1 0 479221676 16572416 3609 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3609 603 41 0 4005 0
vsize: 16184
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 3750 0 0 0 1987 10 0 0 25 0 1 0 479221676 17305600 3728 4294967295 134512640 134672761 3221224624 3221223816 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4225 3728 603 41 0 4184 0
vsize: 16900
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 3750 0 0 0 2987 10 0 0 25 0 1 0 479221676 17305600 3728 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4225 3728 603 41 0 4184 0
vsize: 16900
[startup+40.001 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 3750 0 0 0 3987 10 0 0 25 0 1 0 479221676 17305600 3728 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4225 3728 603 41 0 4184 0
vsize: 16900
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 3856 0 0 0 4986 11 0 0 25 0 1 0 479221676 17747968 3834 4294967295 134512640 134672761 3221224624 3221223808 134558497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4333 3834 603 41 0 4292 0
vsize: 17332
[startup+60.0027 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 4099 0 0 0 5984 13 0 0 25 0 1 0 479221676 18710528 4077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4568 4077 603 41 0 4527 0
vsize: 18272
[startup+70.0026 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 4545 0 0 0 6984 13 0 0 25 0 1 0 479221676 20639744 4523 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5039 4523 603 41 0 4998 0
vsize: 20156
[startup+80.0038 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 5107 0 0 0 7982 15 0 0 25 0 1 0 479221676 22925312 5085 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5597 5085 603 41 0 5556 0
vsize: 22388
[startup+90.0033 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 5583 0 0 0 8980 17 0 0 25 0 1 0 479221676 24813568 5561 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6058 5561 603 41 0 6017 0
vsize: 24232
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 6120 0 0 0 9978 20 0 0 25 0 1 0 479221676 27086848 6098 4294967295 134512640 134672761 3221224624 3221223728 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6613 6098 603 41 0 6572 0
vsize: 26452
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 6602 0 0 0 10976 22 0 0 25 0 1 0 479221676 29097984 6580 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7104 6580 603 41 0 7063 0
vsize: 28416
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 7112 0 0 0 11974 24 0 0 25 0 1 0 479221676 31117312 7090 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7597 7090 603 41 0 7556 0
vsize: 30388
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 7310 0 0 0 12973 25 0 0 25 0 1 0 479221676 31928320 7288 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7795 7288 603 41 0 7754 0
vsize: 31180
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 7310 0 0 0 13973 25 0 0 25 0 1 0 479221676 31928320 7288 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7795 7288 603 41 0 7754 0
vsize: 31180
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 7311 0 0 0 14972 26 0 0 25 0 1 0 479221676 31928320 7289 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7795 7289 603 41 0 7754 0
vsize: 31180
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 7311 0 0 0 15972 27 0 0 25 0 1 0 479221676 31928320 7289 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7795 7289 603 41 0 7754 0
vsize: 31180
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 7840 0 0 0 16970 29 0 0 25 0 1 0 479221676 34074624 7818 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7818 603 41 0 8278 0
vsize: 33276
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 8435 0 0 0 17969 30 0 0 25 0 1 0 479221676 36605952 8413 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8413 603 41 0 8896 0
vsize: 35748
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 8949 0 0 0 18967 32 0 0 25 0 1 0 479221676 38612992 8927 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9427 8927 603 41 0 9386 0
vsize: 37708
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 9465 0 0 0 19965 34 0 0 25 0 1 0 479221676 40755200 9443 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9950 9443 603 41 0 9909 0
vsize: 39800
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 9965 0 0 0 20964 35 0 0 25 0 1 0 479221676 42766336 9943 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10441 9943 603 41 0 10400 0
vsize: 41764
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 10391 0 0 0 21962 37 0 0 25 0 1 0 479221676 44515328 10369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10868 10369 603 41 0 10827 0
vsize: 43472
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 10779 0 0 0 22962 38 0 0 25 0 1 0 479221676 46120960 10757 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11260 10757 603 41 0 11219 0
vsize: 45040
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 23959 40 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 24959 40 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 25959 41 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 26959 41 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 27960 41 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 28960 41 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223808 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 29960 41 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 30959 42 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+320.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 31959 42 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+330.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11069 0 0 0 32959 42 0 0 25 0 1 0 479221676 47251456 11047 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11536 11047 603 41 0 11495 0
vsize: 46144
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11207 0 0 0 33958 43 0 0 25 0 1 0 479221676 47919104 11185 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11699 11185 603 41 0 11658 0
vsize: 46796
[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 11697 0 0 0 34957 44 0 0 25 0 1 0 479221676 49938432 11675 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12192 11675 603 41 0 12151 0
vsize: 48768
[startup+360.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 12141 0 0 0 35956 46 0 0 25 0 1 0 479221676 51666944 12119 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12614 12119 603 41 0 12573 0
vsize: 50456
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 12540 0 0 0 36954 48 0 0 25 0 1 0 479221676 53547008 12518 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13073 12518 603 41 0 13032 0
vsize: 52292
[startup+380.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 12910 0 0 0 37953 49 0 0 25 0 1 0 479221676 55013376 12888 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13431 12888 603 41 0 13390 0
vsize: 53724
[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 38951 51 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 39951 51 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 40951 51 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 41951 51 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 42951 52 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 43951 52 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 44950 52 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 45950 53 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 46950 53 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 47950 54 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 48949 54 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 49949 54 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 50949 55 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 51949 55 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223808 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+530.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13115 0 0 0 52948 56 0 0 25 0 1 0 479221676 55861248 13093 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13093 603 41 0 13597 0
vsize: 54552
[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13117 0 0 0 53948 56 0 0 25 0 1 0 479221676 55861248 13095 4294967295 134512640 134672761 3221224624 3221223808 134559492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13095 603 41 0 13597 0
vsize: 54552
[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13120 0 0 0 54948 56 0 0 25 0 1 0 479221676 55861248 13098 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13638 13098 603 41 0 13597 0
vsize: 54552
[startup+560.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13174 0 0 0 55948 56 0 0 25 0 1 0 479221676 56127488 13152 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13703 13152 603 41 0 13662 0
vsize: 54812
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13470 0 0 0 56947 58 0 0 25 0 1 0 479221676 57327616 13448 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13996 13448 603 41 0 13955 0
vsize: 55984
[startup+580.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 13764 0 0 0 57946 59 0 0 25 0 1 0 479221676 58523648 13742 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14288 13742 603 41 0 14247 0
vsize: 57152
[startup+590.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 14023 0 0 0 58945 60 0 0 25 0 1 0 479221676 59592704 14001 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14549 14001 603 41 0 14508 0
vsize: 58196
[startup+600.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 14304 0 0 0 59944 61 0 0 25 0 1 0 479221676 60657664 14282 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14809 14282 603 41 0 14768 0
vsize: 59236
[startup+610.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 14584 0 0 0 60942 63 0 0 25 0 1 0 479221676 61857792 14562 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15102 14562 603 41 0 15061 0
vsize: 60408
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 14834 0 0 0 61942 64 0 0 25 0 1 0 479221676 62922752 14812 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15362 14812 603 41 0 15321 0
vsize: 61448
[startup+630.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 15033 0 0 0 62941 65 0 0 25 0 1 0 479221676 63713280 15011 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15555 15011 603 41 0 15514 0
vsize: 62220
[startup+640.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 15258 0 0 0 63940 65 0 0 25 0 1 0 479221676 64638976 15236 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15781 15236 603 41 0 15740 0
vsize: 63124
[startup+650.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 15460 0 0 0 64940 66 0 0 25 0 1 0 479221676 65429504 15438 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15974 15438 603 41 0 15933 0
vsize: 63896
[startup+660.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 15667 0 0 0 65940 66 0 0 25 0 1 0 479221676 66228224 15645 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16169 15645 603 41 0 16128 0
vsize: 64676
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 15860 0 0 0 66939 67 0 0 25 0 1 0 479221676 67022848 15838 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16363 15838 603 41 0 16322 0
vsize: 65452
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 16055 0 0 0 67939 68 0 0 25 0 1 0 479221676 67817472 16033 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16557 16033 603 41 0 16516 0
vsize: 66228
[startup+690.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 16236 0 0 0 68938 69 0 0 25 0 1 0 479221676 68612096 16214 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16214 603 41 0 16710 0
vsize: 67004
[startup+700.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 16450 0 0 0 69937 70 0 0 25 0 1 0 479221676 69410816 16428 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16946 16428 603 41 0 16905 0
vsize: 67784
[startup+710.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 16679 0 0 0 70936 70 0 0 25 0 1 0 479221676 70369280 16657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17180 16657 603 41 0 17139 0
vsize: 68720
[startup+720.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 16906 0 0 0 71936 71 0 0 25 0 1 0 479221676 71299072 16884 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17407 16884 603 41 0 17366 0
vsize: 69628
[startup+730.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17127 0 0 0 72936 71 0 0 25 0 1 0 479221676 72241152 17105 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17637 17105 603 41 0 17596 0
vsize: 70548
[startup+740.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17340 0 0 0 73935 72 0 0 25 0 1 0 479221676 73039872 17318 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17832 17318 603 41 0 17791 0
vsize: 71328
[startup+750.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 74936 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+760.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 75936 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+770.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 76936 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+780.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 77936 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 78936 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+800.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 79937 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+810.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 80937 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+820.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 81937 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 82936 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 83937 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+850.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 84937 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 85937 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+870.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17353 0 0 0 86937 72 0 0 25 0 1 0 479221676 73170944 17331 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17331 603 41 0 17823 0
vsize: 71456
[startup+880.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17354 0 0 0 87937 72 0 0 25 0 1 0 479221676 73170944 17332 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17332 603 41 0 17823 0
vsize: 71456
[startup+890.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17354 0 0 0 88937 72 0 0 25 0 1 0 479221676 73170944 17332 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17332 603 41 0 17823 0
vsize: 71456
[startup+900.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17354 0 0 0 89938 72 0 0 25 0 1 0 479221676 73170944 17332 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17332 603 41 0 17823 0
vsize: 71456
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17354 0 0 0 90938 72 0 0 25 0 1 0 479221676 73170944 17332 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17332 603 41 0 17823 0
vsize: 71456
[startup+920.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17354 0 0 0 91938 72 0 0 25 0 1 0 479221676 73170944 17332 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17332 603 41 0 17823 0
vsize: 71456
[startup+930.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 92938 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+940.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 93938 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+950.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 94939 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+960.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 95939 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223728 134555197 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+970.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 96939 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+980.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 97939 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+990.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 98939 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 99940 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 100940 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 101940 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 102940 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 103940 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 104941 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 105941 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17355 0 0 0 106941 72 0 0 25 0 1 0 479221676 73170944 17333 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17864 17333 603 41 0 17823 0
vsize: 71456
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17553 0 0 0 107941 72 0 0 25 0 1 0 479221676 73977856 17531 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18061 17531 603 41 0 18020 0
vsize: 72244
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17777 0 0 0 108941 73 0 0 25 0 1 0 479221676 74907648 17755 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18288 17755 603 41 0 18247 0
vsize: 73152
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 17969 0 0 0 109940 73 0 0 25 0 1 0 479221676 75710464 17947 4294967295 134512640 134672761 3221224624 3221223796 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17947 603 41 0 18443 0
vsize: 73936
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 18198 0 0 0 110939 74 0 0 25 0 1 0 479221676 76648448 18176 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18713 18176 603 41 0 18672 0
vsize: 74852
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 18449 0 0 0 111938 75 0 0 25 0 1 0 479221676 77582336 18427 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18941 18427 603 41 0 18900 0
vsize: 75764
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 18654 0 0 0 112937 76 0 0 25 0 1 0 479221676 78397440 18632 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19140 18632 603 41 0 19099 0
vsize: 76560
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 18878 0 0 0 113937 77 0 0 25 0 1 0 479221676 79327232 18856 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19367 18856 603 41 0 19326 0
vsize: 77468
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 19087 0 0 0 114936 77 0 0 25 0 1 0 479221676 80273408 19065 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19598 19065 603 41 0 19557 0
vsize: 78392
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 19282 0 0 0 115936 78 0 0 25 0 1 0 479221676 81596416 19260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19921 19260 603 41 0 19880 0
vsize: 79684
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 19502 0 0 0 116935 79 0 0 25 0 1 0 479221676 82391040 19480 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20115 19480 603 41 0 20074 0
vsize: 80460
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 19769 0 0 0 117935 79 0 0 25 0 1 0 479221676 83456000 19747 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20375 19747 603 41 0 20334 0
vsize: 81500
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 19999 0 0 0 118935 80 0 0 25 0 1 0 479221676 84398080 19977 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20605 19977 603 41 0 20564 0
vsize: 82420
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14520
Raw data (stat): 14520 (minisat+) R 14519 11931 11930 0 -1 0 20058 0 0 0 119935 80 0 0 25 0 1 0 479221676 84664320 20036 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20670 20036 603 41 0 20629 0
vsize: 82680
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 14520
Raw data (stat): 14520 (minisat+) Z 14519 11931 11930 0 -1 12 20061 0 0 0 119935 84 0 0 25 0 1 0 479221676 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.09
CPU time (s): 1200.2
CPU user time (s): 1199.35
CPU system time (s): 0.840872
CPU usage (%): 100.009
Max. virtual memory (Kb): 82680
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####