PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-5.opb
MD5SUM	6049145b9f1adfd7114adf044503d587
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2642
Optimality of the best value was proved	NO
Number of terms in the objective function	748
Biggest coefficient in the objective function	240
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	33855
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	240
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	33855
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02984
Number of variables	907
Total number of constraints	1309
Number of constraints which are clauses	126
Number of constraints which are cardinality constraints (but not clauses)	1183
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	134
Trace number 5278

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-13 23:14:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3742 boxname=wulflinc11 idbench=358 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6049145b9f1adfd7114adf044503d587  /oldhome/oroussel/tmp/wulflinc11/normalized-ws97-5.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc11/normalized-ws97-5.opb /oldhome/oroussel/tmp/wulflinc11/normalized-ws97-5.opb
IDLAUNCH: 3742
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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	: 2
cpu MHz		: 451.028
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:        915964 kB
Buffers:         34688 kB
Cached:          59728 kB
SwapCached:       4932 kB
Active:          55200 kB
Inactive:        47020 kB
HighTotal:      131008 kB
HighFree:        67508 kB
LowTotal:       903652 kB
LowFree:        848456 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10884 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:34:41 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 3742 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 661 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: ##################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .............................................................................................................................
c ---[ 660]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 659]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 658]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 657]---> Adder-cost: 238   maxlim: 91   bits: 7/7
c ---[ 656]---> Adder-cost: 260   maxlim: 85   bits: 8/7
c ---[ 655]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 654]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 653]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 652]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 651]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 650]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 649]---> Adder-cost: 28   maxlim: 33   bits: 7/6
c ---[ 648]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 647]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 645]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 643]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 641]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 639]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 637]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 635]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 633]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 631]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 629]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 627]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 625]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 623]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 621]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 619]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 617]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 615]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 613]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 611]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 609]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 607]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 605]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 603]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 601]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 599]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 597]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 595]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 593]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 591]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 589]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 587]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 585]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 583]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 581]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 579]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 577]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 575]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 573]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 571]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 569]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 567]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 565]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 563]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 561]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 559]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 557]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 555]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 553]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 551]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 549]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 547]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 545]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 543]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 541]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 539]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 537]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 535]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 533]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 531]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 529]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 527]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 525]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 523]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 521]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 519]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 517]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 515]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 513]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 511]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 509]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 507]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 505]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 503]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 501]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 499]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 497]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 495]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 493]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 491]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 489]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 487]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 485]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 483]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 481]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 479]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 477]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 475]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 473]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 471]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 469]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 467]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 465]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 463]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 461]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 459]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 457]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 455]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 453]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 451]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 449]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 447]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 445]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 443]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 441]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 439]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 437]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 435]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 433]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 431]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 429]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 427]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 425]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 423]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 421]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 419]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 417]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 415]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 413]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 411]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 409]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 407]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 405]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 403]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 401]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 399]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 397]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 395]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 393]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 391]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 389]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 387]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 385]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 383]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 381]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 379]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 377]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 375]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 373]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 371]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 369]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 367]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 365]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 363]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 361]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 359]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 357]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 355]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 353]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 351]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 349]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 347]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 345]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 343]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 341]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 339]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 337]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 335]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 333]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 327]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 325]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 323]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 321]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 319]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 317]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 315]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 313]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 311]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 309]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 307]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 305]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 303]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 301]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 299]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 297]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 295]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 293]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 291]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 289]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 287]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 285]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 283]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 281]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 279]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 277]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 275]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 273]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 271]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 269]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 267]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 265]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 263]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 261]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 259]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 257]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 255]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 253]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 251]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 249]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 247]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 245]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 243]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 241]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 239]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 237]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 235]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 233]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 231]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 229]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 227]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 225]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 223]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 221]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 219]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 217]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 215]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 213]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 211]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 209]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 207]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 205]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 203]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 201]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 199]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 197]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 195]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 193]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 191]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 189]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 187]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 185]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 183]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 181]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 179]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 177]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 175]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 173]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 171]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 169]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 167]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 165]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 163]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 161]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 159]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 157]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 155]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 153]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 151]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 149]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 147]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 145]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 143]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 141]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 139]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 137]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 135]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 133]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 131]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 129]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 127]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   16616    58214 |    5538       0        0     nan |  0.000 % |
c |       101 |   16592    58148 |    6091      98      453     4.6 | 25.667 % |
c |       251 |   16586    58131 |    6700     247     1107     4.5 | 25.691 % |
c |       476 |   16538    57999 |    7371     466     1886     4.0 | 25.974 % |
c |       814 |   16530    57977 |    8108     803     4455     5.5 | 26.021 % |
c |      1320 |   16522    57955 |    8919    1308     7501     5.7 | 26.068 % |
c |      2079 |   16522    57955 |    9810    2067    11705     5.7 | 26.068 % |
c |      3219 |   16522    57955 |   10791    3207    24352     7.6 | 26.068 % |
c |      4929 |   16490    57867 |   11871    4913    59795    12.2 | 26.257 % |
c |      7491 |   16490    57867 |   13058    7475   181148    24.2 | 26.257 % |
c |     11335 |   16490    57867 |   14364   11319   359883    31.8 | 26.257 % |
c |     17102 |   16490    57867 |   15800    9037   534600    59.2 | 26.257 % |
c |     25751 |   16458    57779 |   17380    8893   411846    46.3 | 26.446 % |
c |     38725 |   16442    57735 |   19118   12245   851407    69.5 | 26.541 % |
c |     58188 |   16434    57713 |   21030   21100  1540949    73.0 | 26.588 % |
c |     87388 |   16426    57691 |   23133   16333  1315989    80.6 | 26.635 % |
c |    131177 |   16426    57691 |   25446   22183  2310365   104.2 | 26.635 % |
c |    196864 |   16406    57635 |   27991   18734  2260223   120.6 | 26.777 % |
c |    295392 |   16299    57343 |   30790   18252  1841279   100.9 | 27.462 % |
c |    443182 |   16283    57299 |   33869   25818  2087508    80.9 | 27.556 % |
c |    664867 |   16259    57233 |   37256   23108  2591782   112.2 | 27.698 % |
#### 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.93 0.97 0.91 2/54 5441
Raw data (stat): 5441 (runsolver) R 5440 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421605990 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99996 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 1858 0 0 0 992 6 0 0 25 0 1 0 421605990 9449472 1835 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2307 1835 603 41 0 2266 0
vsize: 9228
[startup+20.0004 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 2456 0 0 0 1989 9 0 0 25 0 1 0 421605990 11878400 2433 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2900 2433 603 41 0 2859 0
vsize: 11600
[startup+30.001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 2705 0 0 0 2987 10 0 0 25 0 1 0 421605990 12828672 2682 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3132 2682 603 41 0 3091 0
vsize: 12528
[startup+40.002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 2999 0 0 0 3986 11 0 0 25 0 1 0 421605990 14049280 2976 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3430 2976 603 41 0 3389 0
vsize: 13720
[startup+50.0028 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 3081 0 0 0 4986 11 0 0 25 0 1 0 421605990 14462976 3058 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3531 3058 603 41 0 3490 0
vsize: 14124
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 3510 0 0 0 5984 13 0 0 25 0 1 0 421605990 16211968 3487 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3958 3487 603 41 0 3917 0
vsize: 15832
[startup+70.0037 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 3543 0 0 0 6983 14 0 0 25 0 1 0 421605990 16343040 3520 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3990 3520 603 41 0 3949 0
vsize: 15960
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 3554 0 0 0 7982 14 0 0 25 0 1 0 421605990 16343040 3531 4294967295 134512640 134672761 3221224576 3221223760 134559601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3990 3531 603 41 0 3949 0
vsize: 15960
[startup+90.0046 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 3824 0 0 0 8981 14 0 0 25 0 1 0 421605990 17424384 3801 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4254 3801 603 41 0 4213 0
vsize: 17016
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4169 0 0 0 9980 16 0 0 25 0 1 0 421605990 18903040 4146 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4615 4146 603 41 0 4574 0
vsize: 18460
[startup+110.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4169 0 0 0 10980 16 0 0 25 0 1 0 421605990 18903040 4146 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4615 4146 603 41 0 4574 0
vsize: 18460
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4171 0 0 0 11980 16 0 0 25 0 1 0 421605990 18903040 4148 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4615 4148 603 41 0 4574 0
vsize: 18460
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4171 0 0 0 12981 16 0 0 25 0 1 0 421605990 18903040 4148 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4615 4148 603 41 0 4574 0
vsize: 18460
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4171 0 0 0 13981 16 0 0 25 0 1 0 421605990 18903040 4148 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4615 4148 603 41 0 4574 0
vsize: 18460
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4507 0 0 0 14980 17 0 0 25 0 1 0 421605990 20246528 4484 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4943 4484 603 41 0 4902 0
vsize: 19772
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4522 0 0 0 15980 17 0 0 25 0 1 0 421605990 20389888 4499 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4499 603 41 0 4937 0
vsize: 19912
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4804 0 0 0 16980 18 0 0 25 0 1 0 421605990 21618688 4781 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5278 4781 603 41 0 5237 0
vsize: 21112
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4887 0 0 0 17980 18 0 0 25 0 1 0 421605990 21889024 4864 4294967295 134512640 134672761 3221224576 3221223760 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5344 4864 603 41 0 5303 0
vsize: 21376
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 4887 0 0 0 18980 18 0 0 25 0 1 0 421605990 21889024 4864 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5344 4864 603 41 0 5303 0
vsize: 21376
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5092 0 0 0 19980 18 0 0 25 0 1 0 421605990 22683648 5069 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5538 5069 603 41 0 5497 0
vsize: 22152
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5095 0 0 0 20980 18 0 0 25 0 1 0 421605990 22683648 5072 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5538 5072 603 41 0 5497 0
vsize: 22152
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5095 0 0 0 21980 18 0 0 25 0 1 0 421605990 22683648 5072 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5538 5072 603 41 0 5497 0
vsize: 22152
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5095 0 0 0 22980 18 0 0 25 0 1 0 421605990 22683648 5072 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5538 5072 603 41 0 5497 0
vsize: 22152
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5095 0 0 0 23980 18 0 0 25 0 1 0 421605990 22683648 5072 4294967295 134512640 134672761 3221224576 3221222624 134565745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5538 5072 603 41 0 5497 0
vsize: 22152
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5095 0 0 0 24981 18 0 0 25 0 1 0 421605990 22683648 5072 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5538 5072 603 41 0 5497 0
vsize: 22152
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5095 0 0 0 25981 18 0 0 25 0 1 0 421605990 22683648 5072 4294967295 134512640 134672761 3221224576 3221223760 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5538 5072 603 41 0 5497 0
vsize: 22152
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5095 0 0 0 26981 18 0 0 25 0 1 0 421605990 22683648 5072 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5538 5072 603 41 0 5497 0
vsize: 22152
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5095 0 0 0 27981 18 0 0 25 0 1 0 421605990 22683648 5072 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5538 5072 603 41 0 5497 0
vsize: 22152
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5408 0 0 0 28980 19 0 0 25 0 1 0 421605990 24047616 5385 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5871 5385 603 41 0 5830 0
vsize: 23484
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5417 0 0 0 29980 19 0 0 25 0 1 0 421605990 24047616 5394 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5871 5394 603 41 0 5830 0
vsize: 23484
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5417 0 0 0 30980 19 0 0 25 0 1 0 421605990 24047616 5394 4294967295 134512640 134672761 3221224576 3221223680 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5871 5394 603 41 0 5830 0
vsize: 23484
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5417 0 0 0 31980 19 0 0 25 0 1 0 421605990 24047616 5394 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5871 5394 603 41 0 5830 0
vsize: 23484
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5452 0 0 0 32979 19 0 0 25 0 1 0 421605990 24309760 5429 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5935 5429 603 41 0 5894 0
vsize: 23740
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5452 0 0 0 33980 19 0 0 25 0 1 0 421605990 24309760 5429 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5935 5429 603 41 0 5894 0
vsize: 23740
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5452 0 0 0 34980 19 0 0 25 0 1 0 421605990 24309760 5429 4294967295 134512640 134672761 3221224576 3221223744 134564451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5935 5429 603 41 0 5894 0
vsize: 23740
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5464 0 0 0 35980 19 0 0 25 0 1 0 421605990 24469504 5441 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5974 5441 603 41 0 5933 0
vsize: 23896
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5464 0 0 0 36980 19 0 0 25 0 1 0 421605990 24469504 5441 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5974 5441 603 41 0 5933 0
vsize: 23896
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5474 0 0 0 37980 19 0 0 25 0 1 0 421605990 24469504 5451 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5974 5451 603 41 0 5933 0
vsize: 23896
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5477 0 0 0 38980 19 0 0 25 0 1 0 421605990 24469504 5454 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5974 5454 603 41 0 5933 0
vsize: 23896
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5487 0 0 0 39980 20 0 0 25 0 1 0 421605990 24469504 5464 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5974 5464 603 41 0 5933 0
vsize: 23896
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5487 0 0 0 40981 20 0 0 25 0 1 0 421605990 24469504 5464 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5974 5464 603 41 0 5933 0
vsize: 23896
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5487 0 0 0 41981 20 0 0 25 0 1 0 421605990 24469504 5464 4294967295 134512640 134672761 3221224576 3221223680 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5974 5464 603 41 0 5933 0
vsize: 23896
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5487 0 0 0 42981 20 0 0 25 0 1 0 421605990 24469504 5464 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5974 5464 603 41 0 5933 0
vsize: 23896
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5500 0 0 0 43981 20 0 0 25 0 1 0 421605990 24666112 5477 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6022 5477 603 41 0 5981 0
vsize: 24088
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5584 0 0 0 44981 20 0 0 25 0 1 0 421605990 24936448 5561 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6088 5561 603 41 0 6047 0
vsize: 24352
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5588 0 0 0 45981 20 0 0 25 0 1 0 421605990 24936448 5565 4294967295 134512640 134672761 3221224576 3221223496 1075351157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6088 5565 603 41 0 6047 0
vsize: 24352
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5591 0 0 0 46981 20 0 0 25 0 1 0 421605990 24936448 5568 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6088 5568 603 41 0 6047 0
vsize: 24352
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5591 0 0 0 47981 20 0 0 25 0 1 0 421605990 24936448 5568 4294967295 134512640 134672761 3221224576 3221223680 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6088 5568 603 41 0 6047 0
vsize: 24352
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5629 0 0 0 48981 20 0 0 25 0 1 0 421605990 25092096 5606 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6126 5606 603 41 0 6085 0
vsize: 24504
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5637 0 0 0 49982 20 0 0 25 0 1 0 421605990 25255936 5614 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6166 5614 603 41 0 6125 0
vsize: 24664
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5646 0 0 0 50982 20 0 0 25 0 1 0 421605990 25255936 5623 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6166 5623 603 41 0 6125 0
vsize: 24664
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5646 0 0 0 51982 20 0 0 25 0 1 0 421605990 25255936 5623 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6166 5623 603 41 0 6125 0
vsize: 24664
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5646 0 0 0 52982 20 0 0 25 0 1 0 421605990 25255936 5623 4294967295 134512640 134672761 3221224576 3221223680 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6166 5623 603 41 0 6125 0
vsize: 24664
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5649 0 0 0 53982 20 0 0 25 0 1 0 421605990 25255936 5626 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6166 5626 603 41 0 6125 0
vsize: 24664
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5649 0 0 0 54982 20 0 0 25 0 1 0 421605990 25255936 5626 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6166 5626 603 41 0 6125 0
vsize: 24664
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5649 0 0 0 55982 20 0 0 25 0 1 0 421605990 25255936 5626 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6166 5626 603 41 0 6125 0
vsize: 24664
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5812 0 0 0 56982 21 0 0 25 0 1 0 421605990 25956352 5789 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6337 5789 603 41 0 6296 0
vsize: 25348
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5986 0 0 0 57981 22 0 0 25 0 1 0 421605990 26624000 5963 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6500 5963 603 41 0 6459 0
vsize: 26000
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 5994 0 0 0 58981 22 0 0 25 0 1 0 421605990 26783744 5971 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6539 5971 603 41 0 6498 0
vsize: 26156
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6005 0 0 0 59981 22 0 0 25 0 1 0 421605990 26783744 5982 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6539 5982 603 41 0 6498 0
vsize: 26156
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6285 0 0 0 60981 22 0 0 25 0 1 0 421605990 28004352 6262 4294967295 134512640 134672761 3221224576 3221223548 1075358820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6262 603 41 0 6796 0
vsize: 27348
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6605 0 0 0 61980 23 0 0 25 0 1 0 421605990 29245440 6582 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7140 6582 603 41 0 7099 0
vsize: 28560
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6605 0 0 0 62980 23 0 0 25 0 1 0 421605990 29245440 6582 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7140 6582 603 41 0 7099 0
vsize: 28560
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6605 0 0 0 63980 23 0 0 25 0 1 0 421605990 29245440 6582 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7140 6582 603 41 0 7099 0
vsize: 28560
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6606 0 0 0 64981 23 0 0 25 0 1 0 421605990 29245440 6583 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7140 6583 603 41 0 7099 0
vsize: 28560
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6799 0 0 0 65980 24 0 0 25 0 1 0 421605990 30052352 6776 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7337 6776 603 41 0 7296 0
vsize: 29348
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6799 0 0 0 66980 24 0 0 25 0 1 0 421605990 30052352 6776 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7337 6776 603 41 0 7296 0
vsize: 29348
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6800 0 0 0 67980 24 0 0 25 0 1 0 421605990 30052352 6777 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7337 6777 603 41 0 7296 0
vsize: 29348
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 6810 0 0 0 68980 24 0 0 25 0 1 0 421605990 30052352 6787 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7337 6787 603 41 0 7296 0
vsize: 29348
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7264 0 0 0 69979 26 0 0 25 0 1 0 421605990 31924224 7241 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7794 7241 603 41 0 7753 0
vsize: 31176
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7264 0 0 0 70979 26 0 0 25 0 1 0 421605990 31924224 7241 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7794 7241 603 41 0 7753 0
vsize: 31176
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7265 0 0 0 71979 26 0 0 25 0 1 0 421605990 31924224 7242 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7794 7242 603 41 0 7753 0
vsize: 31176
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7270 0 0 0 72980 26 0 0 25 0 1 0 421605990 32063488 7247 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7828 7247 603 41 0 7787 0
vsize: 31312
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7445 0 0 0 73980 26 0 0 25 0 1 0 421605990 32727040 7422 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7990 7422 603 41 0 7949 0
vsize: 31960
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7445 0 0 0 74980 26 0 0 25 0 1 0 421605990 32727040 7422 4294967295 134512640 134672761 3221224576 3221223680 134560523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7990 7422 603 41 0 7949 0
vsize: 31960
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7453 0 0 0 75980 26 0 0 25 0 1 0 421605990 32727040 7430 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7990 7430 603 41 0 7949 0
vsize: 31960
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7454 0 0 0 76980 26 0 0 25 0 1 0 421605990 32727040 7431 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7990 7431 603 41 0 7949 0
vsize: 31960
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7463 0 0 0 77980 26 0 0 25 0 1 0 421605990 32899072 7440 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7440 603 41 0 7991 0
vsize: 32128
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 78980 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 79981 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 80981 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223660 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 81981 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 82981 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 83982 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 84982 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223532 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 85982 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 86982 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 87982 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 88982 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 89983 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7465 0 0 0 90983 26 0 0 25 0 1 0 421605990 32899072 7442 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7442 603 41 0 7991 0
vsize: 32128
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7476 0 0 0 91983 26 0 0 25 0 1 0 421605990 32899072 7453 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8032 7453 603 41 0 7991 0
vsize: 32128
[startup+930.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7523 0 0 0 92983 26 0 0 25 0 1 0 421605990 33165312 7500 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8097 7500 603 41 0 8056 0
vsize: 32388
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7523 0 0 0 93983 26 0 0 25 0 1 0 421605990 33165312 7500 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8097 7500 603 41 0 8056 0
vsize: 32388
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7523 0 0 0 94982 26 0 0 25 0 1 0 421605990 33165312 7500 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8097 7500 603 41 0 8056 0
vsize: 32388
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7563 0 0 0 95982 26 0 0 25 0 1 0 421605990 33300480 7540 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8130 7540 603 41 0 8089 0
vsize: 32520
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7618 0 0 0 96982 27 0 0 25 0 1 0 421605990 33435648 7595 4294967295 134512640 134672761 3221224576 3221223760 134558667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8163 7595 603 41 0 8122 0
vsize: 32652
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7618 0 0 0 97983 27 0 0 25 0 1 0 421605990 33435648 7595 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8163 7595 603 41 0 8122 0
vsize: 32652
[startup+990.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7618 0 0 0 98983 27 0 0 25 0 1 0 421605990 33435648 7595 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8163 7595 603 41 0 8122 0
vsize: 32652
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7685 0 0 0 99983 27 0 0 25 0 1 0 421605990 33837056 7662 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7662 603 41 0 8220 0
vsize: 33044
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7685 0 0 0 100983 27 0 0 25 0 1 0 421605990 33837056 7662 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7662 603 41 0 8220 0
vsize: 33044
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7691 0 0 0 101983 27 0 0 25 0 1 0 421605990 33837056 7668 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7668 603 41 0 8220 0
vsize: 33044
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7691 0 0 0 102983 27 0 0 25 0 1 0 421605990 33837056 7668 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7668 603 41 0 8220 0
vsize: 33044
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 7691 0 0 0 103983 27 0 0 25 0 1 0 421605990 33837056 7668 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8261 7668 603 41 0 8220 0
vsize: 33044
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8229 0 0 0 104982 29 0 0 25 0 1 0 421605990 35991552 8206 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8787 8206 603 41 0 8746 0
vsize: 35148
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8391 0 0 0 105982 29 0 0 25 0 1 0 421605990 36651008 8368 4294967295 134512640 134672761 3221224576 3221223744 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8948 8368 603 41 0 8907 0
vsize: 35792
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8396 0 0 0 106982 29 0 0 25 0 1 0 421605990 36786176 8373 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8373 603 41 0 8940 0
vsize: 35924
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8419 0 0 0 107982 29 0 0 25 0 1 0 421605990 36786176 8396 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8396 603 41 0 8940 0
vsize: 35924
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8422 0 0 0 108982 29 0 0 25 0 1 0 421605990 36950016 8399 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9021 8399 603 41 0 8980 0
vsize: 36084
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8541 0 0 0 109982 29 0 0 25 0 1 0 421605990 37351424 8518 4294967295 134512640 134672761 3221224576 3221223744 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9119 8518 603 41 0 9078 0
vsize: 36476
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8804 0 0 0 110981 31 0 0 25 0 1 0 421605990 38412288 8781 4294967295 134512640 134672761 3221224576 3221223680 134560523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9378 8781 603 41 0 9337 0
vsize: 37512
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8806 0 0 0 111981 31 0 0 25 0 1 0 421605990 38412288 8783 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9378 8783 603 41 0 9337 0
vsize: 37512
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8820 0 0 0 112981 31 0 0 25 0 1 0 421605990 38567936 8797 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9416 8797 603 41 0 9375 0
vsize: 37664
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8830 0 0 0 113982 31 0 0 25 0 1 0 421605990 38567936 8807 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9416 8807 603 41 0 9375 0
vsize: 37664
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8830 0 0 0 114982 31 0 0 25 0 1 0 421605990 38567936 8807 4294967295 134512640 134672761 3221224576 3221223760 134558632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9416 8807 603 41 0 9375 0
vsize: 37664
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8830 0 0 0 115982 31 0 0 25 0 1 0 421605990 38567936 8807 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9416 8807 603 41 0 9375 0
vsize: 37664
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8830 0 0 0 116982 31 0 0 25 0 1 0 421605990 38567936 8807 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9416 8807 603 41 0 9375 0
vsize: 37664
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8830 0 0 0 117982 31 0 0 25 0 1 0 421605990 38567936 8807 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9416 8807 603 41 0 9375 0
vsize: 37664
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8830 0 0 0 118983 31 0 0 25 0 1 0 421605990 38567936 8807 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9416 8807 603 41 0 9375 0
vsize: 37664
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5441
Raw data (stat): 5441 (minisat+) R 5440 32461 32460 0 -1 0 8831 0 0 0 119983 31 0 0 25 0 1 0 421605990 38567936 8808 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9416 8808 603 41 0 9375 0
vsize: 37664
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 5441
Raw data (stat): 5441 (minisat+) Z 5440 32461 32460 0 -1 12 8833 0 0 0 119983 32 0 0 25 0 1 0 421605990 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.04
CPU time (s): 1200.16
CPU user time (s): 1199.83
CPU system time (s): 0.329949
CPU usage (%): 100.01
Max. virtual memory (Kb): 37664
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####