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 16058

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 06:11:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16315 boxname=wulflinc28 idbench=1255 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6d2898572483dddc248ecc48cac97a0c  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-sctap1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-sctap1.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-sctap1.opb
IDLAUNCH: 16315
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        734320 kB
Buffers:         22552 kB
Cached:         250364 kB
SwapCached:        104 kB
Active:          54680 kB
Inactive:       220684 kB
HighTotal:      131008 kB
HighFree:        19740 kB
LowTotal:       903652 kB
LowFree:        714580 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            19180 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:31:19 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 16315 7 1200.33 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  787008  2103907 |  262336       0        0     nan |  0.000 % |
c |       100 |  787008  2103907 |  288569     100      308     3.1 |  2.213 % |
c |       250 |  787008  2103907 |  317426     250     1555     6.2 |  2.213 % |
c |       475 |  786981  2103847 |  349169     474     2859     6.0 |  2.216 % |
c |       812 |  786981  2103847 |  384086     811     6843     8.4 |  2.216 % |
c |      1318 |  786981  2103847 |  422494    1317    12209     9.3 |  2.216 % |
c |      2077 |  786941  2103758 |  464744    2075    18313     8.8 |  2.221 % |
c |      3216 |  786802  2103446 |  511218    3204    25805     8.1 |  2.237 % |
c |      4924 |  786802  2103446 |  562340    4912    42820     8.7 |  2.237 % |
c |      7486 |  786661  2103133 |  618574    7467    62712     8.4 |  2.253 % |
c |     11330 |  786003  2101667 |  680432   11278    92567     8.2 |  2.329 % |
c |     17096 |  785643  2100865 |  748475   17034   130384     7.7 |  2.369 % |
c |     25745 |  784891  2099193 |  823322   25659   206405     8.0 |  2.453 % |
c |     38719 |  784288  2097855 |  905655   38608   432242    11.2 |  2.520 % |
c |     58180 |  781968  2092671 |  996220   57984   685481    11.8 |  2.785 % |
c |     87372 |  777206  2082014 | 1095842   86935  1005282    11.6 |  3.336 % |
c |    131161 |  773924  2074627 | 1205426  130530  2026242    15.5 |  3.720 % |
c |    196847 |  771222  2068536 | 1325969  196047  3552864    18.1 |  4.042 % |
c |    295376 |  765722  2056115 | 1458566  294230  5831837    19.8 |  4.705 % |
#### 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.86 0.94 0.91 2/54 20143
Raw data (stat): 20143 (runsolver) R 20142 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542822591 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+9.99959 s]
Raw data (loadavg): 0.88 0.94 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 19788 0 0 0 952 46 0 0 25 0 1 0 542822591 83935232 19074 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20492 19074 603 41 0 20451 0
vsize: 81968
[startup+20.0006 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 19960 0 0 0 1951 47 0 0 25 0 1 0 542822591 84475904 19246 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20624 19246 603 41 0 20583 0
vsize: 82496
[startup+30.0011 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20060 0 0 0 2951 47 0 0 25 0 1 0 542822591 84881408 19346 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20723 19346 603 41 0 20682 0
vsize: 82892
[startup+40.0017 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20120 0 0 0 3950 48 0 0 25 0 1 0 542822591 85016576 19406 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20756 19406 603 41 0 20715 0
vsize: 83024
[startup+50.0026 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20226 0 0 0 4949 49 0 0 25 0 1 0 542822591 85286912 19512 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20822 19512 603 41 0 20781 0
vsize: 83288
[startup+60.002 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20265 0 0 0 5949 49 0 0 25 0 1 0 542822591 85557248 19551 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20888 19551 603 41 0 20847 0
vsize: 83552
[startup+70.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20297 0 0 0 6950 49 0 0 25 0 1 0 542822591 85704704 19583 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20924 19583 603 41 0 20883 0
vsize: 83696
[startup+80.0037 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20335 0 0 0 7950 49 0 0 25 0 1 0 542822591 85839872 19621 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20957 19621 603 41 0 20916 0
vsize: 83828
[startup+90.0041 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20369 0 0 0 8950 49 0 0 25 0 1 0 542822591 85975040 19655 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20990 19655 603 41 0 20949 0
vsize: 83960
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20413 0 0 0 9950 49 0 0 25 0 1 0 542822591 86110208 19699 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21023 19699 603 41 0 20982 0
vsize: 84092
[startup+110.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20473 0 0 0 10950 49 0 0 25 0 1 0 542822591 86380544 19759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21089 19759 603 41 0 21048 0
vsize: 84356
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20562 0 0 0 11950 49 0 0 25 0 1 0 542822591 86646784 19848 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21154 19848 603 41 0 21113 0
vsize: 84616
[startup+130.004 s]
Raw data (loadavg): 1.06 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20721 0 0 0 12950 50 0 0 25 0 1 0 542822591 87449600 20007 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21350 20007 603 41 0 21309 0
vsize: 85400
[startup+140.004 s]
Raw data (loadavg): 1.05 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20786 0 0 0 13950 50 0 0 25 0 1 0 542822591 87715840 20072 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21415 20072 603 41 0 21374 0
vsize: 85660
[startup+150.004 s]
Raw data (loadavg): 1.04 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20832 0 0 0 14949 51 0 0 25 0 1 0 542822591 87846912 20118 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21447 20118 603 41 0 21406 0
vsize: 85788
[startup+160.004 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20875 0 0 0 15949 51 0 0 25 0 1 0 542822591 88117248 20161 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21513 20161 603 41 0 21472 0
vsize: 86052
[startup+170.005 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20909 0 0 0 16949 51 0 0 25 0 1 0 542822591 88252416 20195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21546 20195 603 41 0 21505 0
vsize: 86184
[startup+180.005 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20943 0 0 0 17949 51 0 0 25 0 1 0 542822591 88387584 20229 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21579 20229 603 41 0 21538 0
vsize: 86316
[startup+190.005 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 20975 0 0 0 18949 51 0 0 25 0 1 0 542822591 88522752 20261 4294967295 134512640 134672761 3221224544 3221223712 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21612 20261 603 41 0 21571 0
vsize: 86448
[startup+200.005 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21018 0 0 0 19949 51 0 0 25 0 1 0 542822591 88657920 20304 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21645 20304 603 41 0 21604 0
vsize: 86580
[startup+210.005 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21047 0 0 0 20950 52 0 0 25 0 1 0 542822591 88657920 20333 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21645 20333 603 41 0 21604 0
vsize: 86580
[startup+220.005 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21078 0 0 0 21950 52 0 0 25 0 1 0 542822591 88788992 20364 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21677 20364 603 41 0 21636 0
vsize: 86708
[startup+230.005 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21105 0 0 0 22950 52 0 0 25 0 1 0 542822591 88924160 20391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21710 20391 603 41 0 21669 0
vsize: 86840
[startup+240.005 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21148 0 0 0 23950 52 0 0 25 0 1 0 542822591 89055232 20434 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21742 20434 603 41 0 21701 0
vsize: 86968
[startup+250.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21331 0 0 0 24949 53 0 0 25 0 1 0 542822591 89862144 20617 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21939 20617 603 41 0 21898 0
vsize: 87756
[startup+260.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21359 0 0 0 25949 53 0 0 25 0 1 0 542822591 89862144 20645 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21939 20645 603 41 0 21898 0
vsize: 87756
[startup+270.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21416 0 0 0 26949 53 0 0 25 0 1 0 542822591 90132480 20702 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22005 20702 603 41 0 21964 0
vsize: 88020
[startup+280.003 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21549 0 0 0 27949 53 0 0 25 0 1 0 542822591 90931200 20835 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22200 20835 603 41 0 22159 0
vsize: 88800
[startup+290.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21568 0 0 0 28949 53 0 0 25 0 1 0 542822591 90931200 20854 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22200 20854 603 41 0 22159 0
vsize: 88800
[startup+300.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21604 0 0 0 29949 53 0 0 25 0 1 0 542822591 91201536 20890 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22266 20890 603 41 0 22225 0
vsize: 89064
[startup+310.003 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21637 0 0 0 30949 54 0 0 25 0 1 0 542822591 91201536 20923 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22266 20923 603 41 0 22225 0
vsize: 89064
[startup+320.003 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21669 0 0 0 31949 54 0 0 25 0 1 0 542822591 91332608 20955 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22298 20955 603 41 0 22257 0
vsize: 89192
[startup+330.003 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21699 0 0 0 32949 54 0 0 25 0 1 0 542822591 91467776 20985 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22331 20985 603 41 0 22290 0
vsize: 89324
[startup+340.003 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21730 0 0 0 33949 54 0 0 25 0 1 0 542822591 91598848 21016 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22363 21016 603 41 0 22322 0
vsize: 89452
[startup+350.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21764 0 0 0 34949 54 0 0 25 0 1 0 542822591 91734016 21050 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22396 21050 603 41 0 22355 0
vsize: 89584
[startup+360.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21798 0 0 0 35950 54 0 0 25 0 1 0 542822591 91869184 21084 4294967295 134512640 134672761 3221224544 3221223668 134566145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22429 21084 603 41 0 22388 0
vsize: 89716
[startup+370.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21839 0 0 0 36950 54 0 0 25 0 1 0 542822591 92000256 21125 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22461 21125 603 41 0 22420 0
vsize: 89844
[startup+380.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21854 0 0 0 37950 54 0 0 25 0 1 0 542822591 92000256 21140 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22461 21140 603 41 0 22420 0
vsize: 89844
[startup+390.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 21936 0 0 0 38949 54 0 0 25 0 1 0 542822591 92401664 21222 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22559 21222 603 41 0 22518 0
vsize: 90236
[startup+400.007 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 22007 0 0 0 39949 55 0 0 25 0 1 0 542822591 92672000 21293 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22625 21293 603 41 0 22584 0
vsize: 90500
[startup+410.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 22064 0 0 0 40949 55 0 0 25 0 1 0 542822591 92807168 21350 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22658 21350 603 41 0 22617 0
vsize: 90632
[startup+420.007 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 22184 0 0 0 41949 55 0 0 25 0 1 0 542822591 93339648 21470 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22788 21470 603 41 0 22747 0
vsize: 91152
[startup+430.007 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 22286 0 0 0 42949 55 0 0 25 0 1 0 542822591 93745152 21572 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22887 21572 603 41 0 22846 0
vsize: 91548
[startup+440.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 22402 0 0 0 43950 56 0 0 25 0 1 0 542822591 94146560 21688 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22985 21688 603 41 0 22944 0
vsize: 91940
[startup+450.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 22941 0 0 0 44948 57 0 0 25 0 1 0 542822591 96301056 22227 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23511 22227 603 41 0 23470 0
vsize: 94044
[startup+460.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 23215 0 0 0 45947 58 0 0 25 0 1 0 542822591 97517568 22501 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23808 22501 603 41 0 23767 0
vsize: 95232
[startup+470.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 23248 0 0 0 46948 58 0 0 25 0 1 0 542822591 97648640 22534 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23840 22534 603 41 0 23799 0
vsize: 95360
[startup+480.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 23267 0 0 0 47948 59 0 0 25 0 1 0 542822591 97648640 22553 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23840 22553 603 41 0 23799 0
vsize: 95360
[startup+490.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 23284 0 0 0 48948 59 0 0 25 0 1 0 542822591 97783808 22570 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23873 22570 603 41 0 23832 0
vsize: 95492
[startup+500.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 23311 0 0 0 49948 59 0 0 25 0 1 0 542822591 97783808 22597 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23873 22597 603 41 0 23832 0
vsize: 95492
[startup+510.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 23370 0 0 0 50948 59 0 0 25 0 1 0 542822591 98050048 22656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22656 603 41 0 23897 0
vsize: 95752
[startup+520.016 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 23592 0 0 0 51947 60 0 0 25 0 1 0 542822591 99520512 22878 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24297 22878 603 41 0 24256 0
vsize: 97188
[startup+530.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 23668 0 0 0 52947 60 0 0 25 0 1 0 542822591 99790848 22954 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24363 22954 603 41 0 24322 0
vsize: 97452
[startup+540.016 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 24072 0 0 0 53945 62 0 0 25 0 1 0 542822591 101408768 23358 4294967295 134512640 134672761 3221224544 3221223648 134555089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24758 23358 603 41 0 24717 0
vsize: 99032
[startup+550.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 24367 0 0 0 54944 64 0 0 25 0 1 0 542822591 102621184 23653 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25054 23653 603 41 0 25013 0
vsize: 100216
[startup+560.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 24484 0 0 0 55944 64 0 0 25 0 1 0 542822591 103034880 23770 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25155 23770 603 41 0 25114 0
vsize: 100620
[startup+570.016 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 24533 0 0 0 56944 64 0 0 25 0 1 0 542822591 103170048 23819 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25188 23819 603 41 0 25147 0
vsize: 100752
[startup+580.019 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 24561 0 0 0 57944 64 0 0 25 0 1 0 542822591 103305216 23847 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25221 23847 603 41 0 25180 0
vsize: 100884
[startup+590.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 24591 0 0 0 58944 64 0 0 25 0 1 0 542822591 103440384 23877 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25254 23877 603 41 0 25213 0
vsize: 101016
[startup+600.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 24614 0 0 0 59944 64 0 0 25 0 1 0 542822591 103575552 23900 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25287 23900 603 41 0 25246 0
vsize: 101148
[startup+610.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 24647 0 0 0 60945 64 0 0 25 0 1 0 542822591 103710720 23933 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25320 23933 603 41 0 25279 0
vsize: 101280
[startup+620.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 24690 0 0 0 61944 65 0 0 25 0 1 0 542822591 103845888 23976 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25353 23976 603 41 0 25312 0
vsize: 101412
[startup+630.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25001 0 0 0 62943 66 0 0 25 0 1 0 542822591 105062400 24287 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25650 24287 603 41 0 25609 0
vsize: 102600
[startup+640.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25157 0 0 0 63943 67 0 0 25 0 1 0 542822591 105738240 24443 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25815 24443 603 41 0 25774 0
vsize: 103260
[startup+650.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25303 0 0 0 64942 68 0 0 25 0 1 0 542822591 106278912 24589 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25947 24589 603 41 0 25906 0
vsize: 103788
[startup+660.024 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25364 0 0 0 65942 68 0 0 25 0 1 0 542822591 106545152 24650 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26012 24650 603 41 0 25971 0
vsize: 104048
[startup+670.024 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25440 0 0 0 66943 68 0 0 25 0 1 0 542822591 106815488 24726 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26078 24726 603 41 0 26037 0
vsize: 104312
[startup+680.024 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25636 0 0 0 67942 69 0 0 25 0 1 0 542822591 107618304 24922 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26274 24922 603 41 0 26233 0
vsize: 105096
[startup+690.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25686 0 0 0 68942 69 0 0 25 0 1 0 542822591 107753472 24972 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26307 24972 603 41 0 26266 0
vsize: 105228
[startup+700.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25822 0 0 0 69941 69 0 0 25 0 1 0 542822591 108290048 25108 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26438 25108 603 41 0 26397 0
vsize: 105752
[startup+710.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25851 0 0 0 70942 69 0 0 25 0 1 0 542822591 108425216 25137 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26471 25137 603 41 0 26430 0
vsize: 105884
[startup+720.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25880 0 0 0 71942 69 0 0 25 0 1 0 542822591 108560384 25166 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26504 25166 603 41 0 26463 0
vsize: 106016
[startup+730.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25897 0 0 0 72942 70 0 0 25 0 1 0 542822591 108560384 25183 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26504 25183 603 41 0 26463 0
vsize: 106016
[startup+740.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 25936 0 0 0 73942 70 0 0 25 0 1 0 542822591 108830720 25222 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26570 25222 603 41 0 26529 0
vsize: 106280
[startup+750.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 26146 0 0 0 74941 71 0 0 25 0 1 0 542822591 109641728 25432 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26768 25432 603 41 0 26727 0
vsize: 107072
[startup+760.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 26168 0 0 0 75941 71 0 0 25 0 1 0 542822591 109641728 25454 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26768 25454 603 41 0 26727 0
vsize: 107072
[startup+770.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 26197 0 0 0 76941 71 0 0 25 0 1 0 542822591 109776896 25483 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26801 25483 603 41 0 26760 0
vsize: 107204
[startup+780.027 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 26242 0 0 0 77941 71 0 0 25 0 1 0 542822591 110047232 25528 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26867 25528 603 41 0 26826 0
vsize: 107468
[startup+790.038 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 26497 0 0 0 78942 72 0 0 25 0 1 0 542822591 110985216 25783 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27096 25783 603 41 0 27055 0
vsize: 108384
[startup+800.038 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 26669 0 0 0 79941 73 0 0 25 0 1 0 542822591 111661056 25955 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27261 25955 603 41 0 27220 0
vsize: 109044
[startup+810.038 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 26715 0 0 0 80941 73 0 0 25 0 1 0 542822591 111931392 26001 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27327 26001 603 41 0 27286 0
vsize: 109308
[startup+820.039 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 26761 0 0 0 81941 73 0 0 25 0 1 0 542822591 112066560 26047 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27360 26047 603 41 0 27319 0
vsize: 109440
[startup+830.039 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 26802 0 0 0 82941 73 0 0 25 0 1 0 542822591 112201728 26088 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27393 26088 603 41 0 27352 0
vsize: 109572
[startup+840.045 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27009 0 0 0 83942 73 0 0 25 0 1 0 542822591 113008640 26295 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27590 26295 603 41 0 27549 0
vsize: 110360
[startup+850.062 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27104 0 0 0 84944 73 0 0 25 0 1 0 542822591 113410048 26390 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27688 26390 603 41 0 27647 0
vsize: 110752
[startup+860.075 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27352 0 0 0 85944 74 0 0 25 0 1 0 542822591 114487296 26638 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27951 26638 603 41 0 27910 0
vsize: 111804
[startup+870.078 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27639 0 0 0 86943 76 0 0 25 0 1 0 542822591 115564544 26925 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28214 26925 603 41 0 28173 0
vsize: 112856
[startup+880.079 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27680 0 0 0 87943 76 0 0 25 0 1 0 542822591 115699712 26966 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28247 26966 603 41 0 28206 0
vsize: 112988
[startup+890.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27723 0 0 0 88944 76 0 0 25 0 1 0 542822591 115970048 27009 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28313 27009 603 41 0 28272 0
vsize: 113252
[startup+900.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27780 0 0 0 89944 76 0 0 25 0 1 0 542822591 116105216 27066 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28346 27066 603 41 0 28305 0
vsize: 113384
[startup+910.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27828 0 0 0 90943 76 0 0 25 0 1 0 542822591 116375552 27114 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28412 27114 603 41 0 28371 0
vsize: 113648
[startup+920.081 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27957 0 0 0 91943 77 0 0 25 0 1 0 542822591 117821440 27243 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28765 27243 603 41 0 28724 0
vsize: 115060
[startup+930.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 27989 0 0 0 92943 77 0 0 25 0 1 0 542822591 117956608 27275 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28798 27275 603 41 0 28757 0
vsize: 115192
[startup+940.082 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28012 0 0 0 93943 77 0 0 25 0 1 0 542822591 118091776 27298 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28831 27298 603 41 0 28790 0
vsize: 115324
[startup+950.082 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28190 0 0 0 94943 78 0 0 25 0 1 0 542822591 118767616 27476 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28996 27476 603 41 0 28955 0
vsize: 115984
[startup+960.082 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28235 0 0 0 95943 78 0 0 25 0 1 0 542822591 119037952 27521 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29062 27521 603 41 0 29021 0
vsize: 116248
[startup+970.082 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28292 0 0 0 96943 78 0 0 25 0 1 0 542822591 119173120 27578 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29095 27578 603 41 0 29054 0
vsize: 116380
[startup+980.082 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28434 0 0 0 97943 78 0 0 25 0 1 0 542822591 119705600 27720 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29225 27720 603 41 0 29184 0
vsize: 116900
[startup+990.083 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28508 0 0 0 98943 78 0 0 25 0 1 0 542822591 120111104 27794 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29324 27794 603 41 0 29283 0
vsize: 117296
[startup+1000.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28576 0 0 0 99943 79 0 0 25 0 1 0 542822591 120381440 27862 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29390 27862 603 41 0 29349 0
vsize: 117560
[startup+1010.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28615 0 0 0 100943 79 0 0 25 0 1 0 542822591 120516608 27901 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29423 27901 603 41 0 29382 0
vsize: 117692
[startup+1020.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28662 0 0 0 101943 79 0 0 25 0 1 0 542822591 120651776 27948 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29456 27948 603 41 0 29415 0
vsize: 117824
[startup+1030.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28696 0 0 0 102943 79 0 0 25 0 1 0 542822591 120786944 27982 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29489 27982 603 41 0 29448 0
vsize: 117956
[startup+1040.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28722 0 0 0 103943 79 0 0 25 0 1 0 542822591 120922112 28008 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29522 28008 603 41 0 29481 0
vsize: 118088
[startup+1050.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28764 0 0 0 104943 79 0 0 25 0 1 0 542822591 121053184 28050 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29554 28050 603 41 0 29513 0
vsize: 118216
[startup+1060.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 28884 0 0 0 105942 80 0 0 25 0 1 0 542822591 121593856 28170 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29686 28170 603 41 0 29645 0
vsize: 118744
[startup+1070.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 29252 0 0 0 106943 80 0 0 25 0 1 0 542822591 123068416 28538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30046 28538 603 41 0 30005 0
vsize: 120184
[startup+1080.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 29396 0 0 0 107942 81 0 0 25 0 1 0 542822591 123604992 28682 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30177 28682 603 41 0 30136 0
vsize: 120708
[startup+1090.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 29464 0 0 0 108942 81 0 0 25 0 1 0 542822591 123871232 28750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30242 28750 603 41 0 30201 0
vsize: 120968
[startup+1100.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 29714 0 0 0 109942 81 0 0 25 0 1 0 542822591 124928000 29000 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30500 29000 603 41 0 30459 0
vsize: 122000
[startup+1110.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 29875 0 0 0 110942 82 0 0 25 0 1 0 542822591 125456384 29161 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30629 29161 603 41 0 30588 0
vsize: 122516
[startup+1120.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 29911 0 0 0 111942 82 0 0 25 0 1 0 542822591 125591552 29197 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30662 29197 603 41 0 30621 0
vsize: 122648
[startup+1130.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 29949 0 0 0 112942 82 0 0 25 0 1 0 542822591 125861888 29235 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30728 29235 603 41 0 30687 0
vsize: 122912
[startup+1140.09 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 29977 0 0 0 113942 82 0 0 25 0 1 0 542822591 125861888 29263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30728 29263 603 41 0 30687 0
vsize: 122912
[startup+1150.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 30017 0 0 0 114942 82 0 0 25 0 1 0 542822591 126132224 29303 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30794 29303 603 41 0 30753 0
vsize: 123176
[startup+1160.08 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 30049 0 0 0 115942 82 0 0 25 0 1 0 542822591 126132224 29335 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30794 29335 603 41 0 30753 0
vsize: 123176
[startup+1170.09 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 30082 0 0 0 116943 82 0 0 25 0 1 0 542822591 126267392 29368 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30827 29368 603 41 0 30786 0
vsize: 123308
[startup+1180.09 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 30251 0 0 0 117943 82 0 0 25 0 1 0 542822591 126939136 29537 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30991 29537 603 41 0 30950 0
vsize: 123964
[startup+1190.09 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 30452 0 0 0 118943 83 0 0 25 0 1 0 542822591 127746048 29738 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31188 29738 603 41 0 31147 0
vsize: 124752
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 20143
Raw data (stat): 20143 (minisat+) R 20142 10614 10613 0 -1 0 30520 0 0 0 119944 83 0 0 25 0 1 0 542822591 128016384 29806 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31254 29806 603 41 0 31213 0
vsize: 125016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.97 0.92 1/54 20143
Raw data (stat): 20143 (minisat+) Z 20142 10614 10613 0 -1 12 30522 0 0 0 119944 89 0 0 24 0 1 0 542822591 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.17
CPU time (s): 1200.33
CPU user time (s): 1199.44
CPU system time (s): 0.891864
CPU usage (%): 100.013
Max. virtual memory (Kb): 125016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####