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 19669

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 19:28:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16312 boxname=wulflinc20 idbench=1255 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6d2898572483dddc248ecc48cac97a0c  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-sctap1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-sctap1.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-sctap1.opb
IDLAUNCH: 16312
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        652856 kB
Buffers:         26328 kB
Cached:         332196 kB
SwapCached:        516 kB
Active:          30944 kB
Inactive:       329584 kB
HighTotal:      131008 kB
HighFree:        71708 kB
LowTotal:       903652 kB
LowFree:        581148 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            15804 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:48:14 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 16312 7 1200.29 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]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 404]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 403]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 402]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 401]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 400]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 399]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 398]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 397]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 396]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 395]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 394]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 393]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 392]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 391]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 390]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 389]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 388]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 387]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[ 386]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[ 385]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[ 384]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[ 383]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[ 382]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[ 381]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[ 380]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[ 379]---> Adder-cost: 208   maxlim: 1052399   bits: 22/21
c ---[ 378]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 377]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 376]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 375]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 374]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 373]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 372]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 371]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 370]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 369]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 368]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 367]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 366]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 365]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 364]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 363]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 362]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 361]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 360]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 359]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 358]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 357]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 356]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 355]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 354]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 353]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 352]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 351]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 350]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 349]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 348]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 347]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 346]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 345]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 344]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 343]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 342]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 341]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 340]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 339]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 338]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 337]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 336]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 335]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 334]---> Adder-cost: 218   maxlim: 1050359   bits: 22/21
c ---[ 333]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 332]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 331]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 330]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 329]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 328]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 327]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 326]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 325]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 324]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 323]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 322]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 321]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 320]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 319]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 318]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 317]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 316]---> Adder-cost: 158   maxlim: 1049849   bits: 22/21
c ---[ 315]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 314]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 313]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 312]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 311]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 310]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 309]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 308]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 307]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 306]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 305]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 304]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 303]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 302]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 301]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 300]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 299]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 298]---> Adder-cost: 208   maxlim: 1050359   bits: 22/21
c ---[ 296]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 294]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 292]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 290]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 288]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 286]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 284]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 282]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 280]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 278]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 276]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 274]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 272]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 270]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 268]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 266]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 264]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 262]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 260]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 258]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 256]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 254]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 252]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 250]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 248]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 246]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 244]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 242]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 240]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 238]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 236]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 234]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 232]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 230]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 228]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 226]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 224]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 222]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 220]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 218]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 216]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 214]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 212]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 210]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 208]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 206]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 204]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 202]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 200]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 198]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 196]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 194]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 192]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 190]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 188]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 186]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 184]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 182]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 180]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 178]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 176]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 174]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 172]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 170]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 168]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 166]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 164]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 162]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 160]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 158]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 156]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 154]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 152]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 150]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 148]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 146]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 144]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 142]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 140]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 138]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 136]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 134]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 132]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 130]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 128]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 126]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 124]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 122]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 120]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 118]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 116]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 114]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 112]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 110]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 108]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 106]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 104]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 102]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 100]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  98]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  96]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  94]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  92]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  90]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  88]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  86]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  84]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  82]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  80]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  78]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  76]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  74]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  72]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  70]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  68]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  66]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  64]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  62]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  60]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  58]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  57]---> Adder-cost: 492   maxlim: 2106584   bits: 23/22
c ---[  55]---> Adder-cost: 492   maxlim: 2107864   bits: 23/22
c ---[  54]---> Adder-cost: 492   maxlim: 2109144   bits: 23/22
c ---[  53]---> Adder-cost: 492   maxlim: 2107864   bits: 23/22
c ---[  52]---> Adder-cost: 492   maxlim: 2106968   bits: 23/22
c ---[  51]---> Adder-cost: 492   maxlim: 2106584   bits: 23/22
c ---[  50]---> Adder-cost: 492   maxlim: 2106584   bits: 23/22
c ---[  49]---> Adder-cost: 492   maxlim: 2106584   bits: 23/22
c ---[  48]---> Adder-cost: 492   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]---> Adder-cost: 242   maxlim: 1058264   bits: 22/21
c ---[  36]---> Adder-cost: 242   maxlim: 1059544   bits: 22/21
c ---[  35]---> Adder-cost: 242   maxlim: 1061464   bits: 22/21
c ---[  34]---> Adder-cost: 242   maxlim: 1060824   bits: 22/21
c ---[  33]---> Adder-cost: 242   maxlim: 1060184   bits: 22/21
c ---[  32]---> Adder-cost: 242   maxlim: 1059544   bits: 22/21
c ---[  31]---> Adder-cost: 242   maxlim: 1058264   bits: 22/21
c ---[  30]---> Adder-cost: 242   maxlim: 1058264   bits: 22/21
c ---[  29]---> Adder-cost: 242   maxlim: 1058264   bits: 22/21
c ---[  28]---> Adder-cost: 644   maxlim: 2133104   bits: 23/22
c ---[  27]---> Adder-cost: 644   maxlim: 2133744   bits: 23/22
c ---[  26]---> Adder-cost: 644   maxlim: 2134384   bits: 23/22
c ---[  25]---> Adder-cost: 644   maxlim: 2135664   bits: 23/22
c ---[  24]---> Adder-cost: 644   maxlim: 2135024   bits: 23/22
c ---[  23]---> Adder-cost: 644   maxlim: 2134384   bits: 23/22
c ---[  22]---> Adder-cost: 644   maxlim: 2134384   bits: 23/22
c ---[  21]---> Adder-cost: 644   maxlim: 2133744   bits: 23/22
c ---[  20]---> Adder-cost: 644   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: 286   maxlim: 1056734   bits: 22/21
c ---[   9]---> Adder-cost: 286   maxlim: 1056734   bits: 22/21
c ---[   8]---> Adder-cost: 286   maxlim: 1056734   bits: 22/21
c ---[   7]---> Adder-cost: 286   maxlim: 1056734   bits: 22/21
c ---[   6]---> Adder-cost: 286   maxlim: 1057374   bits: 22/21
c ---[   5]---> Adder-cost: 286   maxlim: 1058654   bits: 22/21
c ---[   4]---> Adder-cost: 286   maxlim: 1059294   bits: 22/21
c ---[   3]---> Adder-cost: 286   maxlim: 1058014   bits: 22/21
c ---[   2]---> Adder-cost: 286   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 |  349113  1249608 |  116371       0        0     nan |  0.000 % |
c |       100 |  349113  1249608 |  128008     100      310     3.1 | 12.546 % |
c |       250 |  349113  1249608 |  140808     250      906     3.6 | 12.546 % |
c |       475 |  349113  1249608 |  154889     475     1905     4.0 | 12.546 % |
c |       814 |  349113  1249608 |  170378     814     3917     4.8 | 12.546 % |
c |      1320 |  349113  1249608 |  187416    1320     6629     5.0 | 12.546 % |
c |      2080 |  349113  1249608 |  206158    2080    10607     5.1 | 12.546 % |
c |      3220 |  349113  1249608 |  226774    3220    16468     5.1 | 12.546 % |
c |      4928 |  349113  1249608 |  249451    4928    27308     5.5 | 12.546 % |
c |      7490 |  349113  1249608 |  274396    7490    42238     5.6 | 12.546 % |
c |     11335 |  349113  1249608 |  301836   11335   118782    10.5 | 12.546 % |
c |     17102 |  349113  1249608 |  332020   17102   191070    11.2 | 12.546 % |
c |     25753 |  349113  1249608 |  365222   25753   299821    11.6 | 12.546 % |
c |     38727 |  349113  1249608 |  401744   38727   423855    10.9 | 12.546 % |
c |     58189 |  349113  1249608 |  441918   58189   865716    14.9 | 12.546 % |
c |     87382 |  349113  1249608 |  486110   87382  1698048    19.4 | 12.546 % |
c |    131171 |  349104  1249577 |  534721  131169  4196144    32.0 | 12.548 % |
c |    196856 |  349104  1249577 |  588193  196854  6257764    31.8 | 12.548 % |
c |    295382 |  349104  1249577 |  647013  295380  9814311    33.2 | 12.548 % |
c |    443172 |  349104  1249577 |  711714  443170 18523733    41.8 | 12.548 % |
#### 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.91 0.95 0.92 2/54 11352
Raw data (stat): 11352 (runsolver) R 11351 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547599207 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 8105 0 0 0 976 21 0 0 25 0 1 0 547599207 38449152 7721 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9387 7721 603 41 0 9346 0
vsize: 37548
[startup+20.0021 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 8363 0 0 0 1974 23 0 0 25 0 1 0 547599207 39493632 7979 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9642 7979 603 41 0 9601 0
vsize: 38568
[startup+30.0024 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 8557 0 0 0 2973 23 0 0 25 0 1 0 547599207 40427520 8173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9870 8173 603 41 0 9829 0
vsize: 39480
[startup+40.0028 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 8979 0 0 0 3971 25 0 0 25 0 1 0 547599207 42172416 8595 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10296 8595 603 41 0 10255 0
vsize: 41184
[startup+50.003 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 9426 0 0 0 4969 27 0 0 25 0 1 0 547599207 43925504 9042 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10724 9042 603 41 0 10683 0
vsize: 42896
[startup+60.0034 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 9718 0 0 0 5968 28 0 0 25 0 1 0 547599207 45264896 9334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11051 9334 603 41 0 11010 0
vsize: 44204
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 10463 0 0 0 6966 30 0 0 25 0 1 0 547599207 48361472 10079 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10079 603 41 0 11766 0
vsize: 47228
[startup+80.0041 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 11096 0 0 0 7964 33 0 0 25 0 1 0 547599207 50778112 10712 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12397 10712 603 41 0 12356 0
vsize: 49588
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 11672 0 0 0 8962 34 0 0 25 0 1 0 547599207 53178368 11288 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12983 11288 603 41 0 12942 0
vsize: 51932
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 12106 0 0 0 9961 36 0 0 25 0 1 0 547599207 54923264 11722 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13409 11722 603 41 0 13368 0
vsize: 53636
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 12483 0 0 0 10959 38 0 0 25 0 1 0 547599207 56516608 12099 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13798 12099 603 41 0 13757 0
vsize: 55192
[startup+120.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 12831 0 0 0 11958 39 0 0 25 0 1 0 547599207 57864192 12447 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14127 12447 603 41 0 14086 0
vsize: 56508
[startup+130.006 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 13116 0 0 0 12958 39 0 0 25 0 1 0 547599207 59088896 12732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14426 12732 603 41 0 14385 0
vsize: 57704
[startup+140.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 13383 0 0 0 13957 40 0 0 25 0 1 0 547599207 60190720 12999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14695 12999 603 41 0 14654 0
vsize: 58780
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 13697 0 0 0 14957 41 0 0 25 0 1 0 547599207 61931520 13313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15120 13313 603 41 0 15079 0
vsize: 60480
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 14456 0 0 0 15955 42 0 0 25 0 1 0 547599207 64897024 14072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15844 14072 603 41 0 15803 0
vsize: 63376
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 15103 0 0 0 16954 44 0 0 25 0 1 0 547599207 67584000 14719 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16500 14719 603 41 0 16459 0
vsize: 66000
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 15571 0 0 0 17951 47 0 0 25 0 1 0 547599207 69419008 15187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16948 15187 603 41 0 16907 0
vsize: 67792
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 16065 0 0 0 18950 48 0 0 25 0 1 0 547599207 71446528 15681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17443 15681 603 41 0 17402 0
vsize: 69772
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 16764 0 0 0 19948 50 0 0 25 0 1 0 547599207 74268672 16380 4294967295 134512640 134672761 3221224544 3221223648 134555098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18132 16380 603 41 0 18091 0
vsize: 72528
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 17351 0 0 0 20947 52 0 0 25 0 1 0 547599207 76562432 16967 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18692 16967 603 41 0 18651 0
vsize: 74768
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 17801 0 0 0 21945 54 0 0 25 0 1 0 547599207 78450688 17417 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19153 17417 603 41 0 19112 0
vsize: 76612
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 18126 0 0 0 22944 55 0 0 25 0 1 0 547599207 79818752 17742 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19487 17742 603 41 0 19446 0
vsize: 77948
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 18392 0 0 0 23943 57 0 0 25 0 1 0 547599207 80887808 18008 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19748 18008 603 41 0 19707 0
vsize: 78992
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 18647 0 0 0 24942 57 0 0 25 0 1 0 547599207 81891328 18263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19993 18263 603 41 0 19952 0
vsize: 79972
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 18905 0 0 0 25941 58 0 0 25 0 1 0 547599207 82976768 18521 4294967295 134512640 134672761 3221224544 3221223744 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20258 18521 603 41 0 20217 0
vsize: 81032
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 19133 0 0 0 26941 59 0 0 25 0 1 0 547599207 83914752 18749 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20487 18749 603 41 0 20446 0
vsize: 81948
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 19337 0 0 0 27941 59 0 0 25 0 1 0 547599207 84733952 18953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20687 18953 603 41 0 20646 0
vsize: 82748
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 19512 0 0 0 28940 60 0 0 25 0 1 0 547599207 85401600 19128 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20850 19128 603 41 0 20809 0
vsize: 83400
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 19721 0 0 0 29940 61 0 0 25 0 1 0 547599207 87449600 19337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21350 19337 603 41 0 21309 0
vsize: 85400
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 19881 0 0 0 30939 62 0 0 25 0 1 0 547599207 87982080 19497 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21480 19497 603 41 0 21439 0
vsize: 85920
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 20036 0 0 0 31939 62 0 0 25 0 1 0 547599207 88657920 19652 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21645 19652 603 41 0 21604 0
vsize: 86580
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 20537 0 0 0 32937 64 0 0 25 0 1 0 547599207 90685440 20153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22140 20153 603 41 0 22099 0
vsize: 88560
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 20894 0 0 0 33936 65 0 0 25 0 1 0 547599207 92045312 20510 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22472 20510 603 41 0 22431 0
vsize: 89888
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 21299 0 0 0 34934 66 0 0 25 0 1 0 547599207 93818880 20915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22905 20915 603 41 0 22864 0
vsize: 91620
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 22068 0 0 0 35932 69 0 0 25 0 1 0 547599207 96899072 21684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23657 21684 603 41 0 23616 0
vsize: 94628
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 22627 0 0 0 36930 71 0 0 25 0 1 0 547599207 99172352 22243 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24212 22243 603 41 0 24171 0
vsize: 96848
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 23111 0 0 0 37928 73 0 0 25 0 1 0 547599207 101195776 22727 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24706 22727 603 41 0 24665 0
vsize: 98824
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 23482 0 0 0 38927 75 0 0 25 0 1 0 547599207 102670336 23098 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25066 23098 603 41 0 25025 0
vsize: 100264
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 23855 0 0 0 39926 76 0 0 25 0 1 0 547599207 104185856 23471 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25436 23471 603 41 0 25395 0
vsize: 101744
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 24143 0 0 0 40925 78 0 0 25 0 1 0 547599207 105381888 23759 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25728 23759 603 41 0 25687 0
vsize: 102912
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 24451 0 0 0 41924 78 0 0 25 0 1 0 547599207 106582016 24067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26021 24067 603 41 0 25980 0
vsize: 104084
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 24754 0 0 0 42924 79 0 0 25 0 1 0 547599207 107782144 24370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26314 24370 603 41 0 26273 0
vsize: 105256
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 25014 0 0 0 43923 80 0 0 25 0 1 0 547599207 108929024 24630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26594 24630 603 41 0 26553 0
vsize: 106376
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 25272 0 0 0 44922 81 0 0 25 0 1 0 547599207 109993984 24888 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26854 24888 603 41 0 26813 0
vsize: 107416
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 25517 0 0 0 45921 82 0 0 25 0 1 0 547599207 110931968 25133 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27083 25133 603 41 0 27042 0
vsize: 108332
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 25783 0 0 0 46921 83 0 0 25 0 1 0 547599207 112050176 25399 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27356 25399 603 41 0 27315 0
vsize: 109424
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 26048 0 0 0 47920 84 0 0 25 0 1 0 547599207 113111040 25664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27615 25664 603 41 0 27574 0
vsize: 110460
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 26290 0 0 0 48919 85 0 0 25 0 1 0 547599207 114036736 25906 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27841 25906 603 41 0 27800 0
vsize: 111364
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 26525 0 0 0 49918 86 0 0 25 0 1 0 547599207 115134464 26141 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28109 26141 603 41 0 28068 0
vsize: 112436
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 26746 0 0 0 50918 86 0 0 25 0 1 0 547599207 115961856 26362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28311 26362 603 41 0 28270 0
vsize: 113244
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 26944 0 0 0 51917 87 0 0 25 0 1 0 547599207 116776960 26560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28510 26560 603 41 0 28469 0
vsize: 114040
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 27153 0 0 0 52917 88 0 0 25 0 1 0 547599207 117575680 26769 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28705 26769 603 41 0 28664 0
vsize: 114820
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 27339 0 0 0 53917 88 0 0 25 0 1 0 547599207 118366208 26955 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28898 26955 603 41 0 28857 0
vsize: 115592
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 27540 0 0 0 54916 89 0 0 25 0 1 0 547599207 119169024 27156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29094 27156 603 41 0 29053 0
vsize: 116376
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 27748 0 0 0 55916 89 0 0 25 0 1 0 547599207 119980032 27364 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29292 27364 603 41 0 29251 0
vsize: 117168
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 27942 0 0 0 56915 90 0 0 25 0 1 0 547599207 120782848 27558 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29488 27558 603 41 0 29447 0
vsize: 117952
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 28131 0 0 0 57914 91 0 0 25 0 1 0 547599207 121597952 27747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29687 27747 603 41 0 29646 0
vsize: 118748
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 28303 0 0 0 58914 92 0 0 25 0 1 0 547599207 122265600 27919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29850 27919 603 41 0 29809 0
vsize: 119400
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 28491 0 0 0 59914 92 0 0 25 0 1 0 547599207 123088896 28107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30051 28107 603 41 0 30010 0
vsize: 120204
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 28654 0 0 0 60913 93 0 0 25 0 1 0 547599207 123817984 28270 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30229 28270 603 41 0 30188 0
vsize: 120916
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 28822 0 0 0 61913 93 0 0 25 0 1 0 547599207 124481536 28438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30391 28438 603 41 0 30350 0
vsize: 121564
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 28982 0 0 0 62913 94 0 0 25 0 1 0 547599207 125157376 28598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30556 28598 603 41 0 30515 0
vsize: 122224
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 29132 0 0 0 63913 94 0 0 25 0 1 0 547599207 125685760 28748 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30685 28748 603 41 0 30644 0
vsize: 122740
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 29271 0 0 0 64913 94 0 0 25 0 1 0 547599207 126386176 28887 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30856 28887 603 41 0 30815 0
vsize: 123424
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 29419 0 0 0 65912 95 0 0 25 0 1 0 547599207 126918656 29035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30986 29035 603 41 0 30945 0
vsize: 123944
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 29544 0 0 0 66912 95 0 0 25 0 1 0 547599207 127455232 29160 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31117 29160 603 41 0 31076 0
vsize: 124468
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 29688 0 0 0 67912 96 0 0 25 0 1 0 547599207 128045056 29304 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31261 29304 603 41 0 31220 0
vsize: 125044
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 29827 0 0 0 68911 97 0 0 25 0 1 0 547599207 128708608 29443 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31423 29443 603 41 0 31382 0
vsize: 125692
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 29966 0 0 0 69911 97 0 0 25 0 1 0 547599207 129241088 29582 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31553 29582 603 41 0 31512 0
vsize: 126212
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 30552 0 0 0 70910 98 0 0 25 0 1 0 547599207 131637248 30168 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32138 30168 603 41 0 32097 0
vsize: 128552
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 30970 0 0 0 71909 99 0 0 25 0 1 0 547599207 133394432 30586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32567 30586 603 41 0 32526 0
vsize: 130268
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 31453 0 0 0 72908 100 0 0 25 0 1 0 547599207 135286784 31069 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33029 31069 603 41 0 32988 0
vsize: 132116
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 31793 0 0 0 73907 101 0 0 25 0 1 0 547599207 136650752 31409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33362 31409 603 41 0 33321 0
vsize: 133448
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 32083 0 0 0 74907 101 0 0 25 0 1 0 547599207 137879552 31699 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33662 31699 603 41 0 33621 0
vsize: 134648
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 32308 0 0 0 75907 102 0 0 25 0 1 0 547599207 138817536 31924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33891 31924 603 41 0 33850 0
vsize: 135564
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 32479 0 0 0 76906 102 0 0 25 0 1 0 547599207 139489280 32095 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34055 32095 603 41 0 34014 0
vsize: 136220
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 32662 0 0 0 77906 103 0 0 25 0 1 0 547599207 140165120 32278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34220 32278 603 41 0 34179 0
vsize: 136880
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 32860 0 0 0 78906 103 0 0 25 0 1 0 547599207 141008896 32476 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34426 32476 603 41 0 34385 0
vsize: 137704
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 33035 0 0 0 79905 104 0 0 25 0 1 0 547599207 141680640 32651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34590 32651 603 41 0 34549 0
vsize: 138360
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 33206 0 0 0 80905 104 0 0 25 0 1 0 547599207 142393344 32822 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34764 32822 603 41 0 34723 0
vsize: 139056
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 33381 0 0 0 81904 106 0 0 25 0 1 0 547599207 143224832 32997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34967 32997 603 41 0 34926 0
vsize: 139868
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 33548 0 0 0 82903 106 0 0 25 0 1 0 547599207 143810560 33164 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35110 33164 603 41 0 35069 0
vsize: 140440
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 33689 0 0 0 83903 107 0 0 25 0 1 0 547599207 144351232 33305 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35242 33305 603 41 0 35201 0
vsize: 140968
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 33838 0 0 0 84903 107 0 0 25 0 1 0 547599207 145027072 33454 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35407 33454 603 41 0 35366 0
vsize: 141628
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 34261 0 0 0 85902 108 0 0 25 0 1 0 547599207 146788352 33877 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35837 33877 603 41 0 35796 0
vsize: 143348
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 34554 0 0 0 86902 109 0 0 25 0 1 0 547599207 147869696 34170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36101 34170 603 41 0 36060 0
vsize: 144404
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 34679 0 0 0 87901 109 0 0 25 0 1 0 547599207 148406272 34295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36232 34295 603 41 0 36191 0
vsize: 144928
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 34813 0 0 0 88901 110 0 0 25 0 1 0 547599207 148938752 34429 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36362 34429 603 41 0 36321 0
vsize: 145448
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 34950 0 0 0 89900 111 0 0 25 0 1 0 547599207 151572480 34566 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37005 34566 603 41 0 36964 0
vsize: 148020
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 35094 0 0 0 90900 111 0 0 25 0 1 0 547599207 152109056 34710 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37136 34710 603 41 0 37095 0
vsize: 148544
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 35237 0 0 0 91900 111 0 0 25 0 1 0 547599207 152784896 34853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37301 34853 603 41 0 37260 0
vsize: 149204
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 35376 0 0 0 92900 112 0 0 25 0 1 0 547599207 153321472 34992 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37432 34992 603 41 0 37391 0
vsize: 149728
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 35533 0 0 0 93900 112 0 0 25 0 1 0 547599207 154013696 35149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37601 35149 603 41 0 37560 0
vsize: 150404
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 35683 0 0 0 94899 113 0 0 25 0 1 0 547599207 154550272 35299 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37732 35299 603 41 0 37691 0
vsize: 150928
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 35843 0 0 0 95899 113 0 0 25 0 1 0 547599207 155217920 35459 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37895 35459 603 41 0 37854 0
vsize: 151580
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 36015 0 0 0 96899 114 0 0 25 0 1 0 547599207 155885568 35631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38058 35631 603 41 0 38017 0
vsize: 152232
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 36151 0 0 0 97899 114 0 0 25 0 1 0 547599207 156422144 35767 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38189 35767 603 41 0 38148 0
vsize: 152756
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 36325 0 0 0 98898 115 0 0 25 0 1 0 547599207 157093888 35941 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38353 35941 603 41 0 38312 0
vsize: 153412
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 36623 0 0 0 99897 116 0 0 25 0 1 0 547599207 158429184 36239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38679 36239 603 41 0 38638 0
vsize: 154716
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 36805 0 0 0 100897 116 0 0 25 0 1 0 547599207 159227904 36421 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38874 36421 603 41 0 38833 0
vsize: 155496
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 36971 0 0 0 101897 117 0 0 25 0 1 0 547599207 159911936 36587 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39041 36587 603 41 0 39000 0
vsize: 156164
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 37153 0 0 0 102896 117 0 0 25 0 1 0 547599207 160604160 36769 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39210 36769 603 41 0 39169 0
vsize: 156840
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 37514 0 0 0 103895 119 0 0 25 0 1 0 547599207 162086912 37130 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39572 37130 603 41 0 39531 0
vsize: 158288
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 37952 0 0 0 104893 121 0 0 25 0 1 0 547599207 163852288 37568 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40003 37568 603 41 0 39962 0
vsize: 160012
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 38184 0 0 0 105893 122 0 0 25 0 1 0 547599207 164790272 37800 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40232 37800 603 41 0 40191 0
vsize: 160928
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 38395 0 0 0 106893 122 0 0 25 0 1 0 547599207 165605376 38011 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40431 38011 603 41 0 40390 0
vsize: 161724
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 38501 0 0 0 107894 123 0 0 25 0 1 0 547599207 166010880 38117 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40530 38117 603 41 0 40489 0
vsize: 162120
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 38697 0 0 0 108893 123 0 0 25 0 1 0 547599207 166813696 38313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40726 38313 603 41 0 40685 0
vsize: 162904
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 39205 0 0 0 109892 124 0 0 25 0 1 0 547599207 168837120 38821 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41220 38821 603 41 0 41179 0
vsize: 164880
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 39368 0 0 0 110892 125 0 0 25 0 1 0 547599207 169508864 38984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41384 38984 603 41 0 41343 0
vsize: 165536
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 39541 0 0 0 111892 125 0 0 25 0 1 0 547599207 170184704 39157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41549 39157 603 41 0 41508 0
vsize: 166196
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 39814 0 0 0 112892 126 0 0 25 0 1 0 547599207 171266048 39430 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41813 39431 603 41 0 41772 0
vsize: 167252
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 40040 0 0 0 113891 127 0 0 25 0 1 0 547599207 172216320 39656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42045 39656 603 41 0 42004 0
vsize: 168180
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 40165 0 0 0 114891 127 0 0 25 0 1 0 547599207 172752896 39781 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42176 39781 603 41 0 42135 0
vsize: 168704
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 40312 0 0 0 115890 128 0 0 25 0 1 0 547599207 173428736 39928 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42341 39928 603 41 0 42300 0
vsize: 169364
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 40463 0 0 0 116889 129 0 0 25 0 1 0 547599207 173965312 40079 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42472 40079 603 41 0 42431 0
vsize: 169888
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 40641 0 0 0 117889 129 0 0 25 0 1 0 547599207 174637056 40257 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42636 40257 603 41 0 42595 0
vsize: 170544
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 40800 0 0 0 118889 130 0 0 25 0 1 0 547599207 175316992 40416 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42802 40416 603 41 0 42761 0
vsize: 171208
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11352
Raw data (stat): 11352 (minisat+) R 11351 27565 27564 0 -1 0 40956 0 0 0 119890 131 0 0 25 0 1 0 547599207 175992832 40572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42967 40572 603 41 0 42926 0
vsize: 171868
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 11352
Raw data (stat): 11352 (minisat+) Z 11351 27565 27564 0 -1 12 40958 0 0 0 119890 138 0 0 21 0 1 0 547599207 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.23
CPU time (s): 1200.29
CPU user time (s): 1198.9
CPU system time (s): 1.38679
CPU usage (%): 100.005
Max. virtual memory (Kb): 171868
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####