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/frb53-24-opb/normalized-frb53-24-2.opb
MD5SUM	45b026c6b351128e9764d865ca917a59
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-40
Optimality of the best value was proved	NO
Number of terms in the objective function	1272
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	1272
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1272
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.11
Number of variables	1272
Total number of constraints	94289
Number of constraints which are clauses	94289
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 5257

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-13 23:01:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3724 boxname=wulflinc32 idbench=340 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  45b026c6b351128e9764d865ca917a59  /oldhome/oroussel/tmp/wulflinc32/normalized-frb53-24-2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc32/normalized-frb53-24-2.opb /oldhome/oroussel/tmp/wulflinc32/normalized-frb53-24-2.opb
IDLAUNCH: 3724
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034724 kB
MemFree:        708956 kB
Buffers:         34168 kB
Cached:         179840 kB
SwapCached:       1212 kB
Active:         145768 kB
Inactive:       148560 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        708700 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2244 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25656 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:21:12 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 3724 7 1200.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 94289 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 |   94289   188578 |   31429       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2518   maxlim: 38   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  111706   250820 |   37235       0        0     nan |  0.000 % |
c |       100 |  111697   250789 |   40958      98      644     6.6 |  0.134 % |
c |       250 |  111688   250758 |   45054     244     1777     7.3 |  0.159 % |
c |       475 |  111679   250727 |   49559     467     3936     8.4 |  0.185 % |
c |       812 |  111661   250665 |   54515     798     7384     9.3 |  0.240 % |
c |      1319 |  111661   250665 |   59967    1305    12773     9.8 |  0.238 % |
c |      2078 |  111616   250510 |   65964    2053    21144    10.3 |  0.371 % |
c |      3217 |  111520   250180 |   72560    3165    35057    11.1 |  0.662 % |
c |      4925 |  111181   249015 |   79816    4783    55765    11.7 |  1.696 % |
c |      7487 |  110537   246805 |   87798    7170    94258    13.1 |  3.947 % |
c |     11331 |  109240   242336 |   96578   10619   185881    17.5 |  9.081 % |
c |     17097 |  106846   234062 |  106235   15569   331393    21.3 | 19.831 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24391 |  105573   229619 |   35191   22132   549665    24.8 | 19.831 % |
c |     24491 |  105523   229439 |   38710   22192   551941    24.9 | 26.707 % |
c |     24641 |  105471   229255 |   42581   22317   555251    24.9 | 27.027 % |
c |     24866 |  105462   229224 |   46839   22528   562591    25.0 | 27.051 % |
c |     25203 |  105444   229162 |   51523   22825   580185    25.4 | 27.104 % |
c |     25709 |  105444   229162 |   56675   23331   594391    25.5 | 27.104 % |
c |     26468 |  105364   228886 |   62343   23990   623209    26.0 | 27.554 % |
c |     27607 |  105170   228204 |   68577   24957   660775    26.5 | 28.614 % |
c |     29319 |  105082   227894 |   75435   26559   734356    27.6 | 29.063 % |
c |     31881 |  104869   227143 |   82978   28957   864040    29.8 | 30.386 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 40   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31972 |  104874   227167 |   34958   29048   870702    30.0 | 30.386 % |
c |     32072 |  104835   227026 |   38453   29118   872548    30.0 | 30.643 % |
c |     32223 |  104835   227026 |   42299   29269   877774    30.0 | 30.643 % |
c |     32448 |  104835   227026 |   46529   29494   886236    30.0 | 30.643 % |
c |     32785 |  104811   226944 |   51182   29755   895966    30.1 | 30.722 % |
c |     33291 |  104805   226924 |   56300   30258   914640    30.2 | 30.749 % |
c |     34050 |  104787   226862 |   61930   30943   950636    30.7 | 30.803 % |
c |     35189 |  104769   226800 |   68123   32009  1013012    31.6 | 30.855 % |
c |     36899 |  104634   226337 |   74935   33348  1158256    34.7 | 31.465 % |
c |     39461 |  104595   226204 |   82429   35750  1379627    38.6 | 31.597 % |
c |     43305 |  104575   226134 |   90672   39493  1580583    40.0 | 31.675 % |
c |     49071 |  104494   225853 |   99739   45025  2041163    45.3 | 31.994 % |
c |     57721 |  104446   225689 |  109713   53519  2880664    53.8 | 32.151 % |
c |     70695 |  104437   225658 |  120684   66452  4202463    63.2 | 32.178 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 41   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77821 |  104275   225104 |   34758   72901  4646065    63.7 | 32.178 % |
c |     77921 |  104275   225104 |   38233   21093  1112844    52.8 | 32.937 % |
c |     78071 |  104243   224998 |   42057   21233  1120704    52.8 | 33.095 % |
c |     78297 |  104243   224998 |   46262   21459  1132786    52.8 | 33.095 % |
c |     78634 |  104243   224998 |   50889   21796  1157070    53.1 | 33.097 % |
c |     79140 |  104204   224865 |   55978   22222  1190202    53.6 | 33.307 % |
c |     79899 |  104204   224865 |   61575   22981  1274849    55.5 | 33.307 % |
c |     81038 |  104204   224865 |   67733   24120  1408269    58.4 | 33.307 % |
c |     82746 |  104176   224767 |   74506   25784  1491906    57.9 | 33.439 % |
c |     85309 |  104176   224767 |   81957   28347  1853786    65.4 | 33.441 % |
c |     89154 |  104124   224587 |   90153   32149  2288119    71.2 | 33.704 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 42   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89910 |  104125   224595 |   34708   32905  2342055    71.2 | 33.704 % |
c |     90010 |  104125   224595 |   38178   33005  2348608    71.2 | 33.721 % |
c |     90160 |  104125   224595 |   41996   33155  2358521    71.1 | 33.723 % |
c |     90385 |  104125   224595 |   46196   33380  2370170    71.0 | 33.723 % |
c |     90722 |  104125   224595 |   50815   33717  2391972    70.9 | 33.721 % |
c |     91228 |  104125   224595 |   55897   34223  2415138    70.6 | 33.721 % |
c |     91988 |  104125   224595 |   61487   34983  2453107    70.1 | 33.721 % |
c |     93128 |  104093   224485 |   67636   36073  2558713    70.9 | 33.853 % |
c |     94839 |  104093   224485 |   74399   37784  2717099    71.9 | 33.855 % |
c |     97402 |  104082   224446 |   81839   40342  2917141    72.3 | 33.906 % |
c |    101247 |  104073   224415 |   90023   44177  3255468    73.7 | 33.933 % |
c |    107015 |  103993   224137 |   99025   49899  3773445    75.6 | 34.330 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 43   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111546 |  103994   224143 |   34664   54430  4350121    79.9 | 34.330 % |
c |    111646 |  103994   224143 |   38130   18605  1313866    70.6 | 34.348 % |
c |    111796 |  103994   224143 |   41943   18755  1322981    70.5 | 34.348 % |
c |    112023 |  103994   224143 |   46137   18982  1340900    70.6 | 34.348 % |
c |    112360 |  103994   224143 |   50751   19319  1357181    70.3 | 34.347 % |
c |    112866 |  103994   224143 |   55826   19825  1398958    70.6 | 34.347 % |
c |    113626 |  103985   224112 |   61409   20565  1461164    71.1 | 34.373 % |
c |    114765 |  103985   224112 |   67550   21704  1520085    70.0 | 34.373 % |
c |    116473 |  103956   224011 |   74305   23405  1650331    70.5 | 34.479 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 44   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    118649 |  103957   224019 |   34652   25581  1856771    72.6 | 34.479 % |
c |    118750 |  103957   224019 |   38117   25682  1865259    72.6 | 34.496 % |
c |    118900 |  103957   224019 |   41928   25832  1875640    72.6 | 34.496 % |
c |    119126 |  103957   224019 |   46121   26058  1884059    72.3 | 34.496 % |
c |    119463 |  103957   224019 |   50733   26395  1891849    71.7 | 34.496 % |
c |    119970 |  103957   224019 |   55807   26902  1942557    72.2 | 34.496 % |
c |    120729 |  103957   224019 |   61388   27661  1971494    71.3 | 34.496 % |
c |    121868 |  103957   224019 |   67526   28800  2080067    72.2 | 34.498 % |
c |    123579 |  103957   224019 |   74279   30511  2191769    71.8 | 34.496 % |
c |    126142 |  103957   224019 |   81707   33074  2556701    77.3 | 34.498 % |
c |    129987 |  103937   223949 |   89878   36908  2928564    79.3 | 34.577 % |
c |    135753 |  103926   223910 |   98866   42670  3739375    87.6 | 34.629 % |
c |    144403 |  103917   223879 |  108752   51303  4553975    88.8 | 34.657 % |
c |    157378 |  103911   223859 |  119628   64274  6852179   106.6 | 34.681 % |
c |    176841 |  103911   223859 |  131590   83737  9098171   108.7 | 34.683 % |
c |    206034 |  103834   223592 |  144750  112872 12108919   107.3 | 35.025 % |
c |    249823 |  103834   223592 |  159225   26964  4960452   184.0 | 35.025 % |
c |    315507 |  103806   223494 |  175147   92637 15011782   162.0 | 35.158 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1272 -C1271 -C1270 C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/53 12830
Raw data (stat): 12830 (runsolver) R 12829 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479743988 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 4512 0 0 0 988 11 0 0 25 0 1 0 479743988 20250624 4490 4294967295 134512640 134672761 3221224560 3221223776 134557618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4944 4490 603 41 0 4903 0
vsize: 19776
[startup+20.002 s]
Raw data (loadavg): 0.89 0.94 0.90 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 4512 0 0 0 1987 11 0 0 25 0 1 0 479743988 20250624 4490 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4944 4490 603 41 0 4903 0
vsize: 19776
[startup+30.0038 s]
Raw data (loadavg): 0.90 0.94 0.90 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 4512 0 0 0 2987 11 0 0 25 0 1 0 479743988 20250624 4490 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4944 4490 603 41 0 4903 0
vsize: 19776
[startup+40.0044 s]
Raw data (loadavg): 0.92 0.94 0.90 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 4512 0 0 0 3987 11 0 0 25 0 1 0 479743988 20250624 4490 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4944 4490 603 41 0 4903 0
vsize: 19776
[startup+50.0054 s]
Raw data (loadavg): 0.93 0.94 0.90 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 4512 0 0 0 4987 12 0 0 25 0 1 0 479743988 20250624 4490 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4944 4490 603 41 0 4903 0
vsize: 19776
[startup+60.006 s]
Raw data (loadavg): 0.94 0.95 0.90 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 4512 0 0 0 5987 12 0 0 25 0 1 0 479743988 20250624 4490 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4490 603 41 0 4903 0
vsize: 19776
[startup+70.0065 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 4512 0 0 0 6987 12 0 0 25 0 1 0 479743988 20250624 4490 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4490 603 41 0 4903 0
vsize: 19776
[startup+80.0075 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 5084 0 0 0 7986 13 0 0 25 0 1 0 479743988 22540288 5062 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5503 5062 603 41 0 5462 0
vsize: 22012
[startup+90.0083 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 5610 0 0 0 8986 14 0 0 25 0 1 0 479743988 24698880 5588 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6030 5588 603 41 0 5989 0
vsize: 24120
[startup+100.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 6164 0 0 0 9985 15 0 0 25 0 1 0 479743988 26963968 6142 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 6142 603 41 0 6542 0
vsize: 26332
[startup+110.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 6742 0 0 0 10983 17 0 0 25 0 1 0 479743988 29630464 6720 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7234 6720 603 41 0 7193 0
vsize: 28936
[startup+120.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7005 0 0 0 11982 17 0 0 25 0 1 0 479743988 30711808 6983 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 6983 603 41 0 7457 0
vsize: 29992
[startup+130.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 12982 18 0 0 25 0 1 0 479743988 31576064 7217 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7217 603 41 0 7668 0
vsize: 30836
[startup+140.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 13982 18 0 0 25 0 1 0 479743988 31576064 7217 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7217 603 41 0 7668 0
vsize: 30836
[startup+150.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 14982 18 0 0 25 0 1 0 479743988 31576064 7217 4294967295 134512640 134672761 3221224560 3221223744 134558629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7217 603 41 0 7668 0
vsize: 30836
[startup+160.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 15982 18 0 0 25 0 1 0 479743988 31576064 7217 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7217 603 41 0 7668 0
vsize: 30836
[startup+170.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 16983 18 0 0 25 0 1 0 479743988 31576064 7217 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7217 603 41 0 7668 0
vsize: 30836
[startup+180.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 17982 18 0 0 25 0 1 0 479743988 31576064 7217 4294967295 134512640 134672761 3221224560 3221222912 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7217 603 41 0 7668 0
vsize: 30836
[startup+190.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 18982 18 0 0 25 0 1 0 479743988 31571968 7217 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7708 7217 603 41 0 7667 0
vsize: 30832
[startup+200.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 19983 18 0 0 25 0 1 0 479743988 31571968 7217 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7708 7217 603 41 0 7667 0
vsize: 30832
[startup+210.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 20983 18 0 0 25 0 1 0 479743988 31571968 7217 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7708 7217 603 41 0 7667 0
vsize: 30832
[startup+220.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7239 0 0 0 21983 18 0 0 25 0 1 0 479743988 31567872 7217 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7707 7217 603 41 0 7666 0
vsize: 30828
[startup+230.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 7240 0 0 0 22983 18 0 0 25 0 1 0 479743988 31567872 7218 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7707 7218 603 41 0 7666 0
vsize: 30828
[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 8044 0 0 0 23982 20 0 0 25 0 1 0 479743988 34926592 8022 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8527 8022 603 41 0 8486 0
vsize: 34108
[startup+250.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 8843 0 0 0 24980 22 0 0 25 0 1 0 479743988 38137856 8821 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9311 8821 603 41 0 9270 0
vsize: 37244
[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 9401 0 0 0 25978 24 0 0 25 0 1 0 479743988 40411136 9379 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9866 9379 603 41 0 9825 0
vsize: 39464
[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 9754 0 0 0 26977 26 0 0 25 0 1 0 479743988 41881600 9732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10225 9732 603 41 0 10184 0
vsize: 40900
[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 10130 0 0 0 27977 26 0 0 25 0 1 0 479743988 43474944 10108 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10614 10108 603 41 0 10573 0
vsize: 42456
[startup+290.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 10472 0 0 0 28976 27 0 0 25 0 1 0 479743988 44806144 10450 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10939 10450 603 41 0 10898 0
vsize: 43756
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12832
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 10858 0 0 0 29976 28 0 0 25 0 1 0 479743988 46407680 10836 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11330 10836 603 41 0 11289 0
vsize: 45320
[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 11161 0 0 0 30974 29 0 0 25 0 1 0 479743988 47603712 11139 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11622 11139 603 41 0 11581 0
vsize: 46488
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 11453 0 0 0 31973 30 0 0 25 0 1 0 479743988 48799744 11431 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11914 11431 603 41 0 11873 0
vsize: 47656
[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 11744 0 0 0 32973 31 0 0 25 0 1 0 479743988 50020352 11722 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12212 11722 603 41 0 12171 0
vsize: 48848
[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 12030 0 0 0 33972 32 0 0 25 0 1 0 479743988 51216384 12008 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12504 12008 603 41 0 12463 0
vsize: 50016
[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 12248 0 0 0 34971 32 0 0 25 0 1 0 479743988 52023296 12226 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12701 12226 603 41 0 12660 0
vsize: 50804
[startup+360.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 12587 0 0 0 35971 33 0 0 25 0 1 0 479743988 53391360 12565 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13035 12565 603 41 0 12994 0
vsize: 52140
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 12898 0 0 0 36970 34 0 0 25 0 1 0 479743988 54730752 12876 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13362 12876 603 41 0 13321 0
vsize: 53448
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 13246 0 0 0 37969 35 0 0 25 0 1 0 479743988 56217600 13224 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13725 13224 603 41 0 13684 0
vsize: 54900
[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 13553 0 0 0 38969 36 0 0 25 0 1 0 479743988 57430016 13531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14021 13531 603 41 0 13980 0
vsize: 56084
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 13862 0 0 0 39967 37 0 0 25 0 1 0 479743988 58630144 13840 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14314 13840 603 41 0 14273 0
vsize: 57256
[startup+410.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 14211 0 0 0 40966 39 0 0 25 0 1 0 479743988 60108800 14189 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14675 14189 603 41 0 14634 0
vsize: 58700
[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 14497 0 0 0 41966 40 0 0 25 0 1 0 479743988 61308928 14475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14968 14475 603 41 0 14927 0
vsize: 59872
[startup+430.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 14784 0 0 0 42965 41 0 0 25 0 1 0 479743988 62369792 14762 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15227 14762 603 41 0 15186 0
vsize: 60908
[startup+440.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 15053 0 0 0 43965 41 0 0 25 0 1 0 479743988 63451136 15031 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15491 15031 603 41 0 15450 0
vsize: 61964
[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 15335 0 0 0 44963 42 0 0 25 0 1 0 479743988 64659456 15313 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15786 15313 603 41 0 15745 0
vsize: 63144
[startup+460.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 15797 0 0 0 45962 44 0 0 25 0 1 0 479743988 66535424 15775 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16244 15775 603 41 0 16203 0
vsize: 64976
[startup+470.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 16189 0 0 0 46961 45 0 0 25 0 1 0 479743988 68145152 16167 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16637 16167 603 41 0 16596 0
vsize: 66548
[startup+480.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 16604 0 0 0 47960 46 0 0 25 0 1 0 479743988 69885952 16582 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17062 16582 603 41 0 17021 0
vsize: 68248
[startup+490.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 17043 0 0 0 48958 48 0 0 25 0 1 0 479743988 71622656 17021 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17486 17021 603 41 0 17445 0
vsize: 69944
[startup+500.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 17435 0 0 0 49958 49 0 0 25 0 1 0 479743988 73224192 17413 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17877 17413 603 41 0 17836 0
vsize: 71508
[startup+510.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 17836 0 0 0 50956 51 0 0 25 0 1 0 479743988 74829824 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18269 17814 603 41 0 18228 0
vsize: 73076
[startup+520.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 18246 0 0 0 51956 52 0 0 25 0 1 0 479743988 76562432 18224 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18224 603 41 0 18651 0
vsize: 74768
[startup+530.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 18585 0 0 0 52954 53 0 0 25 0 1 0 479743988 77901824 18563 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19019 18563 603 41 0 18978 0
vsize: 76076
[startup+540.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 18983 0 0 0 53954 53 0 0 25 0 1 0 479743988 80031744 18961 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19539 18961 603 41 0 19498 0
vsize: 78156
[startup+550.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 19322 0 0 0 54954 54 0 0 25 0 1 0 479743988 81506304 19300 4294967295 134512640 134672761 3221224560 3221223744 134559293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19899 19300 603 41 0 19858 0
vsize: 79596
[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 19634 0 0 0 55953 55 0 0 25 0 1 0 479743988 82735104 19612 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20199 19612 603 41 0 20158 0
vsize: 80796
[startup+570.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 19973 0 0 0 56953 56 0 0 25 0 1 0 479743988 84070400 19951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20525 19951 603 41 0 20484 0
vsize: 82100
[startup+580.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 20292 0 0 0 57952 57 0 0 25 0 1 0 479743988 85405696 20270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20851 20270 603 41 0 20810 0
vsize: 83404
[startup+590.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 20607 0 0 0 58950 58 0 0 25 0 1 0 479743988 86740992 20585 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21177 20585 603 41 0 21136 0
vsize: 84708
[startup+600.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 20915 0 0 0 59949 59 0 0 25 0 1 0 479743988 87941120 20893 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21470 20893 603 41 0 21429 0
vsize: 85880
[startup+610.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 21244 0 0 0 60948 60 0 0 25 0 1 0 479743988 89415680 21222 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21830 21222 603 41 0 21789 0
vsize: 87320
[startup+620.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 21590 0 0 0 61947 61 0 0 25 0 1 0 479743988 90750976 21568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22156 21568 603 41 0 22115 0
vsize: 88624
[startup+630.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 21931 0 0 0 62947 62 0 0 25 0 1 0 479743988 92225536 21909 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22516 21909 603 41 0 22475 0
vsize: 90064
[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22196 0 0 0 63946 63 0 0 25 0 1 0 479743988 93327360 22174 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22785 22174 603 41 0 22744 0
vsize: 91140
[startup+650.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22480 0 0 0 64945 63 0 0 25 0 1 0 479743988 94519296 22458 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23076 22458 603 41 0 23035 0
vsize: 92304
[startup+660.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22650 0 0 0 65945 64 0 0 25 0 1 0 479743988 95178752 22628 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22628 603 41 0 23196 0
vsize: 92948
[startup+670.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22650 0 0 0 66945 64 0 0 25 0 1 0 479743988 95178752 22628 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22628 603 41 0 23196 0
vsize: 92948
[startup+680.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22650 0 0 0 67945 65 0 0 25 0 1 0 479743988 95178752 22628 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22628 603 41 0 23196 0
vsize: 92948
[startup+690.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 68945 65 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+700.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 69944 65 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+710.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 70944 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+720.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 71944 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+730.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 72944 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+740.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 73945 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+750.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 74945 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+760.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 75945 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+770.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 76945 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+780.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 77945 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 78946 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+800.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 79946 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+810.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22651 0 0 0 80946 66 0 0 25 0 1 0 479743988 95178752 22629 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22629 603 41 0 23196 0
vsize: 92948
[startup+820.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 81946 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+830.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 82947 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+840.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 83947 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+850.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 84947 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+860.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 85947 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+870.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 86947 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+880.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 87947 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+890.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 88948 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+900.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 89948 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+910.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 90948 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+920.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 91948 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+930.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 92949 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+940.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 93949 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+950.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 94949 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+960.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 95949 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+970.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22652 0 0 0 96950 66 0 0 25 0 1 0 479743988 95178752 22630 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22630 603 41 0 23196 0
vsize: 92948
[startup+980.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 22987 0 0 0 97949 67 0 0 25 0 1 0 479743988 96514048 22965 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23563 22965 603 41 0 23522 0
vsize: 94252
[startup+990.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 23378 0 0 0 98949 67 0 0 25 0 1 0 479743988 98127872 23356 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23957 23356 603 41 0 23916 0
vsize: 95828
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 23673 0 0 0 99948 68 0 0 25 0 1 0 479743988 99332096 23651 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24251 23651 603 41 0 24210 0
vsize: 97004
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 23903 0 0 0 100948 69 0 0 25 0 1 0 479743988 100274176 23881 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24481 23881 603 41 0 24440 0
vsize: 97924
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 24135 0 0 0 101947 70 0 0 25 0 1 0 479743988 101208064 24113 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24709 24113 603 41 0 24668 0
vsize: 98836
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 24418 0 0 0 102947 70 0 0 25 0 1 0 479743988 102457344 24396 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25014 24396 603 41 0 24973 0
vsize: 100056
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 24720 0 0 0 103946 71 0 0 25 0 1 0 479743988 103669760 24698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25310 24698 603 41 0 25269 0
vsize: 101240
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 24970 0 0 0 104946 72 0 0 25 0 1 0 479743988 104738816 24948 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25571 24948 603 41 0 25530 0
vsize: 102284
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 25246 0 0 0 105945 73 0 0 25 0 1 0 479743988 105820160 25224 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25835 25224 603 41 0 25794 0
vsize: 103340
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 25598 0 0 0 106945 74 0 0 25 0 1 0 479743988 107290624 25576 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26194 25576 603 41 0 26153 0
vsize: 104776
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 25968 0 0 0 107944 74 0 0 25 0 1 0 479743988 108773376 25946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26556 25946 603 41 0 26515 0
vsize: 106224
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 26219 0 0 0 108944 75 0 0 25 0 1 0 479743988 109834240 26197 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26815 26197 603 41 0 26774 0
vsize: 107260
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 26471 0 0 0 109943 76 0 0 25 0 1 0 479743988 110784512 26449 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27047 26449 603 41 0 27006 0
vsize: 108188
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 26732 0 0 0 110943 76 0 0 25 0 1 0 479743988 111861760 26710 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27310 26710 603 41 0 27269 0
vsize: 109240
[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 26996 0 0 0 111943 77 0 0 25 0 1 0 479743988 112934912 26974 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27572 26974 603 41 0 27531 0
vsize: 110288
[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 27243 0 0 0 112942 78 0 0 25 0 1 0 479743988 113995776 27221 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27831 27221 603 41 0 27790 0
vsize: 111324
[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 27505 0 0 0 113942 78 0 0 25 0 1 0 479743988 115064832 27483 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28092 27483 603 41 0 28051 0
vsize: 112368
[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 27792 0 0 0 114941 79 0 0 25 0 1 0 479743988 116269056 27770 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28386 27770 603 41 0 28345 0
vsize: 113544
[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 28072 0 0 0 115940 81 0 0 25 0 1 0 479743988 117469184 28050 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28679 28050 603 41 0 28638 0
vsize: 114716
[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 28332 0 0 0 116939 82 0 0 25 0 1 0 479743988 118411264 28310 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28909 28310 603 41 0 28868 0
vsize: 115636
[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 28517 0 0 0 117939 82 0 0 25 0 1 0 479743988 119214080 28495 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29105 28495 603 41 0 29064 0
vsize: 116420
[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 28658 0 0 0 118939 82 0 0 25 0 1 0 479743988 119754752 28636 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29237 28636 603 41 0 29196 0
vsize: 116948
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12834
Raw data (stat): 12830 (minisat+) R 12829 7987 7986 0 -1 0 28968 0 0 0 119938 83 0 0 25 0 1 0 479743988 121094144 28946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29564 28946 603 41 0 29523 0
vsize: 118256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 12834
Raw data (stat): 12830 (minisat+) Z 12829 7987 7986 0 -1 12 28971 0 0 0 119938 89 0 0 24 0 1 0 479743988 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.16
CPU time (s): 1200.29
CPU user time (s): 1199.39
CPU system time (s): 0.899863
CPU usage (%): 100.011
Max. virtual memory (Kb): 118256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####