PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb45-21-opb/normalized-frb45-21-5.opb
MD5SUM	7850e0b228f4ef5ee038a9c3595683ab
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-33
Optimality of the best value was proved	NO
Number of terms in the objective function	945
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	945
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	945
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	945
Total number of constraints	58579
Number of constraints which are clauses	58579
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 6004

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        861572 kB
Buffers:         35364 kB
Cached:         117812 kB
SwapCached:        164 kB
Active:          55756 kB
Inactive:       100412 kB
HighTotal:      131008 kB
HighFree:         9604 kB
LowTotal:       903652 kB
LowFree:        851968 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11380 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:13:38 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 4469 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58579 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   58579   117158 |   19526       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  104196   224283 |   34732       0        0     nan |  0.000 % |
c |       100 |  103520   222871 |   38205      71      845    11.9 |  1.183 % |
c |       250 |  102504   220679 |   42025     183     4767    26.0 |  3.068 % |
c |       475 |  101590   218699 |   46228     350     8146    23.3 |  4.776 % |
c |       813 |  100165   215558 |   50851     632    11243    17.8 |  7.527 % |
c |      1320 |   98462   211789 |   55936    1027    17710    17.2 | 10.838 % |
c |      2079 |   95481   205142 |   61529    1566    24481    15.6 | 16.713 % |
c |      3218 |   90546   193957 |   67682    2295    35299    15.4 | 26.714 % |
c |      4926 |   84660   180407 |   74451    3424    47764    13.9 | 38.683 % |
c |      7488 |   77958   164680 |   81896    5317    75539    14.2 | 52.819 % |
c |     11332 |   72480   151676 |   90085    7993   127336    15.9 | 64.644 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11631 |   72262   151156 |   24087    8188   132126    16.1 | 64.644 % |
c |     11731 |   71790   150037 |   26495    8190   132316    16.2 | 66.159 % |
c |     11881 |   71669   149766 |   29145    8301   134293    16.2 | 66.400 % |
c |     12106 |   71556   149491 |   32059    8486   137274    16.2 | 66.650 % |
c |     12444 |   71318   148917 |   35265    8727   141189    16.2 | 67.179 % |
c |     12950 |   71120   148440 |   38792    9155   154159    16.8 | 67.618 % |
c |     13709 |   70835   147758 |   42671    9738   167491    17.2 | 68.239 % |
c |     14848 |   70356   146641 |   46938   10734   199805    18.6 | 69.236 % |
c |     16556 |   69392   144296 |   51632   12131   261545    21.6 | 71.384 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18254 |   68786   142907 |   22928   13556   396919    29.3 | 71.384 % |
c |     18354 |   68786   142907 |   25220   13656   397935    29.1 | 72.836 % |
c |     18505 |   68746   142819 |   27742   13744   400828    29.2 | 72.913 % |
c |     18730 |   68746   142819 |   30517   13969   414502    29.7 | 72.913 % |
c |     19067 |   68440   142073 |   33568   14192   420207    29.6 | 73.606 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19471 |   68221   141542 |   22740   14460   433715    30.0 | 73.606 % |
c |     19571 |   68218   141535 |   25014   14558   436494    30.0 | 74.099 % |
c |     19721 |   68215   141528 |   27515   14705   441753    30.0 | 74.106 % |
c |     19946 |   68209   141514 |   30266   14866   447573    30.1 | 74.119 % |
c |     20284 |   68096   141240 |   33293   15135   454576    30.0 | 74.374 % |
c |     20790 |   67967   140930 |   36622   15584   471882    30.3 | 74.655 % |
c |     21550 |   67737   140372 |   40285   16262   499377    30.7 | 75.169 % |
c |     22689 |   67420   139604 |   44313   17090   536134    31.4 | 75.875 % |
c |     24397 |   67334   139396 |   48745   18762   638169    34.0 | 76.070 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25824 |   66748   138007 |   22249   19773   713991    36.1 | 76.070 % |
c |     25926 |   66748   138007 |   24473   19875   721526    36.3 | 77.398 % |
c |     26076 |   66701   137889 |   26921   19988   725709    36.3 | 77.500 % |
c |     26304 |   66691   137865 |   29613   20188   742795    36.8 | 77.522 % |
c |     26641 |   66684   137848 |   32574   20505   764659    37.3 | 77.538 % |
c |     27147 |   66610   137670 |   35832   20966   795602    37.9 | 77.701 % |
c |     27906 |   66557   137538 |   39415   21695   840079    38.7 | 77.822 % |
c |     29045 |   66377   137118 |   43357   22659   906159    40.0 | 78.202 % |
c |     30753 |   66179   136641 |   47692   24049   979559    40.7 | 78.626 % |
c |     33315 |   66156   136582 |   52461   26592  1256078    47.2 | 78.684 % |
c |     37159 |   66080   136394 |   57708   30405  1639687    53.9 | 78.862 % |
c |     42926 |   65943   136061 |   63478   36065  2387802    66.2 | 79.169 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49021 |   65679   135390 |   21893   41853  3046899    72.8 | 79.169 % |
c |     49121 |   65630   135269 |   24082   41903  3047090    72.7 | 79.865 % |
c |     49274 |   65630   135269 |   26490   42056  3057594    72.7 | 79.865 % |
c |     49499 |   65629   135266 |   29139   42276  3063604    72.5 | 79.869 % |
c |     49837 |   65629   135266 |   32053   42614  3083440    72.4 | 79.869 % |
c |     50343 |   65606   135209 |   35258   43116  3115471    72.3 | 79.920 % |
c |     51103 |   65606   135209 |   38784   43876  3179341    72.5 | 79.920 % |
c |     52243 |   65603   135202 |   42663   45015  3258321    72.4 | 79.926 % |
c |     53951 |   65539   135048 |   46929   46676  3413313    73.1 | 80.070 % |
c |     56513 |   65539   135048 |   51622   49238  3666917    74.5 | 80.070 % |
c |     60357 |   65472   134879 |   56784   52868  4089603    77.4 | 80.232 % |
c |     66123 |   65472   134879 |   62463   58634  4702227    80.2 | 80.232 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74242 |   65424   134793 |   21808   66575  5682677    85.4 | 80.232 % |
c |     74342 |   65424   134793 |   23988   20814  1496451    71.9 | 80.407 % |
c |     74492 |   65424   134793 |   26387   20964  1504397    71.8 | 80.407 % |
c |     74717 |   65424   134793 |   29026   21189  1515936    71.5 | 80.407 % |
c |     75054 |   65424   134793 |   31929   21526  1554455    72.2 | 80.407 % |
c |     75560 |   65424   134793 |   35122   22032  1597367    72.5 | 80.407 % |
c |     76319 |   65401   134738 |   38634   22787  1659051    72.8 | 80.458 % |
c |     77458 |   65316   134534 |   42497   23897  1771616    74.1 | 80.645 % |
c |     79166 |   65306   134512 |   46747   25597  1907763    74.5 | 80.664 % |
c |     81728 |   65202   134254 |   51422   28146  2157205    76.6 | 80.903 % |
c |     85572 |   65193   134233 |   56564   31985  2530523    79.1 | 80.922 % |
c |     91338 |   65193   134233 |   62220   37751  3122150    82.7 | 80.922 % |
c |     99987 |   65123   134064 |   68442   46388  4220348    91.0 | 81.078 % |
c |    112962 |   65112   134039 |   75287   59336  5908485    99.6 | 81.100 % |
c |    132424 |   65098   134005 |   82815   78794  8817211   111.9 | 81.132 % |
c |    161617 |   65022   133819 |   91097  107974 12083003   111.9 | 81.297 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    180293 |   64927   133578 |   21642   31533  3240241   102.8 | 81.297 % |
c |    180393 |   64927   133578 |   23806   31633  3247194   102.7 | 81.511 % |
c |    180543 |   64927   133578 |   26186   31783  3252928   102.3 | 81.511 % |
c |    180768 |   64897   133504 |   28805   32002  3271201   102.2 | 81.581 % |
c |    181105 |   64897   133504 |   31686   32339  3303052   102.1 | 81.581 % |
c |    181611 |   64870   133439 |   34854   32828  3344803   101.9 | 81.641 % |
c |    182370 |   64870   133439 |   38340   33587  3402298   101.3 | 81.641 % |
c |    183510 |   64831   133342 |   42174   34709  3497246   100.8 | 81.734 % |
c |    185218 |   64831   133342 |   46391   36417  3743711   102.8 | 81.734 % |
c |    187780 |   64831   133342 |   51030   38979  4036614   103.6 | 81.734 % |
c |    191624 |   64795   133255 |   56133   42814  4428110   103.4 | 81.813 % |
c |    197390 |   64795   133255 |   61747   48580  5334245   109.8 | 81.813 % |
c |    206042 |   64693   133013 |   67921   57199  6439905   112.6 | 82.035 % |
c |    219017 |   64610   132809 |   74714   70080  7853073   112.1 | 82.226 % |
c |    238478 |   64559   132679 |   82185   89486  9966107   111.4 | 82.347 % |
c |    267670 |   64534   132616 |   90404   31903  2477608    77.7 | 82.407 % |
c |    311459 |   64455   132423 |   99444   75666  9108779   120.4 | 82.589 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 1/54 31760
Raw data (stat): 31760 (runsolver) R 31759 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422929058 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0008 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 3629 0 0 0 989 9 0 0 25 0 1 0 422929058 16498688 3607 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4028 3607 603 41 0 3987 0
vsize: 16112
[startup+20.0018 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 3646 0 0 0 1988 9 0 0 25 0 1 0 422929058 16633856 3624 4294967295 134512640 134672761 3221224560 3221223776 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4061 3624 603 41 0 4020 0
vsize: 16244
[startup+30.0024 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 3657 0 0 0 2988 9 0 0 25 0 1 0 422929058 16633856 3635 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4061 3635 603 41 0 4020 0
vsize: 16244
[startup+40.0025 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 3679 0 0 0 3987 10 0 0 25 0 1 0 422929058 16769024 3657 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4094 3657 603 41 0 4053 0
vsize: 16376
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 3822 0 0 0 4986 11 0 0 25 0 1 0 422929058 17690624 3800 4294967295 134512640 134672761 3221224560 3221223776 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4319 3800 603 41 0 4278 0
vsize: 17276
[startup+60.0034 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 3968 0 0 0 5985 12 0 0 25 0 1 0 422929058 18227200 3946 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4450 3946 603 41 0 4409 0
vsize: 17800
[startup+70.0032 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 4321 0 0 0 6983 14 0 0 25 0 1 0 422929058 19755008 4299 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4299 603 41 0 4782 0
vsize: 19292
[startup+80.0032 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 4739 0 0 0 7981 16 0 0 25 0 1 0 422929058 21467136 4717 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5241 4717 603 41 0 5200 0
vsize: 20964
[startup+90.0038 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 5425 0 0 0 8979 18 0 0 25 0 1 0 422929058 24141824 5403 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5894 5403 603 41 0 5853 0
vsize: 23576
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 6090 0 0 0 9976 21 0 0 25 0 1 0 422929058 26963968 6068 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6583 6068 603 41 0 6542 0
vsize: 26332
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 6561 0 0 0 10974 23 0 0 25 0 1 0 422929058 28975104 6539 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7074 6539 603 41 0 7033 0
vsize: 28296
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 7075 0 0 0 11971 26 0 0 25 0 1 0 422929058 30986240 7053 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7565 7053 603 41 0 7524 0
vsize: 30260
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 7482 0 0 0 12970 27 0 0 25 0 1 0 422929058 32731136 7460 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7991 7460 603 41 0 7950 0
vsize: 31964
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 7978 0 0 0 13968 29 0 0 25 0 1 0 422929058 34742272 7956 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8482 7956 603 41 0 8441 0
vsize: 33928
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 8406 0 0 0 14966 31 0 0 25 0 1 0 422929058 36487168 8384 4294967295 134512640 134672761 3221224560 3221223744 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8908 8384 603 41 0 8867 0
vsize: 35632
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 8881 0 0 0 15965 32 0 0 25 0 1 0 422929058 38350848 8859 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9363 8859 603 41 0 9322 0
vsize: 37452
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9258 0 0 0 16963 34 0 0 25 0 1 0 422929058 39825408 9236 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9723 9236 603 41 0 9682 0
vsize: 38892
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9734 0 0 0 17961 35 0 0 25 0 1 0 422929058 42090496 9712 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10276 9712 603 41 0 10235 0
vsize: 41104
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9876 0 0 0 18961 36 0 0 25 0 1 0 422929058 42614784 9854 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10404 9854 603 41 0 10363 0
vsize: 41616
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9876 0 0 0 19960 36 0 0 25 0 1 0 422929058 42614784 9854 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10404 9854 603 41 0 10363 0
vsize: 41616
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9876 0 0 0 20960 37 0 0 25 0 1 0 422929058 42614784 9854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10404 9854 603 41 0 10363 0
vsize: 41616
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9876 0 0 0 21960 37 0 0 25 0 1 0 422929058 42614784 9854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10404 9854 603 41 0 10363 0
vsize: 41616
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9876 0 0 0 22960 37 0 0 25 0 1 0 422929058 42614784 9854 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10404 9854 603 41 0 10363 0
vsize: 41616
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9876 0 0 0 23959 37 0 0 25 0 1 0 422929058 42614784 9854 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10404 9854 603 41 0 10363 0
vsize: 41616
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9876 0 0 0 24959 38 0 0 25 0 1 0 422929058 42614784 9854 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10404 9854 603 41 0 10363 0
vsize: 41616
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9876 0 0 0 25958 38 0 0 25 0 1 0 422929058 42614784 9854 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10404 9854 603 41 0 10363 0
vsize: 41616
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 9876 0 0 0 26958 38 0 0 25 0 1 0 422929058 42614784 9854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10404 9854 603 41 0 10363 0
vsize: 41616
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 10131 0 0 0 27957 40 0 0 25 0 1 0 422929058 43683840 10109 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10665 10109 603 41 0 10624 0
vsize: 42660
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 10606 0 0 0 28954 42 0 0 25 0 1 0 422929058 45674496 10584 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11151 10584 603 41 0 11110 0
vsize: 44604
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 11185 0 0 0 29952 44 0 0 25 0 1 0 422929058 48082944 11163 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11739 11163 603 41 0 11698 0
vsize: 46956
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 11720 0 0 0 30951 46 0 0 25 0 1 0 422929058 50208768 11698 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12258 11698 603 41 0 12217 0
vsize: 49032
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 12104 0 0 0 31949 47 0 0 25 0 1 0 422929058 51810304 12082 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12649 12082 603 41 0 12608 0
vsize: 50596
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 12473 0 0 0 32948 49 0 0 25 0 1 0 422929058 53280768 12451 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13008 12451 603 41 0 12967 0
vsize: 52032
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 12862 0 0 0 33947 50 0 0 25 0 1 0 422929058 54890496 12840 4294967295 134512640 134672761 3221224560 3221223744 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13401 12840 603 41 0 13360 0
vsize: 53604
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 13221 0 0 0 34946 51 0 0 25 0 1 0 422929058 56360960 13199 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13760 13199 603 41 0 13719 0
vsize: 55040
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 13538 0 0 0 35944 52 0 0 25 0 1 0 422929058 57556992 13516 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14052 13516 603 41 0 14011 0
vsize: 56208
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 13903 0 0 0 36942 54 0 0 25 0 1 0 422929058 59027456 13881 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14411 13881 603 41 0 14370 0
vsize: 57644
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31760
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 14202 0 0 0 37941 55 0 0 25 0 1 0 422929058 60362752 14180 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14737 14180 603 41 0 14696 0
vsize: 58948
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 31795
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 14509 0 0 0 38939 56 0 0 25 0 1 0 422929058 61566976 14487 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15031 14487 603 41 0 14990 0
vsize: 60124
[startup+400.012 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 31813
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 14807 0 0 0 39938 58 0 0 25 0 1 0 422929058 62754816 14785 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15321 14785 603 41 0 15280 0
vsize: 61284
[startup+410.013 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 31813
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 15098 0 0 0 40937 58 0 0 25 0 1 0 422929058 63950848 15076 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15613 15076 603 41 0 15572 0
vsize: 62452
[startup+420.012 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 31813
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 15398 0 0 0 41936 59 0 0 25 0 1 0 422929058 65155072 15376 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15907 15376 603 41 0 15866 0
vsize: 63628
[startup+430.013 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31813
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 15653 0 0 0 42936 60 0 0 25 0 1 0 422929058 66224128 15631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16168 15631 603 41 0 16127 0
vsize: 64672
[startup+440.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31813
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 15896 0 0 0 43936 61 0 0 25 0 1 0 422929058 67149824 15874 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16394 15874 603 41 0 16353 0
vsize: 65576
[startup+450.013 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31813
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 16120 0 0 0 44935 61 0 0 25 0 1 0 422929058 68075520 16098 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16620 16098 603 41 0 16579 0
vsize: 66480
[startup+460.013 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31813
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 16361 0 0 0 45935 62 0 0 25 0 1 0 422929058 69140480 16339 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16880 16339 603 41 0 16839 0
vsize: 67520
[startup+470.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 16617 0 0 0 46934 62 0 0 25 0 1 0 422929058 70066176 16595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17106 16595 603 41 0 17065 0
vsize: 68424
[startup+480.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 16903 0 0 0 47933 63 0 0 25 0 1 0 422929058 71282688 16881 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17403 16881 603 41 0 17362 0
vsize: 69612
[startup+490.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 17259 0 0 0 48932 65 0 0 25 0 1 0 422929058 72749056 17237 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17761 17237 603 41 0 17720 0
vsize: 71044
[startup+500.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 17597 0 0 0 49932 65 0 0 25 0 1 0 422929058 74076160 17575 4294967295 134512640 134672761 3221224560 3221223744 134559599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18085 17575 603 41 0 18044 0
vsize: 72340
[startup+510.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 17940 0 0 0 50930 67 0 0 25 0 1 0 422929058 75546624 17918 4294967295 134512640 134672761 3221224560 3221223700 134560629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18444 17918 603 41 0 18403 0
vsize: 73776
[startup+520.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18268 0 0 0 51929 68 0 0 25 0 1 0 422929058 76881920 18246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18770 18246 603 41 0 18729 0
vsize: 75080
[startup+530.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 52929 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+540.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 53930 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+550.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 54930 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+560.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 55930 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+570.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 56930 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+580.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 57930 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+590.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 58930 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+600.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 59931 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+610.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 60931 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+620.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 61931 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+630.016 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 62931 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+640.017 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 63931 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+650.016 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 64932 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+660.017 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 65932 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+670.017 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 66932 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+680.017 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 67932 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+690.017 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 68932 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+700.017 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 69933 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+710.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 70933 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+720.017 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 71933 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+730.017 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 72933 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+740.017 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 73933 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223744 134558880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+750.017 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 31815
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 74934 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+760.017 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 75934 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+770.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 76934 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+780.018 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 77934 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+790.018 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 78934 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+800.019 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 79935 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+810.019 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 80935 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+820.019 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 81935 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+830.018 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 82935 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+840.019 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 83935 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+850.019 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 84936 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223664 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+860.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 85936 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+870.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 86936 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+880.019 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 87936 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+890.02 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 88936 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+900.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 89937 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+910.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 90937 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+920.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 91937 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223716 134559752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+930.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 92937 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+940.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 93937 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+950.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 94938 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+960.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 95938 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+970.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 96938 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+980.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 97938 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+990.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 98938 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223664 134560523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 99938 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 100938 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 101939 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 102939 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 103939 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 104939 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 105940 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 106940 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 107940 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18368 0 0 0 108940 68 0 0 25 0 1 0 422929058 77279232 18346 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 18346 603 41 0 18826 0
vsize: 75468
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 18652 0 0 0 109939 70 0 0 25 0 1 0 422929058 78475264 18630 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19159 18630 603 41 0 19118 0
vsize: 76636
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 19031 0 0 0 110938 71 0 0 25 0 1 0 422929058 79949824 19009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19519 19009 603 41 0 19478 0
vsize: 78076
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 19322 0 0 0 111937 72 0 0 25 0 1 0 422929058 81158144 19300 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19814 19300 603 41 0 19773 0
vsize: 79256
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 19645 0 0 0 112936 73 0 0 25 0 1 0 422929058 82485248 19623 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20138 19623 603 41 0 20097 0
vsize: 80552
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 20009 0 0 0 113935 75 0 0 25 0 1 0 422929058 83951616 19987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20496 19987 603 41 0 20455 0
vsize: 81984
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 20370 0 0 0 114934 76 0 0 25 0 1 0 422929058 85426176 20348 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20856 20348 603 41 0 20815 0
vsize: 83424
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 20709 0 0 0 115933 77 0 0 25 0 1 0 422929058 86888448 20687 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21213 20687 603 41 0 21172 0
vsize: 84852
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 21037 0 0 0 116933 78 0 0 25 0 1 0 422929058 88219648 21015 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21538 21015 603 41 0 21497 0
vsize: 86152
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 21365 0 0 0 117931 80 0 0 25 0 1 0 422929058 89554944 21343 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21864 21343 603 41 0 21823 0
vsize: 87456
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 21690 0 0 0 118931 80 0 0 25 0 1 0 422929058 90894336 21668 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22191 21668 603 41 0 22150 0
vsize: 88764
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 31817
Raw data (stat): 31760 (minisat+) R 31759 25347 25346 0 -1 0 22003 0 0 0 119930 81 0 0 25 0 1 0 422929058 92094464 21981 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22484 21981 603 41 0 22443 0
vsize: 89936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 31817
Raw data (stat): 31760 (minisat+) Z 31759 25347 25346 0 -1 12 22006 0 0 0 119930 85 0 0 25 0 1 0 422929058 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.08
CPU time (s): 1200.17
CPU user time (s): 1199.31
CPU system time (s): 0.859869
CPU usage (%): 100.007
Max. virtual memory (Kb): 89936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####