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 19696

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        620904 kB
Buffers:         29540 kB
Cached:         358476 kB
SwapCached:        536 kB
Active:          46296 kB
Inactive:       343868 kB
HighTotal:      131008 kB
HighFree:          336 kB
LowTotal:       903652 kB
LowFree:        620568 kB
SwapTotal:     2097136 kB
SwapFree:      2095852 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            17980 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 19:48:59 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 16307 7 1200.26 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 |  737570  1962473 |  245856       0        0     nan |  0.000 % |
c |       100 |  737570  1962473 |  270441     100      303     3.0 |  2.213 % |
c |       250 |  737570  1962473 |  297485     250     1359     5.4 |  2.213 % |
c |       475 |  737480  1962274 |  327234     464     2850     6.1 |  2.225 % |
c |       812 |  737480  1962274 |  359957     801     5368     6.7 |  2.225 % |
c |      1318 |  737393  1962084 |  395953    1302    10403     8.0 |  2.237 % |
c |      2077 |  737372  1962038 |  435548    2060    16010     7.8 |  2.239 % |
c |      3217 |  737332  1961949 |  479103    3199    25873     8.1 |  2.244 % |
c |      4925 |  737328  1961940 |  527014    4906    42291     8.6 |  2.244 % |
c |      7487 |  736894  1960980 |  579715    7445    70975     9.5 |  2.298 % |
c |     11331 |  736441  1959974 |  637687   11267   116725    10.4 |  2.354 % |
c |     17097 |  736011  1959018 |  701455   17011   189025    11.1 |  2.405 % |
c |     25746 |  735783  1958513 |  771601   25650   340902    13.3 |  2.433 % |
c |     38720 |  734802  1956342 |  848761   38584   530877    13.8 |  2.551 % |
c |     58183 |  733625  1953719 |  933637   57989   937432    16.2 |  2.692 % |
c |     87375 |  729949  1945555 | 1027001   87031  1287153    14.8 |  3.131 % |
c |    131164 |  725405  1935449 | 1129701  130597  1857353    14.2 |  3.686 % |
c |    196849 |  721369  1926446 | 1242671  196014  2756586    14.1 |  4.198 % |
c |    295375 |  717812  1918495 | 1366939  294336  4699345    16.0 |  4.647 % |
#### 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.79 0.95 0.93 2/54 10745
Raw data (stat): 10745 (runsolver) R 10744 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547603925 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.82 0.95 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 19525 0 0 0 951 47 0 0 25 0 1 0 547603925 83304448 18811 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20338 18811 603 41 0 20297 0
vsize: 81352
[startup+20.0013 s]
Raw data (loadavg): 0.85 0.95 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 19723 0 0 0 1950 48 0 0 25 0 1 0 547603925 83980288 19009 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20503 19009 603 41 0 20462 0
vsize: 82012
[startup+30.0014 s]
Raw data (loadavg): 0.87 0.95 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 19903 0 0 0 2949 49 0 0 25 0 1 0 547603925 84541440 19189 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20640 19189 603 41 0 20599 0
vsize: 82560
[startup+40.0022 s]
Raw data (loadavg): 0.89 0.95 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 19986 0 0 0 3947 49 0 0 25 0 1 0 547603925 84946944 19272 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20739 19272 603 41 0 20698 0
vsize: 82956
[startup+50.0024 s]
Raw data (loadavg): 0.90 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 20165 0 0 0 4946 51 0 0 25 0 1 0 547603925 85639168 19451 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20908 19451 603 41 0 20867 0
vsize: 83632
[startup+60.0035 s]
Raw data (loadavg): 0.92 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 20311 0 0 0 5945 52 0 0 25 0 1 0 547603925 86175744 19597 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 19597 603 41 0 20998 0
vsize: 84156
[startup+70.004 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 20422 0 0 0 6945 53 0 0 25 0 1 0 547603925 86581248 19708 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21138 19708 603 41 0 21097 0
vsize: 84552
[startup+80.0042 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 20490 0 0 0 7944 53 0 0 25 0 1 0 547603925 86847488 19776 4294967295 134512640 134672761 3221224624 3221223748 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21203 19776 603 41 0 21162 0
vsize: 84812
[startup+90.0045 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 20627 0 0 0 8943 54 0 0 25 0 1 0 547603925 87515136 19913 4294967295 134512640 134672761 3221224624 3221223816 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21366 19913 603 41 0 21325 0
vsize: 85464
[startup+100.005 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 20702 0 0 0 9943 54 0 0 25 0 1 0 547603925 87785472 19988 4294967295 134512640 134672761 3221224624 3221223748 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21432 19988 603 41 0 21391 0
vsize: 85728
[startup+110.005 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 20793 0 0 0 10943 55 0 0 25 0 1 0 547603925 88186880 20079 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21530 20079 603 41 0 21489 0
vsize: 86120
[startup+120.007 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 20873 0 0 0 11942 56 0 0 25 0 1 0 547603925 88457216 20159 4294967295 134512640 134672761 3221224624 3221223888 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21596 20159 603 41 0 21555 0
vsize: 86384
[startup+130.007 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 20920 0 0 0 12942 57 0 0 25 0 1 0 547603925 88592384 20206 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21629 20206 603 41 0 21588 0
vsize: 86516
[startup+140.007 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21216 0 0 0 13940 58 0 0 25 0 1 0 547603925 89808896 20502 4294967295 134512640 134672761 3221224624 3221223840 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21926 20502 603 41 0 21885 0
vsize: 87704
[startup+150.013 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21335 0 0 0 14940 59 0 0 25 0 1 0 547603925 90210304 20621 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22024 20621 603 41 0 21983 0
vsize: 88096
[startup+160.014 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21457 0 0 0 15940 59 0 0 25 0 1 0 547603925 90746880 20743 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22155 20743 603 41 0 22114 0
vsize: 88620
[startup+170.014 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21601 0 0 0 16939 60 0 0 25 0 1 0 547603925 91541504 20887 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22349 20887 603 41 0 22308 0
vsize: 89396
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21637 0 0 0 17939 61 0 0 25 0 1 0 547603925 91672576 20923 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22381 20923 603 41 0 22340 0
vsize: 89524
[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21669 0 0 0 18938 61 0 0 25 0 1 0 547603925 91807744 20955 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22414 20955 603 41 0 22373 0
vsize: 89656
[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21771 0 0 0 19938 62 0 0 25 0 1 0 547603925 92209152 21057 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22512 21057 603 41 0 22471 0
vsize: 90048
[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21820 0 0 0 20938 62 0 0 25 0 1 0 547603925 92479488 21106 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22578 21106 603 41 0 22537 0
vsize: 90312
[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21870 0 0 0 21938 63 0 0 25 0 1 0 547603925 92610560 21156 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22610 21156 603 41 0 22569 0
vsize: 90440
[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21902 0 0 0 22937 63 0 0 25 0 1 0 547603925 92745728 21188 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22643 21188 603 41 0 22602 0
vsize: 90572
[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21959 0 0 0 23937 63 0 0 25 0 1 0 547603925 92876800 21245 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22675 21245 603 41 0 22634 0
vsize: 90700
[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 21986 0 0 0 24937 63 0 0 25 0 1 0 547603925 93011968 21272 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22708 21272 603 41 0 22667 0
vsize: 90832
[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22012 0 0 0 25937 64 0 0 25 0 1 0 547603925 93147136 21298 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22741 21298 603 41 0 22700 0
vsize: 90964
[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22044 0 0 0 26937 64 0 0 25 0 1 0 547603925 93278208 21330 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22773 21330 603 41 0 22732 0
vsize: 91092
[startup+280.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22092 0 0 0 27936 65 0 0 25 0 1 0 547603925 93413376 21378 4294967295 134512640 134672761 3221224624 3221223824 134557965 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22806 21378 603 41 0 22765 0
vsize: 91224
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22142 0 0 0 28936 65 0 0 25 0 1 0 547603925 93544448 21428 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22838 21428 603 41 0 22797 0
vsize: 91352
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22182 0 0 0 29936 65 0 0 25 0 1 0 547603925 93679616 21468 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22871 21468 603 41 0 22830 0
vsize: 91484
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22223 0 0 0 30936 66 0 0 25 0 1 0 547603925 93814784 21509 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22904 21509 603 41 0 22863 0
vsize: 91616
[startup+320.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22249 0 0 0 31935 66 0 0 25 0 1 0 547603925 93945856 21535 4294967295 134512640 134672761 3221224624 3221223792 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22936 21535 603 41 0 22895 0
vsize: 91744
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22314 0 0 0 32935 67 0 0 25 0 1 0 547603925 94212096 21600 4294967295 134512640 134672761 3221224624 3221223776 134564780 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23001 21600 603 41 0 22960 0
vsize: 92004
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22380 0 0 0 33934 67 0 0 25 0 1 0 547603925 94482432 21666 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23067 21666 603 41 0 23026 0
vsize: 92268
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22418 0 0 0 34934 68 0 0 25 0 1 0 547603925 94617600 21704 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23100 21704 603 41 0 23059 0
vsize: 92400
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22453 0 0 0 35934 68 0 0 25 0 1 0 547603925 94752768 21739 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23133 21739 603 41 0 23092 0
vsize: 92532
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22480 0 0 0 36933 69 0 0 25 0 1 0 547603925 94887936 21766 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23166 21766 603 41 0 23125 0
vsize: 92664
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22503 0 0 0 37933 69 0 0 25 0 1 0 547603925 94887936 21789 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23166 21789 603 41 0 23125 0
vsize: 92664
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22629 0 0 0 38932 70 0 0 25 0 1 0 547603925 95420416 21915 4294967295 134512640 134672761 3221224624 3221223792 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23296 21915 603 41 0 23255 0
vsize: 93184
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22658 0 0 0 39932 70 0 0 25 0 1 0 547603925 95555584 21944 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23329 21944 603 41 0 23288 0
vsize: 93316
[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22730 0 0 0 40931 71 0 0 25 0 1 0 547603925 95825920 22016 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23395 22016 603 41 0 23354 0
vsize: 93580
[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22842 0 0 0 41931 71 0 0 25 0 1 0 547603925 96227328 22128 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23493 22128 603 41 0 23452 0
vsize: 93972
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22895 0 0 0 42931 72 0 0 25 0 1 0 547603925 96497664 22181 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23559 22181 603 41 0 23518 0
vsize: 94236
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22919 0 0 0 43931 72 0 0 25 0 1 0 547603925 96632832 22205 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23592 22205 603 41 0 23551 0
vsize: 94368
[startup+450.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22959 0 0 0 44930 73 0 0 25 0 1 0 547603925 96768000 22245 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23625 22245 603 41 0 23584 0
vsize: 94500
[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 22989 0 0 0 45930 73 0 0 25 0 1 0 547603925 96903168 22275 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23658 22275 603 41 0 23617 0
vsize: 94632
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23055 0 0 0 46929 74 0 0 25 0 1 0 547603925 97173504 22341 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23724 22341 603 41 0 23683 0
vsize: 94896
[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23159 0 0 0 47929 74 0 0 25 0 1 0 547603925 98099200 22445 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23950 22445 603 41 0 23909 0
vsize: 95800
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23212 0 0 0 48928 75 0 0 25 0 1 0 547603925 98234368 22498 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23983 22498 603 41 0 23942 0
vsize: 95932
[startup+500.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23255 0 0 0 49928 76 0 0 25 0 1 0 547603925 98369536 22541 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24016 22541 603 41 0 23975 0
vsize: 96064
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23281 0 0 0 50928 76 0 0 25 0 1 0 547603925 98500608 22567 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24048 22567 603 41 0 24007 0
vsize: 96192
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23307 0 0 0 51927 77 0 0 25 0 1 0 547603925 98635776 22593 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24081 22593 603 41 0 24040 0
vsize: 96324
[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23337 0 0 0 52927 77 0 0 25 0 1 0 547603925 98770944 22623 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24114 22623 603 41 0 24073 0
vsize: 96456
[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23361 0 0 0 53927 78 0 0 25 0 1 0 547603925 98770944 22647 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24114 22647 603 41 0 24073 0
vsize: 96456
[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23388 0 0 0 54927 78 0 0 25 0 1 0 547603925 98906112 22674 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24147 22674 603 41 0 24106 0
vsize: 96588
[startup+560.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23440 0 0 0 55926 78 0 0 25 0 1 0 547603925 99172352 22726 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24212 22726 603 41 0 24171 0
vsize: 96848
[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23504 0 0 0 56926 79 0 0 25 0 1 0 547603925 99442688 22790 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24278 22790 603 41 0 24237 0
vsize: 97112
[startup+580.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23544 0 0 0 57925 79 0 0 25 0 1 0 547603925 99577856 22830 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 22830 603 41 0 24270 0
vsize: 97244
[startup+590.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23585 0 0 0 58925 80 0 0 25 0 1 0 547603925 99713024 22871 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24344 22871 603 41 0 24303 0
vsize: 97376
[startup+600.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23628 0 0 0 59925 80 0 0 25 0 1 0 547603925 99848192 22914 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24377 22914 603 41 0 24336 0
vsize: 97508
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23691 0 0 0 60924 81 0 0 25 0 1 0 547603925 100118528 22977 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24443 22977 603 41 0 24402 0
vsize: 97772
[startup+620.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23761 0 0 0 61924 81 0 0 25 0 1 0 547603925 100384768 23047 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24508 23047 603 41 0 24467 0
vsize: 98032
[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23900 0 0 0 62923 82 0 0 25 0 1 0 547603925 100925440 23186 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24640 23186 603 41 0 24599 0
vsize: 98560
[startup+640.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23928 0 0 0 63922 83 0 0 25 0 1 0 547603925 101056512 23214 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24672 23214 603 41 0 24631 0
vsize: 98688
[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 23984 0 0 0 64922 84 0 0 25 0 1 0 547603925 101326848 23270 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24738 23270 603 41 0 24697 0
vsize: 98952
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24030 0 0 0 65922 84 0 0 25 0 1 0 547603925 101462016 23316 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24771 23316 603 41 0 24730 0
vsize: 99084
[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24062 0 0 0 66922 84 0 0 25 0 1 0 547603925 101593088 23348 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24803 23348 603 41 0 24762 0
vsize: 99212
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24109 0 0 0 67922 85 0 0 25 0 1 0 547603925 101728256 23395 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24836 23395 603 41 0 24795 0
vsize: 99344
[startup+690.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24132 0 0 0 68922 85 0 0 25 0 1 0 547603925 101863424 23418 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24869 23418 603 41 0 24828 0
vsize: 99476
[startup+700.043 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24181 0 0 0 69921 86 0 0 25 0 1 0 547603925 101998592 23467 4294967295 134512640 134672761 3221224624 3221223776 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24902 23467 603 41 0 24861 0
vsize: 99608
[startup+710.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24203 0 0 0 70922 86 0 0 25 0 1 0 547603925 102133760 23489 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24935 23489 603 41 0 24894 0
vsize: 99740
[startup+720.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24288 0 0 0 71921 86 0 0 25 0 1 0 547603925 102408192 23574 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25002 23574 603 41 0 24961 0
vsize: 100008
[startup+730.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24348 0 0 0 72921 87 0 0 25 0 1 0 547603925 102678528 23634 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25068 23634 603 41 0 25027 0
vsize: 100272
[startup+740.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24435 0 0 0 73921 88 0 0 25 0 1 0 547603925 103084032 23721 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25167 23721 603 41 0 25126 0
vsize: 100668
[startup+750.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24488 0 0 0 74920 88 0 0 25 0 1 0 547603925 103219200 23774 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25200 23774 603 41 0 25159 0
vsize: 100800
[startup+760.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24570 0 0 0 75920 89 0 0 25 0 1 0 547603925 103620608 23856 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25298 23856 603 41 0 25257 0
vsize: 101192
[startup+770.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24722 0 0 0 76919 90 0 0 25 0 1 0 547603925 104153088 24008 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25428 24008 603 41 0 25387 0
vsize: 101712
[startup+780.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24862 0 0 0 77917 91 0 0 25 0 1 0 547603925 104693760 24148 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25560 24148 603 41 0 25519 0
vsize: 102240
[startup+790.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 24952 0 0 0 78917 92 0 0 25 0 1 0 547603925 105099264 24238 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25659 24238 603 41 0 25618 0
vsize: 102636
[startup+800.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25189 0 0 0 79917 92 0 0 25 0 1 0 547603925 106045440 24475 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25890 24475 603 41 0 25849 0
vsize: 103560
[startup+810.055 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25422 0 0 0 80915 94 0 0 25 0 1 0 547603925 106987520 24708 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26120 24708 603 41 0 26079 0
vsize: 104480
[startup+820.055 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25521 0 0 0 81915 94 0 0 25 0 1 0 547603925 107388928 24807 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26218 24807 603 41 0 26177 0
vsize: 104872
[startup+830.055 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25616 0 0 0 82915 94 0 0 25 0 1 0 547603925 107794432 24902 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26317 24902 603 41 0 26276 0
vsize: 105268
[startup+840.056 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25742 0 0 0 83914 95 0 0 25 0 1 0 547603925 108199936 25028 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26416 25028 603 41 0 26375 0
vsize: 105664
[startup+850.056 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25818 0 0 0 84914 96 0 0 25 0 1 0 547603925 108474368 25104 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26483 25104 603 41 0 26442 0
vsize: 105932
[startup+860.057 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25869 0 0 0 85914 96 0 0 25 0 1 0 547603925 108744704 25155 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26549 25155 603 41 0 26508 0
vsize: 106196
[startup+870.056 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25904 0 0 0 86914 96 0 0 25 0 1 0 547603925 108879872 25190 4294967295 134512640 134672761 3221224624 3221223840 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26582 25190 603 41 0 26541 0
vsize: 106328
[startup+880.056 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25928 0 0 0 87913 97 0 0 25 0 1 0 547603925 109015040 25214 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26615 25214 603 41 0 26574 0
vsize: 106460
[startup+890.056 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 25988 0 0 0 88913 97 0 0 25 0 1 0 547603925 109150208 25274 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26648 25274 603 41 0 26607 0
vsize: 106592
[startup+900.057 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26031 0 0 0 89913 97 0 0 25 0 1 0 547603925 109416448 25317 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26713 25317 603 41 0 26672 0
vsize: 106852
[startup+910.057 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26083 0 0 0 90913 98 0 0 25 0 1 0 547603925 109551616 25369 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26746 25369 603 41 0 26705 0
vsize: 106984
[startup+920.057 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26115 0 0 0 91912 98 0 0 25 0 1 0 547603925 109686784 25401 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26779 25401 603 41 0 26738 0
vsize: 107116
[startup+930.057 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26153 0 0 0 92912 99 0 0 25 0 1 0 547603925 109817856 25439 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26811 25439 603 41 0 26770 0
vsize: 107244
[startup+940.058 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26191 0 0 0 93911 99 0 0 25 0 1 0 547603925 109953024 25477 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26844 25477 603 41 0 26803 0
vsize: 107376
[startup+950.067 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26241 0 0 0 94912 100 0 0 25 0 1 0 547603925 110223360 25527 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26910 25527 603 41 0 26869 0
vsize: 107640
[startup+960.076 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26336 0 0 0 95913 100 0 0 25 0 1 0 547603925 110493696 25622 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26976 25622 603 41 0 26935 0
vsize: 107904
[startup+970.077 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26394 0 0 0 96913 100 0 0 25 0 1 0 547603925 110759936 25680 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27041 25680 603 41 0 27000 0
vsize: 108164
[startup+980.077 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26425 0 0 0 97913 100 0 0 25 0 1 0 547603925 110895104 25711 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27074 25711 603 41 0 27033 0
vsize: 108296
[startup+990.077 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26485 0 0 0 98913 100 0 0 25 0 1 0 547603925 111165440 25771 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27140 25771 603 41 0 27099 0
vsize: 108560
[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26598 0 0 0 99913 101 0 0 25 0 1 0 547603925 112619520 25884 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27495 25884 603 41 0 27454 0
vsize: 109980
[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26623 0 0 0 100912 101 0 0 25 0 1 0 547603925 112750592 25909 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27527 25909 603 41 0 27486 0
vsize: 110108
[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26654 0 0 0 101912 101 0 0 25 0 1 0 547603925 112881664 25940 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27559 25940 603 41 0 27518 0
vsize: 110236
[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26680 0 0 0 102913 102 0 0 25 0 1 0 547603925 113012736 25966 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27591 25966 603 41 0 27550 0
vsize: 110364
[startup+1040.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26713 0 0 0 103913 102 0 0 25 0 1 0 547603925 113147904 25999 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27624 25999 603 41 0 27583 0
vsize: 110496
[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26748 0 0 0 104913 103 0 0 25 0 1 0 547603925 113283072 26034 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27657 26034 603 41 0 27616 0
vsize: 110628
[startup+1060.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26805 0 0 0 105912 103 0 0 25 0 1 0 547603925 113418240 26091 4294967295 134512640 134672761 3221224624 3221223808 134559257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27690 26091 603 41 0 27649 0
vsize: 110760
[startup+1070.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 26976 0 0 0 106912 104 0 0 25 0 1 0 547603925 114094080 26262 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27855 26262 603 41 0 27814 0
vsize: 111420
[startup+1080.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27039 0 0 0 107911 104 0 0 25 0 1 0 547603925 114364416 26325 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27921 26325 603 41 0 27880 0
vsize: 111684
[startup+1090.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27086 0 0 0 108912 104 0 0 25 0 1 0 547603925 114499584 26372 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27954 26372 603 41 0 27913 0
vsize: 111816
[startup+1100.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27136 0 0 0 109911 104 0 0 25 0 1 0 547603925 114769920 26422 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28020 26422 603 41 0 27979 0
vsize: 112080
[startup+1110.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27194 0 0 0 110912 105 0 0 25 0 1 0 547603925 115036160 26480 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28085 26480 603 41 0 28044 0
vsize: 112340
[startup+1120.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27470 0 0 0 111911 106 0 0 25 0 1 0 547603925 116109312 26756 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28347 26756 603 41 0 28306 0
vsize: 113388
[startup+1130.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27593 0 0 0 112910 106 0 0 25 0 1 0 547603925 116645888 26879 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28478 26879 603 41 0 28437 0
vsize: 113912
[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27669 0 0 0 113910 107 0 0 25 0 1 0 547603925 116912128 26955 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28543 26955 603 41 0 28502 0
vsize: 114172
[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27704 0 0 0 114910 107 0 0 25 0 1 0 547603925 117047296 26990 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28576 26990 603 41 0 28535 0
vsize: 114304
[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27793 0 0 0 115910 107 0 0 25 0 1 0 547603925 117313536 27079 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28641 27079 603 41 0 28600 0
vsize: 114564
[startup+1170.12 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27836 0 0 0 116912 107 0 0 25 0 1 0 547603925 117583872 27122 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28707 27122 603 41 0 28666 0
vsize: 114828
[startup+1180.12 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27885 0 0 0 117912 107 0 0 25 0 1 0 547603925 117714944 27171 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28739 27171 603 41 0 28698 0
vsize: 114956
[startup+1190.12 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 27919 0 0 0 118912 107 0 0 25 0 1 0 547603925 117850112 27205 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28772 27205 603 41 0 28731 0
vsize: 115088
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 10745
Raw data (stat): 10745 (minisat+) R 10744 3260 3259 0 -1 0 28108 0 0 0 119911 108 0 0 25 0 1 0 547603925 118652928 27394 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 27394 603 41 0 28927 0
vsize: 115872
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 10745
Raw data (stat): 10745 (minisat+) Z 10744 3260 3259 0 -1 12 28110 0 0 0 119912 113 0 0 25 0 1 0 547603925 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.18
CPU time (s): 1200.26
CPU user time (s): 1199.12
CPU system time (s): 1.13583
CPU usage (%): 100.007
Max. virtual memory (Kb): 115872
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####