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/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-sctap1.opb
MD5SUM	6d2898572483dddc248ecc48cac97a0c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5657891
Optimality of the best value was proved	NO
Number of terms in the objective function	7200
Biggest coefficient in the objective function	41943040
Number of bits for the biggest coefficient in the objective function	26
Sum of the numbers in the objective function	6207564000
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	41943040
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	6207564000
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	390.25
Number of variables	9600
Total number of constraints	300
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	300
Minimum length of a constraint	60
Maximum length of a constraint	440
Trace number 19667

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 19:28:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16313 boxname=wulflinc29 idbench=1255 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6d2898572483dddc248ecc48cac97a0c  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-sctap1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-sctap1.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-sctap1.opb
IDLAUNCH: 16313
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        870140 kB
Buffers:         25748 kB
Cached:         112680 kB
SwapCached:       4304 kB
Active:          40948 kB
Inactive:       103224 kB
HighTotal:      131008 kB
HighFree:        21028 kB
LowTotal:       903652 kB
LowFree:        849112 kB
SwapTotal:     2097892 kB
SwapFree:      2092680 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            14764 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:48:08 (client local time) WITH STATUS 0 IN 1200.39 SECONDS
stats: 16313 7 1200.39 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 404 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): ss
c ---[ 405]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 404]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 399]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 398]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 397]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 393]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 389]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 387]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 383]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 381]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 375]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 369]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 367]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 363]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 361]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 359]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 358]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 357]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 355]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 354]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 353]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 351]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 346]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 345]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 339]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 337]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 336]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 333]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 331]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 329]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 327]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 325]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 323]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 321]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 317]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 315]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 313]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 307]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> BDD-cost:   76
c ---[ 294]---> BDD-cost:   76
c ---[ 292]---> BDD-cost:   76
c ---[ 290]---> BDD-cost:   76
c ---[ 288]---> BDD-cost:   76
c ---[ 286]---> BDD-cost:   76
c ---[ 284]---> BDD-cost:   76
c ---[ 282]---> BDD-cost:   76
c ---[ 280]---> BDD-cost:   76
c ---[ 278]---> BDD-cost:   76
c ---[ 276]---> BDD-cost:   76
c ---[ 274]---> BDD-cost:   76
c ---[ 272]---> BDD-cost:   76
c ---[ 270]---> BDD-cost:   76
c ---[ 268]---> BDD-cost:   76
c ---[ 266]---> BDD-cost:   76
c ---[ 264]---> BDD-cost:   76
c ---[ 262]---> BDD-cost:   76
c ---[ 260]---> BDD-cost:   76
c ---[ 258]---> BDD-cost:   76
c ---[ 256]---> BDD-cost:   76
c ---[ 254]---> BDD-cost:   76
c ---[ 252]---> BDD-cost:   76
c ---[ 250]---> BDD-cost:   76
c ---[ 248]---> BDD-cost:   76
c ---[ 246]---> BDD-cost:   76
c ---[ 244]---> BDD-cost:   76
c ---[ 242]---> BDD-cost:   76
c ---[ 240]---> BDD-cost:   76
c ---[ 238]---> BDD-cost:   76
c ---[ 236]---> BDD-cost:   76
c ---[ 234]---> BDD-cost:   76
c ---[ 232]---> BDD-cost:   76
c ---[ 230]---> BDD-cost:   76
c ---[ 228]---> BDD-cost:   76
c ---[ 226]---> BDD-cost:   76
c ---[ 224]---> BDD-cost:   76
c ---[ 222]---> BDD-cost:   76
c ---[ 220]---> BDD-cost:   76
c ---[ 218]---> BDD-cost:   76
c ---[ 216]---> BDD-cost:   76
c ---[ 214]---> BDD-cost:   76
c ---[ 212]---> BDD-cost:   76
c ---[ 210]---> BDD-cost:   76
c ---[ 208]---> BDD-cost:   76
c ---[ 206]---> BDD-cost:   76
c ---[ 204]---> BDD-cost:   76
c ---[ 202]---> BDD-cost:   76
c ---[ 200]---> BDD-cost:   76
c ---[ 198]---> BDD-cost:   76
c ---[ 196]---> BDD-cost:   76
c ---[ 194]---> BDD-cost:   76
c ---[ 192]---> BDD-cost:   76
c ---[ 190]---> BDD-cost:   76
c ---[ 188]---> BDD-cost:   76
c ---[ 186]---> BDD-cost:   76
c ---[ 184]---> BDD-cost:   76
c ---[ 182]---> BDD-cost:   76
c ---[ 180]---> BDD-cost:   76
c ---[ 178]---> BDD-cost:   76
c ---[ 176]---> BDD-cost:   76
c ---[ 174]---> BDD-cost:   76
c ---[ 172]---> BDD-cost:   76
c ---[ 170]---> BDD-cost:   76
c ---[ 168]---> BDD-cost:   76
c ---[ 166]---> BDD-cost:   76
c ---[ 164]---> BDD-cost:   76
c ---[ 162]---> BDD-cost:   76
c ---[ 160]---> BDD-cost:   76
c ---[ 158]---> BDD-cost:   76
c ---[ 156]---> BDD-cost:   76
c ---[ 154]---> BDD-cost:   76
c ---[ 152]---> BDD-cost:   76
c ---[ 150]---> BDD-cost:   76
c ---[ 148]---> BDD-cost:   76
c ---[ 146]---> BDD-cost:   76
c ---[ 144]---> BDD-cost:   76
c ---[ 142]---> BDD-cost:   76
c ---[ 140]---> BDD-cost:   76
c ---[ 138]---> BDD-cost:   76
c ---[ 136]---> BDD-cost:   76
c ---[ 134]---> BDD-cost:   76
c ---[ 132]---> BDD-cost:   76
c ---[ 130]---> BDD-cost:   76
c ---[ 128]---> BDD-cost:   76
c ---[ 126]---> BDD-cost:   76
c ---[ 124]---> BDD-cost:   76
c ---[ 122]---> BDD-cost:   76
c ---[ 120]---> BDD-cost:   76
c ---[ 118]---> BDD-cost:   76
c ---[ 116]---> BDD-cost:   76
c ---[ 114]---> BDD-cost:   76
c ---[ 112]---> BDD-cost:   76
c ---[ 110]---> BDD-cost:   76
c ---[ 108]---> BDD-cost:   76
c ---[ 106]---> BDD-cost:   76
c ---[ 104]---> BDD-cost:   76
c ---[ 102]---> BDD-cost:   76
c ---[ 100]---> BDD-cost:   76
c ---[  98]---> BDD-cost:   76
c ---[  96]---> BDD-cost:   74
c ---[  94]---> BDD-cost:   76
c ---[  92]---> BDD-cost:   74
c ---[  90]---> BDD-cost:   74
c ---[  88]---> BDD-cost:   74
c ---[  86]---> BDD-cost:   74
c ---[  84]---> BDD-cost:   74
c ---[  82]---> BDD-cost:   74
c ---[  80]---> BDD-cost:   74
c ---[  78]---> BDD-cost:   74
c ---[  76]---> BDD-cost:   74
c ---[  74]---> BDD-cost:   76
c ---[  72]---> BDD-cost:   74
c ---[  70]---> BDD-cost:   74
c ---[  68]---> BDD-cost:   74
c ---[  66]---> BDD-cost:   74
c ---[  64]---> BDD-cost:   74
c ---[  62]---> BDD-cost:   74
c ---[  60]---> BDD-cost:   74
c ---[  58]---> BDD-cost:   74
c ---[  57]---> Adder-cost: 494   maxlim: 2106584   bits: 23/22
c ---[  55]---> Adder-cost: 494   maxlim: 2107864   bits: 23/22
c ---[  54]---> Adder-cost: 494   maxlim: 2109144   bits: 23/22
c ---[  53]---> Adder-cost: 494   maxlim: 2107864   bits: 23/22
c ---[  52]---> Adder-cost: 494   maxlim: 2106968   bits: 23/22
c ---[  51]---> Adder-cost: 494   maxlim: 2106584   bits: 23/22
c ---[  50]---> Adder-cost: 494   maxlim: 2106584   bits: 23/22
c ---[  49]---> Adder-cost: 494   maxlim: 2106584   bits: 23/22
c ---[  48]---> Adder-cost: 494   maxlim: 2106584   bits: 23/22
c ---[  47]---> Adder-cost: 860   maxlim: 4206794   bits: 24/23
c ---[  45]---> Adder-cost: 860   maxlim: 4210634   bits: 24/23
c ---[  44]---> Adder-cost: 860   maxlim: 4211914   bits: 24/23
c ---[  43]---> Adder-cost: 860   maxlim: 4210634   bits: 24/23
c ---[  42]---> Adder-cost: 860   maxlim: 4209994   bits: 24/23
c ---[  41]---> Adder-cost: 860   maxlim: 4209354   bits: 24/23
c ---[  40]---> Adder-cost: 860   maxlim: 4208074   bits: 24/23
c ---[  39]---> Adder-cost: 860   maxlim: 4206794   bits: 24/23
c ---[  38]---> Adder-cost: 860   maxlim: 4206794   bits: 24/23
c ---[  37]---> Sorter-cost: 2521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost: 2531     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost: 2521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost: 2521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost: 2521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost: 2521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost: 2521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost: 2521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost: 2521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Adder-cost: 646   maxlim: 2133104   bits: 23/22
c ---[  27]---> Adder-cost: 646   maxlim: 2133744   bits: 23/22
c ---[  26]---> Adder-cost: 646   maxlim: 2134384   bits: 23/22
c ---[  25]---> Adder-cost: 646   maxlim: 2135664   bits: 23/22
c ---[  24]---> Adder-cost: 646   maxlim: 2135024   bits: 23/22
c ---[  23]---> Adder-cost: 646   maxlim: 2134384   bits: 23/22
c ---[  22]---> Adder-cost: 646   maxlim: 2134384   bits: 23/22
c ---[  21]---> Adder-cost: 646   maxlim: 2133744   bits: 23/22
c ---[  20]---> Adder-cost: 646   maxlim: 2133104   bits: 23/22
c ---[  19]---> Adder-cost: 688   maxlim: 2131574   bits: 23/22
c ---[  18]---> Adder-cost: 688   maxlim: 2131574   bits: 23/22
c ---[  17]---> Adder-cost: 688   maxlim: 2133494   bits: 23/22
c ---[  16]---> Adder-cost: 688   maxlim: 2136694   bits: 23/22
c ---[  15]---> Adder-cost: 688   maxlim: 2135414   bits: 23/22
c ---[  14]---> Adder-cost: 688   maxlim: 2134134   bits: 23/22
c ---[  13]---> Adder-cost: 688   maxlim: 2132854   bits: 23/22
c ---[  12]---> Adder-cost: 688   maxlim: 2131574   bits: 23/22
c ---[  11]---> Adder-cost: 688   maxlim: 2131574   bits: 23/22
c ---[  10]---> Adder-cost: 312   maxlim: 1056734   bits: 22/21
c ---[   9]---> Adder-cost: 312   maxlim: 1056734   bits: 22/21
c ---[   8]---> Adder-cost: 312   maxlim: 1056734   bits: 22/21
c ---[   7]---> Adder-cost: 312   maxlim: 1056734   bits: 22/21
c ---[   6]---> Adder-cost: 312   maxlim: 1057374   bits: 22/21
c ---[   5]---> Adder-cost: 312   maxlim: 1058654   bits: 22/21
c ---[   4]---> Adder-cost: 312   maxlim: 1059294   bits: 22/21
c ---[   3]---> Adder-cost: 312   maxlim: 1058014   bits: 22/21
c ---[   2]---> Adder-cost: 312   maxlim: 1057374   bits: 22/21
c ---[   1]---> Adder-cost: 154   maxlim: 639   bits: 11/10
c ---[   0]---> Adder-cost: 287   maxlim: 639   bits: 11/10
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  737570  1962473 |  221270       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/220839          
c   -- var.elim.:  2000/220839          
c   -- var.elim.:  3000/220839          
c   -- var.elim.:  4000/220839          
c   -- var.elim.:  5000/220839          
c   -- var.elim.:  6000/220839          
c   -- var.elim.:  7000/220839          
c   -- var.elim.:  8000/220839          
c   -- var.elim.:  9000/220839          
c   -- var.elim.:  10000/220839          
c   -- var.elim.:  11000/220839          
c   -- var.elim.:  12000/220839          
c   -- var.elim.:  13000/220839          
c   -- var.elim.:  14000/220839          
c   -- var.elim.:  15000/220839          
c   -- var.elim.:  16000/220839          
c   -- var.elim.:  17000/220839          
c   -- var.elim.:  18000/220839          
c   -- var.elim.:  19000/220839          
c   -- var.elim.:  20000/220839          
c   -- var.elim.:  21000/220839          
c   -- var.elim.:  22000/220839          
c   -- var.elim.:  23000/220839          
c   -- var.elim.:  24000/220839          
c   -- var.elim.:  25000/220839          
c   -- var.elim.:  26000/220839          
c   -- var.elim.:  27000/220839          
c   -- var.elim.:  28000/220839          
c   -- var.elim.:  29000/220839          
c   -- var.elim.:  30000/220839          
c   -- var.elim.:  31000/220839          
c   -- var.elim.:  32000/220839          
c   -- var.elim.:  33000/220839          
c   -- var.elim.:  34000/220839          
c   -- var.elim.:  35000/220839          
c   -- var.elim.:  36000/220839          
c   -- var.elim.:  37000/220839          
c   -- var.elim.:  38000/220839          
c   -- var.elim.:  39000/220839          
c   -- var.elim.:  40000/220839          
c   -- var.elim.:  41000/220839          
c   -- var.elim.:  42000/220839          
c   -- var.elim.:  43000/220839          
c   -- var.elim.:  44000/220839          
c   -- var.elim.:  45000/220839          
c   -- var.elim.:  46000/220839          
c   -- var.elim.:  47000/220839          
c   -- var.elim.:  48000/220839          
c   -- var.elim.:  49000/220839          
c   -- var.elim.:  50000/220839          
c   -- var.elim.:  51000/220839          
c   -- var.elim.:  52000/220839          
c   -- var.elim.:  53000/220839          
c   -- var.elim.:  54000/220839          
c   -- var.elim.:  55000/220839          
c   -- var.elim.:  56000/220839          
c   -- var.elim.:  57000/220839          
c   -- var.elim.:  58000/220839          
c   -- var.elim.:  59000/220839          
c   -- var.elim.:  60000/220839          
c   -- var.elim.:  61000/220839          
c   -- var.elim.:  62000/220839          
c   -- var.elim.:  63000/220839          
c   -- var.elim.:  64000/220839          
c   -- var.elim.:  65000/220839          
c   -- var.elim.:  66000/220839          
c   -- var.elim.:  67000/220839          
c   -- var.elim.:  68000/220839          
c   -- var.elim.:  69000/220839          
c   -- var.elim.:  70000/220839          
c   -- var.elim.:  71000/220839          
c   -- var.elim.:  72000/220839          
c   -- var.elim.:  73000/220839          
c   -- var.elim.:  74000/220839          
c   -- var.elim.:  75000/220839          
c   -- var.elim.:  76000/220839          
c   -- var.elim.:  77000/220839          
c   -- var.elim.:  78000/220839          
c   -- var.elim.:  79000/220839          
c   -- var.elim.:  80000/220839          
c   -- var.elim.:  81000/220839          
c   -- var.elim.:  82000/220839          
c   -- var.elim.:  83000/220839          
c   -- var.elim.:  84000/220839          
c   -- var.elim.:  85000/220839          
c   -- var.elim.:  86000/220839          
c   -- var.elim.:  87000/220839          
c   -- var.elim.:  88000/220839          
c   -- var.elim.:  89000/220839          
c   -- var.elim.:  90000/220839          
c   -- var.elim.:  91000/220839          
c   -- var.elim.:  92000/220839          
c   -- var.elim.:  93000/220839          
c   -- var.elim.:  94000/220839          
c   -- var.elim.:  95000/220839          
c   -- var.elim.:  96000/220839          
c   -- var.elim.:  97000/220839          
c   -- var.elim.:  98000/220839          
c   -- var.elim.:  99000/220839          
c   -- var.elim.:  100000/220839          
c   -- var.elim.:  101000/220839          
c   -- var.elim.:  102000/220839          
c   -- var.elim.:  103000/220839          
c   -- var.elim.:  104000/220839          
c   -- var.elim.:  105000/220839          
c   -- var.elim.:  106000/220839          
c   -- var.elim.:  107000/220839          
c   -- var.elim.:  108000/220839          
c   -- var.elim.:  109000/220839          
c   -- var.elim.:  110000/220839          
c   -- var.elim.:  111000/220839          
c   -- var.elim.:  112000/220839          
c   -- var.elim.:  113000/220839          
c   -- var.elim.:  114000/220839          
c   -- var.elim.:  115000/220839          
c   -- var.elim.:  116000/220839          
c   -- var.elim.:  117000/220839          
c   -- var.elim.:  118000/220839          
c   -- var.elim.:  119000/220839          
c   -- var.elim.:  120000/220839          
c   -- var.elim.:  121000/220839          
c   -- var.elim.:  122000/220839          
c   -- var.elim.:  123000/220839          
c   -- var.elim.:  124000/220839          
c   -- var.elim.:  125000/220839          
c   -- var.elim.:  126000/220839          
c   -- var.elim.:  127000/220839          
c   -- var.elim.:  128000/220839          
c   -- var.elim.:  129000/220839          
c   -- var.elim.:  130000/220839          
c   -- var.elim.:  131000/220839          
c   -- var.elim.:  132000/220839          
c   -- var.elim.:  133000/220839          
c   -- var.elim.:  134000/220839          
c   -- var.elim.:  135000/220839          
c   -- var.elim.:  136000/220839          
c   -- var.elim.:  137000/220839          
c   -- var.elim.:  138000/220839          
c   -- var.elim.:  139000/220839          
c   -- var.elim.:  140000/220839          
c   -- var.elim.:  141000/220839          
c   -- var.elim.:  142000/220839          
c   -- var.elim.:  143000/220839          
c   -- var.elim.:  144000/220839          
c   -- var.elim.:  145000/220839          
c   -- var.elim.:  146000/220839          
c   -- var.elim.:  147000/220839          
c   -- var.elim.:  148000/220839          
c   -- var.elim.:  149000/220839          
c   -- var.elim.:  150000/220839          
c   -- var.elim.:  151000/220839          
c   -- var.elim.:  152000/220839          
c   -- var.elim.:  153000/220839          
c   -- var.elim.:  154000/220839          
c   -- var.elim.:  155000/220839          
c   -- var.elim.:  156000/220839          
c   -- var.elim.:  157000/220839          
c   -- var.elim.:  158000/220839          
c   -- var.elim.:  159000/220839          
c   -- var.elim.:  160000/220839          
c   -- var.elim.:  161000/220839          
c   -- var.elim.:  162000/220839          
c   -- var.elim.:  163000/220839          
c   -- var.elim.:  164000/220839          
c   -- var.elim.:  165000/220839          
c   -- var.elim.:  166000/220839          
c   -- var.elim.:  167000/220839          
c   -- var.elim.:  168000/220839          
c   -- var.elim.:  169000/220839          
c   -- var.elim.:  170000/220839          
c   -- var.elim.:  171000/220839          
c   -- var.elim.:  172000/220839          
c   -- var.elim.:  173000/220839          
c   -- var.elim.:  174000/220839          
c   -- var.elim.:  175000/220839          
c   -- var.elim.:  176000/220839          
c   -- var.elim.:  177000/220839          
c   -- var.elim.:  178000/220839          
c   -- var.elim.:  179000/220839          
c   -- var.elim.:  180000/220839          
c   -- var.elim.:  181000/220839          
c   -- var.elim.:  182000/220839          
c   -- var.elim.:  183000/220839          
c   -- var.elim.:  184000/220839          
c   -- var.elim.:  185000/220839          
c   -- var.elim.:  186000/220839          
c   -- var.elim.:  187000/220839          
c   -- var.elim.:  188000/220839          
c   -- var.elim.:  189000/220839          
c   -- var.elim.:  190000/220839          
c   -- var.elim.:  191000/220839          
c   -- var.elim.:  192000/220839          
c   -- var.elim.:  193000/220839          
c   -- var.elim.:  194000/220839          
c   -- var.elim.:  195000/220839          
c   -- var.elim.:  196000/220839          
c   -- var.elim.:  197000/220839          
c   -- var.elim.:  198000/220839          
c   -- var.elim.:  199000/220839          
c   -- var.elim.:  200000/220839          
c   -- var.elim.:  201000/220839          
c   -- var.elim.:  202000/220839          
c   -- var.elim.:  203000/220839          
c   -- var.elim.:  204000/220839          
c   -- var.elim.:  205000/220839          
c   -- var.elim.:  206000/220839          
c   -- var.elim.:  207000/220839          
c   -- var.elim.:  208000/220839          
c   -- var.elim.:  209000/220839          
c   -- var.elim.:  210000/220839          
c   -- var.elim.:  211000/220839          
c   -- var.elim.:  212000/220839          
c   -- var.elim.:  213000/220839          
c   -- var.elim.:  214000/220839          
c   -- var.elim.:  215000/220839          
c   -- var.elim.:  216000/220839          
c   -- var.elim.:  217000/220839          
c   -- var.elim.:  218000/220839          
c   -- var.elim.:  219000/220839          
c   -- var.elim.:  220000/220839          
c   -- var.elim.:  220839/220839          
c   -- var.elim.:  1000/106351          
c   -- var.elim.:  2000/106351          
c   -- var.elim.:  3000/106351          
c   -- var.elim.:  4000/106351          
c   -- var.elim.:  5000/106351          
c   -- var.elim.:  6000/106351          
c   -- var.elim.:  7000/106351          
c   -- var.elim.:  8000/106351          
c   -- var.elim.:  9000/106351          
c   -- var.elim.:  10000/106351          
c   -- var.elim.:  11000/106351          
c   -- var.elim.:  12000/106351          
c   -- var.elim.:  13000/106351          
c   -- var.elim.:  14000/106351          
c   -- var.elim.:  15000/106351          
c   -- var.elim.:  16000/106351          
c   -- var.elim.:  17000/106351          
c   -- var.elim.:  18000/106351          
c   -- var.elim.:  19000/106351          
c   -- var.elim.:  20000/106351          
c   -- var.elim.:  21000/106351          
c   -- var.elim.:  22000/106351          
c   -- var.elim.:  23000/106351          
c   -- var.elim.:  24000/106351          
c   -- var.elim.:  25000/106351          
c   -- var.elim.:  26000/106351          
c   -- var.elim.:  27000/106351          
c   -- var.elim.:  28000/106351          
c   -- var.elim.:  29000/106351          
c   -- var.elim.:  30000/106351          
c   -- var.elim.:  31000/106351          
c   -- var.elim.:  32000/106351          
c   -- var.elim.:  33000/106351          
c   -- var.elim.:  34000/106351          
c   -- var.elim.:  35000/106351          
c   -- var.elim.:  36000/106351          
c   -- var.elim.:  37000/106351          
c   -- var.elim.:  38000/106351          
c   -- var.elim.:  39000/106351          
c   -- var.elim.:  40000/106351          
c   -- var.elim.:  41000/106351          
c   -- var.elim.:  42000/106351          
c   -- var.elim.:  43000/106351          
c   -- var.elim.:  44000/106351          
c   -- var.elim.:  45000/106351          
c   -- var.elim.:  46000/106351          
c   -- var.elim.:  47000/106351          
c   -- var.elim.:  48000/106351          
c   -- var.elim.:  49000/106351          
c   -- var.elim.:  50000/106351          
c   -- var.elim.:  51000/106351          
c   -- var.elim.:  52000/106351          
c   -- var.elim.:  53000/106351          
c   -- var.elim.:  54000/106351          
c   -- var.elim.:  55000/106351          
c   -- var.elim.:  56000/106351          
c   -- var.elim.:  57000/106351          
c   -- var.elim.:  58000/106351          
c   -- var.elim.:  59000/106351          
c   -- var.elim.:  60000/106351          
c   -- var.elim.:  61000/106351          
c   -- var.elim.:  62000/106351          
c   -- var.elim.:  63000/106351          
c   -- var.elim.:  64000/106351          
c   -- var.elim.:  65000/106351          
c   -- var.elim.:  66000/106351          
c   -- var.elim.:  67000/106351          
c   -- var.elim.:  68000/106351          
c   -- var.elim.:  69000/106351          
c   -- var.elim.:  70000/106351          
c   -- var.elim.:  71000/106351          
c   -- var.elim.:  72000/106351          
c   -- var.elim.:  73000/106351          
c   -- var.elim.:  74000/106351          
c   -- var.elim.:  75000/106351          
c   -- var.elim.:  76000/106351          
c   -- var.elim.:  77000/106351          
c   -- var.elim.:  78000/106351          
c   -- var.elim.:  79000/106351          
c   -- var.elim.:  80000/106351          
c   -- var.elim.:  81000/106351          
c   -- var.elim.:  82000/106351          
c   -- var.elim.:  83000/106351          
c   -- var.elim.:  84000/106351          
c   -- var.elim.:  85000/106351          
c   -- var.elim.:  86000/106351          
c   -- var.elim.:  87000/106351          
c   -- var.elim.:  88000/106351          
c   -- var.elim.:  89000/106351          
c   -- var.elim.:  90000/106351          
c   -- var.elim.:  91000/106351          
c   -- var.elim.:  92000/106351          
c   -- var.elim.:  93000/106351          
c   -- var.elim.:  94000/106351          
c   -- var.elim.:  95000/106351          
c   -- var.elim.:  96000/106351          
c   -- var.elim.:  97000/106351          
c   -- var.elim.:  98000/106351          
c   -- var.elim.:  99000/106351          
c   -- var.elim.:  100000/106351          
c   -- var.elim.:  101000/106351          
c   -- var.elim.:  102000/106351          
c   -- var.elim.:  103000/106351          
c   -- var.elim.:  104000/106351          
c   -- var.elim.:  105000/106351          
c   -- var.elim.:  106000/106351          
c   -- var.elim.:  106351/106351          
c   -- var.elim.:  614/614          
c   -- subsuming                       
c   -- var.elim.:  1000/20572          
c   -- var.elim.:  2000/20572          
c   -- var.elim.:  3000/20572          
c   -- var.elim.:  4000/20572          
c   -- var.elim.:  5000/20572          
c   -- var.elim.:  6000/20572          
c   -- var.elim.:  7000/20572          
c   -- var.elim.:  8000/20572          
c   -- var.elim.:  9000/20572          
c   -- var.elim.:  10000/20572          
c   -- var.elim.:  11000/20572          
c   -- var.elim.:  12000/20572          
c   -- var.elim.:  13000/20572          
c   -- var.elim.:  14000/20572          
c   -- var.elim.:  15000/20572          
c   -- var.elim.:  16000/20572          
c   -- var.elim.:  17000/20572          
c   -- var.elim.:  18000/20572          
c   -- var.elim.:  19000/20572          
c   -- var.elim.:  20000/20572          
c   -- var.elim.:  20572/20572          
c   -- var.elim.:  1000/9426          
c   -- var.elim.:  2000/9426          
c   -- var.elim.:  3000/9426          
c   -- var.elim.:  4000/9426          
c   -- var.elim.:  5000/9426          
c   -- var.elim.:  6000/9426          
c   -- var.elim.:  7000/9426          
c   -- var.elim.:  8000/9426          
c   -- var.elim.:  9000/9426          
c   -- var.elim.:  9426/9426          
c   -- subsuming                       
c   -- var.elim.:  1000/6369          
c   -- var.elim.:  2000/6369          
c   -- var.elim.:  3000/6369          
c   -- var.elim.:  4000/6369          
c   -- var.elim.:  5000/6369          
c   -- var.elim.:  6000/6369          
c   -- var.elim.:  6369/6369          
c   -- var.elim.:  432/432          
c   -- subsuming                       
c   -- var.elim.:  162/162          
c |         0 |  662564  2103658 |      --       0       --      -- |     --   | -75006/142103
c |         0 |  662564  2103658 |  265025       0        0     nan |  0.000 % |
c |       101 |  662564  2103658 |  291528     101      431     4.3 |  3.834 % |
c |       251 |  662546  2103542 |  320672   #### 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.78 0.91 0.89 2/54 4702
Raw data (stat): 4702 (runsolver) R 4701 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547596328 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.81 0.91 0.89 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 34154 0 0 0 916 82 0 0 25 0 1 0 547596328 146296832 33441 4294967295 134512640 134672761 3221224544 3221223172 134622553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35717 33441 603 41 0 35676 0
vsize: 142868
[startup+20.0021 s]
Raw data (loadavg): 0.84 0.92 0.89 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 35827 0 0 0 1897 100 0 0 25 0 1 0 547596328 148684800 33951 4294967295 134512640 134672761 3221224544 3221222928 134632058 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36300 33951 603 41 0 36259 0
vsize: 145200
[startup+30.0024 s]
Raw data (loadavg): 0.86 0.92 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 36128 0 0 0 2884 112 0 0 25 0 1 0 547596328 149082112 34004 4294967295 134512640 134672761 3221224544 3221222960 134631410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36397 34004 603 41 0 36356 0
vsize: 145588
[startup+40.0026 s]
Raw data (loadavg): 0.88 0.92 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 39478 0 0 0 3875 121 0 0 25 0 1 0 547596328 147509248 33702 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36013 33702 603 41 0 35972 0
vsize: 144052
[startup+50.0033 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 39567 0 0 0 4874 122 0 0 25 0 1 0 547596328 148004864 33791 4294967295 134512640 134672761 3221224544 3221223688 134616123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36134 33791 603 41 0 36093 0
vsize: 144536
[startup+60.0037 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 39581 0 0 0 5874 122 0 0 25 0 1 0 547596328 148267008 33805 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36198 33805 603 41 0 36157 0
vsize: 144792
[startup+70.004 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 39596 0 0 0 6874 122 0 0 25 0 1 0 547596328 148267008 33820 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36198 33820 603 41 0 36157 0
vsize: 144792
[startup+80.0045 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 39653 0 0 0 7874 122 0 0 25 0 1 0 547596328 148529152 33877 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36262 33877 603 41 0 36221 0
vsize: 145048
[startup+90.005 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 39786 0 0 0 8874 123 0 0 25 0 1 0 547596328 148934656 34010 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36361 34010 603 41 0 36320 0
vsize: 145444
[startup+100.012 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 39851 0 0 0 9874 123 0 0 25 0 1 0 547596328 149331968 34075 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36458 34075 603 41 0 36417 0
vsize: 145832
[startup+110.02 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 39890 0 0 0 10875 123 0 0 25 0 1 0 547596328 149467136 34114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36491 34114 603 41 0 36450 0
vsize: 145964
[startup+120.019 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 39930 0 0 0 11875 123 0 0 25 0 1 0 547596328 149602304 34154 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36524 34154 603 41 0 36483 0
vsize: 146096
[startup+130.02 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 40010 0 0 0 12875 124 0 0 25 0 1 0 547596328 150003712 34234 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36622 34234 603 41 0 36581 0
vsize: 146488
[startup+140.02 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 40040 0 0 0 13875 124 0 0 25 0 1 0 547596328 150003712 34264 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36622 34264 603 41 0 36581 0
vsize: 146488
[startup+150.021 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 40136 0 0 0 14875 124 0 0 25 0 1 0 547596328 150409216 34360 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36721 34360 603 41 0 36680 0
vsize: 146884
[startup+160.021 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 40364 0 0 0 15875 125 0 0 25 0 1 0 547596328 151343104 34588 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36949 34588 603 41 0 36908 0
vsize: 147796
[startup+170.021 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 40583 0 0 0 16874 126 0 0 25 0 1 0 547596328 152399872 34807 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37207 34807 603 41 0 37166 0
vsize: 148828
[startup+180.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 41134 0 0 0 17872 127 0 0 25 0 1 0 547596328 154652672 35358 4294967295 134512640 134672761 3221224544 3221223648 134604297 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37757 35358 603 41 0 37716 0
vsize: 151028
[startup+190.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 41591 0 0 0 18872 128 0 0 25 0 1 0 547596328 156504064 35815 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38209 35815 603 41 0 38168 0
vsize: 152836
[startup+200.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 41783 0 0 0 19871 129 0 0 25 0 1 0 547596328 157298688 36007 4294967295 134512640 134672761 3221224544 3221223808 134617971 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38403 36007 603 41 0 38362 0
vsize: 153612
[startup+210.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 41823 0 0 0 20872 129 0 0 25 0 1 0 547596328 157433856 36047 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38436 36047 603 41 0 38395 0
vsize: 153744
[startup+220.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 41947 0 0 0 21871 129 0 0 25 0 1 0 547596328 157966336 36171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38566 36171 603 41 0 38525 0
vsize: 154264
[startup+230.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 41997 0 0 0 22871 130 0 0 25 0 1 0 547596328 158097408 36221 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38598 36221 603 41 0 38557 0
vsize: 154392
[startup+240.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 42036 0 0 0 23871 130 0 0 25 0 1 0 547596328 158232576 36260 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38631 36260 603 41 0 38590 0
vsize: 154524
[startup+250.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 42344 0 0 0 24871 130 0 0 25 0 1 0 547596328 159563776 36568 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38956 36568 603 41 0 38915 0
vsize: 155824
[startup+260.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 42551 0 0 0 25870 131 0 0 25 0 1 0 547596328 160370688 36775 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39153 36775 603 41 0 39112 0
vsize: 156612
[startup+270.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 42871 0 0 0 26870 131 0 0 25 0 1 0 547596328 161693696 37095 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39476 37095 603 41 0 39435 0
vsize: 157904
[startup+280.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 43130 0 0 0 27870 132 0 0 25 0 1 0 547596328 162779136 37354 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39741 37354 603 41 0 39700 0
vsize: 158964
[startup+290.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 43201 0 0 0 28870 132 0 0 25 0 1 0 547596328 163573760 37425 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39935 37425 603 41 0 39894 0
vsize: 159740
[startup+300.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 43257 0 0 0 29870 132 0 0 25 0 1 0 547596328 163704832 37481 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39967 37481 603 41 0 39926 0
vsize: 159868
[startup+310.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 43314 0 0 0 30870 133 0 0 25 0 1 0 547596328 163971072 37538 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40032 37538 603 41 0 39991 0
vsize: 160128
[startup+320.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 43391 0 0 0 31870 133 0 0 25 0 1 0 547596328 164233216 37615 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40096 37615 603 41 0 40055 0
vsize: 160384
[startup+330.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 43745 0 0 0 32869 134 0 0 25 0 1 0 547596328 165822464 37969 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40484 37969 603 41 0 40443 0
vsize: 161936
[startup+340.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 43833 0 0 0 33869 134 0 0 25 0 1 0 547596328 166088704 38057 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40549 38057 603 41 0 40508 0
vsize: 162196
[startup+350.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 43936 0 0 0 34869 134 0 0 25 0 1 0 547596328 166486016 38160 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40646 38160 603 41 0 40605 0
vsize: 162584
[startup+360.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44001 0 0 0 35869 135 0 0 25 0 1 0 547596328 166756352 38225 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40712 38225 603 41 0 40671 0
vsize: 162848
[startup+370.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44055 0 0 0 36869 135 0 0 25 0 1 0 547596328 167018496 38279 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40776 38279 603 41 0 40735 0
vsize: 163104
[startup+380.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44115 0 0 0 37869 135 0 0 25 0 1 0 547596328 167153664 38339 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40809 38339 603 41 0 40768 0
vsize: 163236
[startup+390.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44150 0 0 0 38870 135 0 0 25 0 1 0 547596328 167284736 38374 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40841 38374 603 41 0 40800 0
vsize: 163364
[startup+400.034 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44231 0 0 0 39870 135 0 0 25 0 1 0 547596328 167550976 38455 4294967295 134512640 134672761 3221224544 3221223744 134610637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40906 38455 603 41 0 40865 0
vsize: 163624
[startup+410.035 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44290 0 0 0 40870 136 0 0 25 0 1 0 547596328 167817216 38514 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40971 38514 603 41 0 40930 0
vsize: 163884
[startup+420.035 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44336 0 0 0 41869 136 0 0 25 0 1 0 547596328 167952384 38560 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41004 38560 603 41 0 40963 0
vsize: 164016
[startup+430.035 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44386 0 0 0 42869 136 0 0 25 0 1 0 547596328 168087552 38610 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41037 38610 603 41 0 40996 0
vsize: 164148
[startup+440.036 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44451 0 0 0 43869 136 0 0 25 0 1 0 547596328 168353792 38675 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41102 38675 603 41 0 41061 0
vsize: 164408
[startup+450.036 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44501 0 0 0 44869 136 0 0 25 0 1 0 547596328 168620032 38725 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41167 38725 603 41 0 41126 0
vsize: 164668
[startup+460.036 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44545 0 0 0 45870 136 0 0 25 0 1 0 547596328 168755200 38769 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41200 38769 603 41 0 41159 0
vsize: 164800
[startup+470.036 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44615 0 0 0 46870 137 0 0 25 0 1 0 547596328 169025536 38839 4294967295 134512640 134672761 3221224544 3221223688 134616339 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41266 38839 603 41 0 41225 0
vsize: 165064
[startup+480.036 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44650 0 0 0 47870 137 0 0 25 0 1 0 547596328 169160704 38874 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41299 38874 603 41 0 41258 0
vsize: 165196
[startup+490.037 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44737 0 0 0 48870 137 0 0 25 0 1 0 547596328 169562112 38961 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41397 38961 603 41 0 41356 0
vsize: 165588
[startup+500.037 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44795 0 0 0 49870 137 0 0 25 0 1 0 547596328 169697280 39019 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41430 39019 603 41 0 41389 0
vsize: 165720
[startup+510.038 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44873 0 0 0 50870 137 0 0 25 0 1 0 547596328 170098688 39097 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41528 39097 603 41 0 41487 0
vsize: 166112
[startup+520.038 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 44992 0 0 0 51869 138 0 0 25 0 1 0 547596328 170500096 39216 4294967295 134512640 134672761 3221224544 3221223808 134618040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41626 39216 603 41 0 41585 0
vsize: 166504
[startup+530.038 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 45045 0 0 0 52869 138 0 0 25 0 1 0 547596328 170676224 39269 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41669 39269 603 41 0 41628 0
vsize: 166676
[startup+540.039 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 45092 0 0 0 53869 138 0 0 25 0 1 0 547596328 170942464 39316 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41734 39316 603 41 0 41693 0
vsize: 166936
[startup+550.038 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 45174 0 0 0 54869 139 0 0 25 0 1 0 547596328 171208704 39398 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41799 39398 603 41 0 41758 0
vsize: 167196
[startup+560.039 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 45228 0 0 0 55869 139 0 0 25 0 1 0 547596328 171474944 39452 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41864 39452 603 41 0 41823 0
vsize: 167456
[startup+570.04 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 45319 0 0 0 56869 139 0 0 25 0 1 0 547596328 171745280 39543 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41930 39543 603 41 0 41889 0
vsize: 167720
[startup+580.039 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 45950 0 0 0 57868 141 0 0 25 0 1 0 547596328 174379008 40174 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42573 40174 603 41 0 42532 0
vsize: 170292
[startup+590.039 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 46079 0 0 0 58867 141 0 0 25 0 1 0 547596328 174907392 40303 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42702 40303 603 41 0 42661 0
vsize: 170808
[startup+600.04 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 46181 0 0 0 59867 142 0 0 25 0 1 0 547596328 175304704 40405 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42799 40405 603 41 0 42758 0
vsize: 171196
[startup+610.041 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 46233 0 0 0 60867 142 0 0 25 0 1 0 547596328 175439872 40457 4294967295 134512640 134672761 3221224544 3221223696 134565089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42832 40457 603 41 0 42791 0
vsize: 171328
[startup+620.042 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 46286 0 0 0 61867 142 0 0 25 0 1 0 547596328 175706112 40510 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42897 40510 603 41 0 42856 0
vsize: 171588
[startup+630.042 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 46596 0 0 0 62866 144 0 0 25 0 1 0 547596328 176898048 40820 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43188 40820 603 41 0 43147 0
vsize: 172752
[startup+640.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 47299 0 0 0 63864 145 0 0 25 0 1 0 547596328 179826688 41523 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43903 41523 603 41 0 43862 0
vsize: 175612
[startup+650.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 47905 0 0 0 64862 147 0 0 25 0 1 0 547596328 182218752 42129 4294967295 134512640 134672761 3221224544 3221223584 134612536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44487 42129 603 41 0 44446 0
vsize: 177948
[startup+660.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 48407 0 0 0 65861 149 0 0 25 0 1 0 547596328 184328192 42631 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45002 42631 603 41 0 44961 0
vsize: 180008
[startup+670.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 48874 0 0 0 66860 150 0 0 25 0 1 0 547596328 186179584 43098 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45454 43098 603 41 0 45413 0
vsize: 181816
[startup+680.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 49226 0 0 0 67859 152 0 0 25 0 1 0 547596328 188682240 43450 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46065 43450 603 41 0 46024 0
vsize: 184260
[startup+690.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 49567 0 0 0 68859 152 0 0 25 0 1 0 547596328 190005248 43791 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46388 43791 603 41 0 46347 0
vsize: 185552
[startup+700.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 49953 0 0 0 69858 153 0 0 25 0 1 0 547596328 191582208 44177 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46773 44177 603 41 0 46732 0
vsize: 187092
[startup+710.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 50239 0 0 0 70857 154 0 0 25 0 1 0 547596328 192782336 44463 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47066 44463 603 41 0 47025 0
vsize: 188264
[startup+720.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 50512 0 0 0 71857 155 0 0 25 0 1 0 547596328 193839104 44736 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47324 44736 603 41 0 47283 0
vsize: 189296
[startup+730.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 50778 0 0 0 72856 156 0 0 25 0 1 0 547596328 195067904 45002 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47624 45002 603 41 0 47583 0
vsize: 190496
[startup+740.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 51071 0 0 0 73855 157 0 0 25 0 1 0 547596328 196255744 45295 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47914 45295 603 41 0 47873 0
vsize: 191656
[startup+750.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 51291 0 0 0 74855 157 0 0 25 0 1 0 547596328 197046272 45515 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48107 45515 603 41 0 48066 0
vsize: 192428
[startup+760.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 51578 0 0 0 75854 159 0 0 25 0 1 0 547596328 198238208 45802 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48398 45802 603 41 0 48357 0
vsize: 193592
[startup+770.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 51799 0 0 0 76853 159 0 0 25 0 1 0 547596328 199159808 46023 4294967295 134512640 134672761 3221224544 3221223680 134614683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48623 46023 603 41 0 48582 0
vsize: 194492
[startup+780.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52026 0 0 0 77853 160 0 0 25 0 1 0 547596328 200081408 46250 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48848 46250 603 41 0 48807 0
vsize: 195392
[startup+790.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52132 0 0 0 78853 160 0 0 25 0 1 0 547596328 200482816 46356 4294967295 134512640 134672761 3221224544 3221223744 134610683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48946 46356 603 41 0 48905 0
vsize: 195784
[startup+800.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52204 0 0 0 79853 161 0 0 25 0 1 0 547596328 200757248 46428 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49013 46428 603 41 0 48972 0
vsize: 196052
[startup+810.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52243 0 0 0 80853 161 0 0 25 0 1 0 547596328 200892416 46467 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49046 46467 603 41 0 49005 0
vsize: 196184
[startup+820.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52288 0 0 0 81853 161 0 0 25 0 1 0 547596328 201162752 46512 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49112 46512 603 41 0 49071 0
vsize: 196448
[startup+830.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52347 0 0 0 82853 161 0 0 25 0 1 0 547596328 201428992 46571 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49177 46571 603 41 0 49136 0
vsize: 196708
[startup+840.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52394 0 0 0 83853 161 0 0 25 0 1 0 547596328 201564160 46618 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49210 46618 603 41 0 49169 0
vsize: 196840
[startup+850.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52440 0 0 0 84853 162 0 0 25 0 1 0 547596328 201695232 46664 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49242 46664 603 41 0 49201 0
vsize: 196968
[startup+860.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52497 0 0 0 85853 162 0 0 25 0 1 0 547596328 201961472 46721 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49307 46721 603 41 0 49266 0
vsize: 197228
[startup+870.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52557 0 0 0 86853 162 0 0 25 0 1 0 547596328 202227712 46781 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49372 46781 603 41 0 49331 0
vsize: 197488
[startup+880.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52696 0 0 0 87852 162 0 0 25 0 1 0 547596328 202760192 46920 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49502 46920 603 41 0 49461 0
vsize: 198008
[startup+890.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52741 0 0 0 88852 163 0 0 25 0 1 0 547596328 202891264 46965 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49534 46965 603 41 0 49493 0
vsize: 198136
[startup+900.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52791 0 0 0 89852 163 0 0 25 0 1 0 547596328 203161600 47015 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49600 47015 603 41 0 49559 0
vsize: 198400
[startup+910.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52859 0 0 0 90852 163 0 0 25 0 1 0 547596328 203427840 47083 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49665 47083 603 41 0 49624 0
vsize: 198660
[startup+920.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52917 0 0 0 91853 163 0 0 25 0 1 0 547596328 203558912 47141 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49697 47141 603 41 0 49656 0
vsize: 198788
[startup+930.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 52970 0 0 0 92853 163 0 0 25 0 1 0 547596328 203829248 47194 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49763 47194 603 41 0 49722 0
vsize: 199052
[startup+940.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 53031 0 0 0 93852 164 0 0 25 0 1 0 547596328 204095488 47255 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49828 47255 603 41 0 49787 0
vsize: 199312
[startup+950.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 53151 0 0 0 94852 164 0 0 25 0 1 0 547596328 204500992 47375 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49927 47375 603 41 0 49886 0
vsize: 199708
[startup+960.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 53258 0 0 0 95852 164 0 0 25 0 1 0 547596328 205033472 47482 4294967295 134512640 134672761 3221224544 3221223584 134612739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50057 47482 603 41 0 50016 0
vsize: 200228
[startup+970.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 53455 0 0 0 96852 165 0 0 25 0 1 0 547596328 205701120 47679 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50220 47679 603 41 0 50179 0
vsize: 200880
[startup+980.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 53662 0 0 0 97852 165 0 0 25 0 1 0 547596328 206635008 47886 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50448 47886 603 41 0 50407 0
vsize: 201792
[startup+990.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 53812 0 0 0 98851 166 0 0 25 0 1 0 547596328 207163392 48036 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50577 48036 603 41 0 50536 0
vsize: 202308
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 53877 0 0 0 99851 166 0 0 25 0 1 0 547596328 207433728 48101 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50643 48101 603 41 0 50602 0
vsize: 202572
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 53951 0 0 0 100851 167 0 0 25 0 1 0 547596328 207704064 48175 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50709 48175 603 41 0 50668 0
vsize: 202836
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 54030 0 0 0 101852 167 0 0 25 0 1 0 547596328 208109568 48254 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50808 48254 603 41 0 50767 0
vsize: 203232
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 54119 0 0 0 102851 167 0 0 25 0 1 0 547596328 208379904 48343 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50874 48343 603 41 0 50833 0
vsize: 203496
[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 54225 0 0 0 103852 168 0 0 25 0 1 0 547596328 208785408 48449 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50973 48449 603 41 0 50932 0
vsize: 203892
[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 54375 0 0 0 104851 168 0 0 25 0 1 0 547596328 209448960 48599 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51135 48599 603 41 0 51094 0
vsize: 204540
[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 54434 0 0 0 105851 168 0 0 25 0 1 0 547596328 209584128 48658 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51168 48658 603 41 0 51127 0
vsize: 204672
[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 54584 0 0 0 106850 169 0 0 25 0 1 0 547596328 210251776 48808 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51331 48808 603 41 0 51290 0
vsize: 205324
[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 54787 0 0 0 107851 170 0 0 25 0 1 0 547596328 211054592 49011 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51527 49011 603 41 0 51486 0
vsize: 206108
[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 55074 0 0 0 108853 171 0 0 25 0 1 0 547596328 212238336 49298 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51816 49298 603 41 0 51775 0
vsize: 207264
[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 55324 0 0 0 109852 171 0 0 25 0 1 0 547596328 213172224 49548 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52044 49548 603 41 0 52003 0
vsize: 208176
[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 55561 0 0 0 110853 171 0 0 25 0 1 0 547596328 214241280 49785 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52305 49785 603 41 0 52264 0
vsize: 209220
[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 55818 0 0 0 111852 172 0 0 25 0 1 0 547596328 215179264 50042 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52534 50042 603 41 0 52493 0
vsize: 210136
[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 56014 0 0 0 112851 173 0 0 25 0 1 0 547596328 215977984 50238 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52729 50238 603 41 0 52688 0
vsize: 210916
[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 56189 0 0 0 113851 173 0 0 25 0 1 0 547596328 216657920 50413 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52895 50413 603 41 0 52854 0
vsize: 211580
[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 56352 0 0 0 114851 173 0 0 25 0 1 0 547596328 217325568 50576 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53058 50576 603 41 0 53017 0
vsize: 212232
[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 56500 0 0 0 115851 174 0 0 25 0 1 0 547596328 218009600 50724 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53225 50724 603 41 0 53184 0
vsize: 212900
[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 56660 0 0 0 116850 175 0 0 25 0 1 0 547596328 218701824 50884 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53394 50884 603 41 0 53353 0
vsize: 213576
[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 56811 0 0 0 117850 175 0 0 25 0 1 0 547596328 219238400 51035 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53525 51035 603 41 0 53484 0
vsize: 214100
[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 56960 0 0 0 118849 176 0 0 25 0 1 0 547596328 219897856 51184 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53686 51184 603 41 0 53645 0
vsize: 214744
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 4702
Raw data (stat): 4702 (minisat+) R 4701 27222 27221 0 -1 0 57137 0 0 0 119850 176 0 0 25 0 1 0 547596328 220741632 51361 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53892 51361 603 41 0 53851 0
vsize: 215568
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.35 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 4702
Raw data (stat): 4702 (minisat+) Z 4701 27222 27221 0 -1 12 57137 0 0 0 119850 188 0 0 24 0 1 0 547596328 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.35
CPU time (s): 1200.39
CPU user time (s): 1198.51
CPU system time (s): 1.88071
CPU usage (%): 100.004
Max. virtual memory (Kb): 215568
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####