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/MIPLIB/miplib2003/normalized-mps-v2-13-7-fixnet6.opb
MD5SUM	08a1ce7c6c4cc8e461ae1aeabdf15da0
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3289593
Optimality of the best value was proved	NO
Number of terms in the objective function	8282
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	524133752
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	524133752
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.04
Number of variables	9890
Total number of constraints	978
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	378
Number of constraints which are nor clauses,nor cardinality constraints	600
Minimum length of a constraint	1
Maximum length of a constraint	1072
Trace number 15430

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 04:22:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17547 boxname=wulflinc12 idbench=1350 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  08a1ce7c6c4cc8e461ae1aeabdf15da0  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-fixnet6.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-fixnet6.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-fixnet6.opb
IDLAUNCH: 17547
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        797812 kB
Buffers:         26616 kB
Cached:         188220 kB
SwapCached:        316 kB
Active:          38380 kB
Inactive:       178724 kB
HighTotal:      131008 kB
HighFree:        12376 kB
LowTotal:       903652 kB
LowFree:        785436 kB
SwapTotal:     2097136 kB
SwapFree:      2096236 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            14072 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:42:57 (client local time) WITH STATUS 0 IN 1200.41 SECONDS
stats: 17547 7 1200.41 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 700 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssss
c ---[ 593]---> Adder-cost: 84   maxlim: 68348   bits: 18/17
c ---[ 591]---> Adder-cost: 868   maxlim: 359136   bits: 20/19
c ---[ 589]---> Adder-cost: 77   maxlim: 768   bits: 11/10
c ---[ 588]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 587]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 586]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 585]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 584]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 583]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 582]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 581]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 580]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 578]---> Adder-cost: 657   maxlim: 219625   bits: 19/18
c ---[ 577]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 576]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 575]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 574]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 573]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 572]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 571]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 570]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 569]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 568]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 566]---> Adder-cost: 342   maxlim: 75000   bits: 18/17
c ---[ 565]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 564]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 563]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 562]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 561]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 560]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 559]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 558]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 557]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 556]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 554]---> Adder-cost: 1288   maxlim: 642508   bits: 20/20
c ---[ 553]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 552]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 551]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 550]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 549]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 548]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 547]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 546]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 545]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 544]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 542]---> Adder-cost: 512   maxlim: 285163   bits: 19/19
c ---[ 541]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 540]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 539]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 538]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 537]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 536]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 535]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 534]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 533]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 532]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 530]---> Adder-cost: 519   maxlim: 215791   bits: 19/18
c ---[ 529]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 528]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 527]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 526]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 525]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 524]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 523]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 522]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 521]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 520]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 518]---> Adder-cost: 468   maxlim: 216816   bits: 19/18
c ---[ 517]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 516]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 515]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 514]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 513]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 512]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 511]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 510]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 509]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 508]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 506]---> Adder-cost: 191   maxlim: 70139   bits: 18/17
c ---[ 505]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 504]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 503]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 502]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 501]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 500]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 499]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 498]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 497]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 496]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 494]---> Adder-cost: 1230   maxlim: 826322   bits: 21/20
c ---[ 493]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 492]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 491]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 490]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 489]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 488]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 487]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 486]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 485]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 484]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 482]---> Adder-cost: 1152   maxlim: 575183   bits: 20/20
c ---[ 481]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 480]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 479]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 478]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 477]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 476]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 475]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 474]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 473]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 472]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 470]---> Adder-cost: 896   maxlim: 492249   bits: 20/19
c ---[ 468]---> Adder-cost: 390   maxlim: 79860   bits: 18/17
c ---[ 467]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 466]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 465]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 464]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 463]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 462]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 461]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 460]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 459]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 458]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 456]---> Adder-cost: 66   maxlim: 1280   bits: 12/11
c ---[ 455]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 454]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 453]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 452]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 451]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 450]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 449]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 448]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 447]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 446]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 444]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 443]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 442]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 441]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 440]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 439]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 438]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 437]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 436]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 435]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 434]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 432]---> Adder-cost: 98   maxlim: 768   bits: 11/10
c ---[ 431]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 430]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 429]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 428]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 427]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 426]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 425]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 424]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 423]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 422]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 420]---> Adder-cost: 69   maxlim: 256   bits: 10/9
c ---[ 419]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 418]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 417]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 416]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 415]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 414]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 413]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 412]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 411]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 410]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 408]---> Adder-cost: 66   maxlim: 1408   bits: 12/11
c ---[ 407]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 406]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 405]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 404]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 403]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 402]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 401]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 400]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 399]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 398]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 396]---> Adder-cost: 39   maxlim: 768   bits: 11/10
c ---[ 395]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 394]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 393]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 392]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 391]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 390]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 389]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 388]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 387]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 386]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 384]---> Adder-cost: 35   maxlim: 384   bits: 10/9
c ---[ 383]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 382]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 381]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 380]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 379]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 378]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 377]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 376]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 375]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 374]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 372]---> Adder-cost: 117   maxlim: 768   bits: 11/10
c ---[ 371]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 370]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 369]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 368]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 367]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 366]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 365]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 364]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 363]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 362]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 360]---> Adder-cost: 66   maxlim: 1920   bits: 12/11
c ---[ 359]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 358]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 357]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 356]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 355]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 354]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 353]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 352]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 351]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 350]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 348]---> Adder-cost: 224   maxlim: 140282   bits: 19/18
c ---[ 346]---> Adder-cost: 124   maxlim: 384   bits: 10/9
c ---[ 345]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 344]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 343]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 342]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 341]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 340]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 339]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 338]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 337]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 336]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 334]---> Adder-cost: 93   maxlim: 128   bits: 9/8
c ---[ 333]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 332]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 331]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 330]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 329]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 328]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 327]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 326]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 325]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 324]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 322]---> Adder-cost: 98   maxlim: 512   bits: 11/10
c ---[ 321]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 320]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 319]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 318]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 317]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 316]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 315]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 314]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 313]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 312]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 310]---> Adder-cost: 43   maxlim: 1280   bits: 12/11
c ---[ 309]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 308]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 307]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 306]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 305]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 304]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 303]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 302]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 301]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 300]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 298]---> Adder-cost: 66   maxlim: 1408   bits: 12/11
c ---[ 297]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 296]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 295]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 294]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 293]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 292]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 291]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 290]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 289]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 288]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 286]---> Adder-cost: 117   maxlim: 768   bits: 11/10
c ---[ 285]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 284]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 283]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 282]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 281]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 280]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 279]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 278]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 277]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 276]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 274]---> Adder-cost: 117   maxlim: 640   bits: 11/10
c ---[ 273]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 272]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 271]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 270]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 269]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 268]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 267]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 266]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 265]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 264]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 262]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 261]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 260]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 259]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 258]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 257]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 256]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 255]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 254]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 253]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 252]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 250]---> Adder-cost: 54   maxlim: 256   bits: 10/9
c ---[ 249]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 248]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 247]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 246]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 245]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 244]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 243]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 242]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 241]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 240]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 238]---> Adder-cost: 93   maxlim: 3584   bits: 13/12
c ---[ 237]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 236]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 235]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 234]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 233]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 232]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 231]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 230]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 229]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 228]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 226]---> Adder-cost: 1068   maxlim: 306133   bits: 20/19
c ---[ 224]---> Adder-cost: 117   maxlim: 512   bits: 11/10
c ---[ 223]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 222]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 221]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 220]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 219]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 218]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 217]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 216]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 215]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 214]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 212]---> Adder-cost: 153   maxlim: 768   bits: 11/10
c ---[ 211]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 210]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 209]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 208]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 207]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 206]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 205]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 204]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 203]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 202]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 200]---> Adder-cost: 98   maxlim: 640   bits: 11/10
c ---[ 199]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 198]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 197]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 196]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 195]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 194]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 193]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 192]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 191]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 190]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 188]---> Adder-cost: 39   maxlim: 768   bits: 11/10
c ---[ 187]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 186]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 185]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 184]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 183]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 182]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 181]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 180]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 179]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 178]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 176]---> Adder-cost: 93   maxlim: 128   bits: 9/8
c ---[ 175]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 174]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 173]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 172]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 171]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 170]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 169]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 168]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 167]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 166]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 164]---> Adder-cost: 98   maxlim: 896   bits: 11/10
c ---[ 163]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 162]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 161]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 160]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 159]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 158]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 157]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 156]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 155]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 154]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 152]---> Adder-cost: 60   maxlim: 512   bits: 11/10
c ---[ 151]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 150]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 149]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 148]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 147]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 146]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 145]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 144]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 143]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 142]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 140]---> Adder-cost: 77   maxlim: 640   bits: 11/10
c ---[ 139]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 138]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 137]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 136]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 135]---> Adder-cost: 7   maxlim: 1022   bits: 11/10
c ---[ 134]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 9   maxlim: 2046   bits: 12/11
c ---[ 132]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 131]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 129]---> Adder-cost: 66   maxlim: 1408   bits: 12/11
c ---[ 127]---> Adder-cost: 88   maxlim: 384   bits: 10/9
c ---[ 125]---> Adder-cost: 536   maxlim: 216300   bits: 19/18
c ---[ 123]---> Adder-cost: 85   maxlim: 1152   bits: 12/11
c ---[ 121]---> Adder-cost: 60   maxlim: 512   bits: 11/10
c ---[ 119]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 117]---> Adder-cost: 54   maxlim: 384   bits: 10/9
c ---[ 115]---> Adder-cost: 66   maxlim: 1152   bits: 12/11
c ---[ 113]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 111]---> Adder-cost: 93   maxlim: 128   bits: 9/8
c ---[ 109]---> Adder-cost: 77   maxlim: 512   bits: 11/10
c ---[ 107]---> Adder-cost: 98   maxlim: 640   bits: 11/10
c ---[ 105]---> Adder-cost: 93   maxlim: 2048   bits: 13/12
c ---[ 103]---> Adder-cost: 958   maxlim: 434137   bits: 20/19
c ---[ 101]---> Adder-cost: 43   maxlim: 1152   bits: 12/11
c ---[  99]---> Adder-cost: 60   maxlim: 896   bits: 11/10
c ---[  97]---> Adder-cost: 152   maxlim: 1664   bits: 12/11
c ---[  95]---> Adder-cost: 85   maxlim: 1024   bits: 12/11
c ---[  93]---> Adder-cost: 117   maxlim: 512   bits: 11/10
c ---[  91]---> Adder-cost: 117   maxlim: 640   bits: 11/10
c ---[  89]---> Adder-cost: 108   maxlim: 1408   bits: 12/11
c ---[  87]---> Adder-cost: 85   maxlim: 1536   bits: 12/11
c ---[  85]---> Adder-cost: 105   maxlim: 384   bits: 10/9
c ---[  83]---> Adder-cost: 77   maxlim: 640   bits: 11/10
c ---[  81]---> Adder-cost: 518   maxlim: 272114   bits: 20/19
c ---[  79]---> Adder-cost: 98   maxlim: 512   bits: 11/10
c ---[  77]---> Adder-cost: 85   maxlim: 1280   bits: 12/11
c ---[  75]---> Adder-cost: 39   maxlim: 768   bits: 11/10
c ---[  73]---> Adder-cost: 108   maxlim: 1024   bits: 12/11
c ---[  71]---> Adder-cost: 60   maxlim: 768   bits: 11/10
c ---[  69]---> Adder-cost: 60   maxlim: 768   bits: 11/10
c ---[  67]---> Adder-cost: 60   maxlim: 768   bits: 11/10
c ---[  65]---> Adder-cost: 18   maxlim: 256   bits: 10/9
c ---[  63]---> Adder-cost: 78   maxlim: 128   bits: 9/8
c ---[  61]---> Adder-cost: 60   maxlim: 512   bits: 11/10
c ---[  59]---> Adder-cost: 824   maxlim: 289249   bits: 20/19
c ---[  57]---> Adder-cost: 69   maxlim: 256   bits: 10/9
c ---[  55]---> Adder-cost: 192   maxlim: 1024   bits: 12/11
c ---[  53]---> Adder-cost: 78   maxlim: 128   bits: 9/8
c ---[  51]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[  49]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[  47]---> Adder-cost: 66   maxlim: 1280   bits: 12/11
c ---[  45]---> Adder-cost: 98   maxlim: 896   bits: 11/10
c ---[  43]---> Adder-cost: 88   maxlim: 384   bits: 10/9
c ---[  41]---> Adder-cost: 117   maxlim: 896   bits: 11/10
c ---[  39]---> Adder-cost: 54   maxlim: 384   bits: 10/9
c ---[  37]---> Adder-cost: 620   maxlim: 346857   bits: 20/19
c ---[  35]---> Adder-cost: 98   maxlim: 512   bits: 11/10
c ---[  33]---> Adder-cost: 60   maxlim: 896   bits: 11/10
c ---[  31]---> Adder-cost: 66   maxlim: 1792   bits: 12/11
c ---[  29]---> Adder-cost: 66   maxlim: 1152   bits: 12/11
c ---[  27]---> Adder-cost: 98   maxlim: 768   bits: 11/10
c ---[  25]---> Adder-cost: 98   maxlim: 640   bits: 11/10
c ---[  23]---> Adder-cost: 85   maxlim: 1024   bits: 12/11
c ---[  21]---> Adder-cost: 61   maxlim: 128   bits: 9/8
c ---[  19]---> Adder-cost: 117   maxlim: 640   bits: 11/10
c ---[  17]---> Adder-cost: 54   maxlim: 256   bits: 10/9
c ---[  16]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  15]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  14]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  13]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  12]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  11]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  10]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   9]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   8]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   7]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   6]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   5]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   4]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   3]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   2]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   1]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   0]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  149078   548212 |   49692       0        0     nan |  0.000 % |
c |       104 |  149078   548212 |   54661     104      689     6.6 | 29.329 % |
c |       255 |  149070   548186 |   60127     254     1312     5.2 | 29.331 % |
c |       480 |  149070   548186 |   66140     479     2084     4.4 | 29.331 % |
c |       817 |  149062   548160 |   72754     815     3241     4.0 | 29.334 % |
c |      1324 |  149018   548022 |   80029    1321     4987     3.8 | 29.360 % |
c |      2083 |  149018   548022 |   88032    2080     7801     3.8 | 29.360 % |
c |      3222 |  149002   547970 |   96835    3217    12048     3.7 | 29.365 % |
c |      4931 |  148986   547918 |  106519    4924    20422     4.1 | 29.371 % |
c |      7493 |  148970   547870 |  117171    7483    33207     4.4 | 29.379 % |
c |     11337 |  148970   547870 |  128888   11327    56774     5.0 | 29.379 % |
c |     17103 |  148970   547870 |  141777   17093   112923     6.6 | 29.379 % |
c |     25752 |  148956   547826 |  155954   25740   209178     8.1 | 29.384 % |
c |     38727 |  148940   547778 |  171550   38713   334600     8.6 | 29.392 % |
c |     58190 |  148932   547752 |  188705   58175   664701    11.4 | 29.394 % |
c |     87382 |  148916   547700 |  207575   87365  1036297    11.9 | 29.400 % |
c |    131171 |  148908   547674 |  228333  131153  2079553    15.9 | 29.402 % |
c |    196855 |  148862   547526 |  251166  196831  3241035    16.5 | 29.418 % |
c |    295381 |  148822   547396 |  276283   69617   655599     9.4 | 29.431 % |
c |    443170 |  148822   547396 |  303911  217406  6398081    29.4 | 29.431 % |
#### 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.49 0.81 0.87 2/54 20293
Raw data (stat): 20293 (runsolver) R 20292 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483942593 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.57 0.82 0.87 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 4207 0 0 0 988 10 0 0 25 0 1 0 483942593 20004864 3976 4294967295 134512640 134672761 3221224544 3221223696 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4884 3976 603 41 0 4843 0
vsize: 19536
[startup+20.0016 s]
Raw data (loadavg): 0.63 0.82 0.87 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 4289 0 0 0 1988 10 0 0 25 0 1 0 483942593 20275200 4058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4950 4058 603 41 0 4909 0
vsize: 19800
[startup+30.0024 s]
Raw data (loadavg): 0.69 0.83 0.87 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 4442 0 0 0 2987 11 0 0 25 0 1 0 483942593 21028864 4211 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5134 4211 603 41 0 5093 0
vsize: 20536
[startup+40.0018 s]
Raw data (loadavg): 0.74 0.83 0.87 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 4586 0 0 0 3986 12 0 0 25 0 1 0 483942593 21569536 4355 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5266 4355 603 41 0 5225 0
vsize: 21064
[startup+50.0031 s]
Raw data (loadavg): 0.78 0.84 0.87 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 4694 0 0 0 4986 13 0 0 25 0 1 0 483942593 21975040 4463 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5365 4463 603 41 0 5324 0
vsize: 21460
[startup+60.004 s]
Raw data (loadavg): 0.81 0.84 0.87 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 4797 0 0 0 5986 13 0 0 25 0 1 0 483942593 22503424 4566 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4566 603 41 0 5453 0
vsize: 21976
[startup+70.0054 s]
Raw data (loadavg): 0.84 0.85 0.87 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 4899 0 0 0 6985 14 0 0 25 0 1 0 483942593 22908928 4668 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5593 4668 603 41 0 5552 0
vsize: 22372
[startup+80.0067 s]
Raw data (loadavg): 0.86 0.85 0.87 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 5037 0 0 0 7984 15 0 0 25 0 1 0 483942593 23449600 4806 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5725 4806 603 41 0 5684 0
vsize: 22900
[startup+90.0065 s]
Raw data (loadavg): 0.88 0.86 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 5150 0 0 0 8984 15 0 0 25 0 1 0 483942593 23855104 4919 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5824 4919 603 41 0 5783 0
vsize: 23296
[startup+100.007 s]
Raw data (loadavg): 0.90 0.86 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 5424 0 0 0 9983 17 0 0 25 0 1 0 483942593 24932352 5193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6087 5193 603 41 0 6046 0
vsize: 24348
[startup+110.008 s]
Raw data (loadavg): 0.92 0.86 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 5523 0 0 0 10982 18 0 0 25 0 1 0 483942593 25333760 5292 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6185 5292 603 41 0 6144 0
vsize: 24740
[startup+120.01 s]
Raw data (loadavg): 0.93 0.87 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 5609 0 0 0 11981 19 0 0 25 0 1 0 483942593 25997312 5378 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6347 5378 603 41 0 6306 0
vsize: 25388
[startup+130.01 s]
Raw data (loadavg): 0.94 0.87 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 5741 0 0 0 12980 19 0 0 25 0 1 0 483942593 26537984 5510 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6479 5510 603 41 0 6438 0
vsize: 25916
[startup+140.011 s]
Raw data (loadavg): 0.95 0.88 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 5922 0 0 0 13980 20 0 0 25 0 1 0 483942593 27213824 5691 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6644 5691 603 41 0 6603 0
vsize: 26576
[startup+150.011 s]
Raw data (loadavg): 0.95 0.88 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 6042 0 0 0 14979 21 0 0 25 0 1 0 483942593 27619328 5811 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6743 5811 603 41 0 6702 0
vsize: 26972
[startup+160.011 s]
Raw data (loadavg): 0.96 0.88 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 6170 0 0 0 15978 22 0 0 25 0 1 0 483942593 28160000 5939 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6875 5939 603 41 0 6834 0
vsize: 27500
[startup+170.012 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 6387 0 0 0 16978 23 0 0 25 0 1 0 483942593 29102080 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7105 6156 603 41 0 7064 0
vsize: 28420
[startup+180.013 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 6604 0 0 0 17977 24 0 0 25 0 1 0 483942593 29913088 6373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7303 6373 603 41 0 7262 0
vsize: 29212
[startup+190.013 s]
Raw data (loadavg): 0.98 0.89 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 7228 0 0 0 18975 27 0 0 25 0 1 0 483942593 32481280 6997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7930 6997 603 41 0 7889 0
vsize: 31720
[startup+200.013 s]
Raw data (loadavg): 0.98 0.90 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 7406 0 0 0 19974 27 0 0 25 0 1 0 483942593 33153024 7175 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8094 7175 603 41 0 8053 0
vsize: 32376
[startup+210.013 s]
Raw data (loadavg): 0.98 0.90 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 7480 0 0 0 20974 28 0 0 25 0 1 0 483942593 33423360 7249 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8160 7249 603 41 0 8119 0
vsize: 32640
[startup+220.014 s]
Raw data (loadavg): 0.98 0.90 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 7568 0 0 0 21973 28 0 0 25 0 1 0 483942593 33693696 7337 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8226 7337 603 41 0 8185 0
vsize: 32904
[startup+230.027 s]
Raw data (loadavg): 0.99 0.90 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 7664 0 0 0 22974 29 0 0 25 0 1 0 483942593 34619392 7433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8452 7433 603 41 0 8411 0
vsize: 33808
[startup+240.049 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 7728 0 0 0 23976 29 0 0 25 0 1 0 483942593 34889728 7497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8518 7497 603 41 0 8477 0
vsize: 34072
[startup+250.049 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 7798 0 0 0 24975 31 0 0 25 0 1 0 483942593 35160064 7567 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8584 7567 603 41 0 8543 0
vsize: 34336
[startup+260.152 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 7849 0 0 0 25985 31 0 0 25 0 1 0 483942593 35430400 7618 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8650 7618 603 41 0 8609 0
vsize: 34600
[startup+270.153 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 7913 0 0 0 26985 31 0 0 25 0 1 0 483942593 35565568 7682 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8683 7682 603 41 0 8642 0
vsize: 34732
[startup+280.153 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 8020 0 0 0 27984 32 0 0 25 0 1 0 483942593 36106240 7789 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8815 7789 603 41 0 8774 0
vsize: 35260
[startup+290.153 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 8396 0 0 0 28983 33 0 0 25 0 1 0 483942593 37584896 8165 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9176 8165 603 41 0 9135 0
vsize: 36704
[startup+300.154 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 8468 0 0 0 29982 34 0 0 25 0 1 0 483942593 37855232 8237 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9242 8237 603 41 0 9201 0
vsize: 36968
[startup+310.153 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 8534 0 0 0 30982 35 0 0 25 0 1 0 483942593 38125568 8303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9308 8303 603 41 0 9267 0
vsize: 37232
[startup+320.196 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 8604 0 0 0 31986 35 0 0 25 0 1 0 483942593 38395904 8373 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9374 8373 603 41 0 9333 0
vsize: 37496
[startup+330.211 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 8654 0 0 0 32988 35 0 0 25 0 1 0 483942593 38531072 8423 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9407 8423 603 41 0 9366 0
vsize: 37628
[startup+340.211 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 8749 0 0 0 33987 36 0 0 25 0 1 0 483942593 38936576 8518 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8518 603 41 0 9465 0
vsize: 38024
[startup+350.212 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9189 0 0 0 34985 37 0 0 25 0 1 0 483942593 40685568 8958 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9933 8958 603 41 0 9892 0
vsize: 39732
[startup+360.212 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9262 0 0 0 35985 38 0 0 25 0 1 0 483942593 40955904 9031 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9999 9031 603 41 0 9958 0
vsize: 39996
[startup+370.213 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9350 0 0 0 36985 38 0 0 25 0 1 0 483942593 41361408 9119 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10098 9119 603 41 0 10057 0
vsize: 40392
[startup+380.214 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9458 0 0 0 37984 39 0 0 25 0 1 0 483942593 41766912 9227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10197 9227 603 41 0 10156 0
vsize: 40788
[startup+390.213 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9568 0 0 0 38984 40 0 0 25 0 1 0 483942593 42172416 9337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10296 9337 603 41 0 10255 0
vsize: 41184
[startup+400.215 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9628 0 0 0 39984 40 0 0 25 0 1 0 483942593 42438656 9397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10361 9397 603 41 0 10320 0
vsize: 41444
[startup+410.214 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9671 0 0 0 40983 41 0 0 25 0 1 0 483942593 42573824 9440 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10394 9440 603 41 0 10353 0
vsize: 41576
[startup+420.214 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9721 0 0 0 41983 41 0 0 25 0 1 0 483942593 42844160 9490 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10460 9490 603 41 0 10419 0
vsize: 41840
[startup+430.215 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9763 0 0 0 42983 41 0 0 25 0 1 0 483942593 42979328 9532 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10493 9532 603 41 0 10452 0
vsize: 41972
[startup+440.215 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9819 0 0 0 43983 42 0 0 25 0 1 0 483942593 43114496 9588 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10526 9588 603 41 0 10485 0
vsize: 42104
[startup+450.215 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9881 0 0 0 44983 42 0 0 25 0 1 0 483942593 43384832 9650 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10592 9650 603 41 0 10551 0
vsize: 42368
[startup+460.215 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9937 0 0 0 45983 42 0 0 25 0 1 0 483942593 43655168 9706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10658 9706 603 41 0 10617 0
vsize: 42632
[startup+470.215 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 9978 0 0 0 46983 42 0 0 25 0 1 0 483942593 43790336 9747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10691 9747 603 41 0 10650 0
vsize: 42764
[startup+480.216 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 10029 0 0 0 47983 42 0 0 25 0 1 0 483942593 43925504 9798 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10724 9798 603 41 0 10683 0
vsize: 42896
[startup+490.216 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 10109 0 0 0 48983 42 0 0 25 0 1 0 483942593 44331008 9878 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10823 9878 603 41 0 10782 0
vsize: 43292
[startup+500.216 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 10196 0 0 0 49983 42 0 0 25 0 1 0 483942593 44601344 9965 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10889 9965 603 41 0 10848 0
vsize: 43556
[startup+510.216 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 10470 0 0 0 50983 43 0 0 25 0 1 0 483942593 45682688 10239 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11153 10239 603 41 0 11112 0
vsize: 44612
[startup+520.216 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 10559 0 0 0 51982 44 0 0 25 0 1 0 483942593 46088192 10328 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10328 603 41 0 11211 0
vsize: 45008
[startup+530.216 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 10623 0 0 0 52982 44 0 0 25 0 1 0 483942593 46358528 10392 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11318 10392 603 41 0 11277 0
vsize: 45272
[startup+540.217 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 10687 0 0 0 53982 44 0 0 25 0 1 0 483942593 46628864 10456 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11384 10456 603 41 0 11343 0
vsize: 45536
[startup+550.217 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 10765 0 0 0 54982 44 0 0 25 0 1 0 483942593 46899200 10534 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11450 10534 603 41 0 11409 0
vsize: 45800
[startup+560.217 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 10965 0 0 0 55982 45 0 0 25 0 1 0 483942593 47706112 10734 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11647 10734 603 41 0 11606 0
vsize: 46588
[startup+570.217 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11051 0 0 0 56982 45 0 0 25 0 1 0 483942593 47976448 10820 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11713 10820 603 41 0 11672 0
vsize: 46852
[startup+580.217 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11142 0 0 0 57982 45 0 0 25 0 1 0 483942593 48381952 10911 4294967295 134512640 134672761 3221224544 3221223792 134562762 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11812 10911 603 41 0 11771 0
vsize: 47248
[startup+590.218 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 58982 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+600.219 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 59982 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+610.219 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 60982 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+620.219 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 61982 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+630.22 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 62983 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+640.22 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 63983 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+650.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 64983 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+660.221 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 65983 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223788 134561422 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+670.221 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 66983 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+680.221 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 67983 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223680 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+690.221 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 68983 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+700.221 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 69983 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+710.221 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 70983 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+720.221 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 71984 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+730.222 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 72984 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+740.222 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11274 0 0 0 73984 46 0 0 25 0 1 0 483942593 49971200 11043 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11043 603 41 0 12159 0
vsize: 48800
[startup+750.222 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11279 0 0 0 74984 46 0 0 25 0 1 0 483942593 49971200 11048 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11048 603 41 0 12159 0
vsize: 48800
[startup+760.222 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11279 0 0 0 75984 46 0 0 25 0 1 0 483942593 49971200 11048 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11048 603 41 0 12159 0
vsize: 48800
[startup+770.222 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11279 0 0 0 76984 46 0 0 25 0 1 0 483942593 49971200 11048 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11048 603 41 0 12159 0
vsize: 48800
[startup+780.224 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11279 0 0 0 77984 46 0 0 25 0 1 0 483942593 49971200 11048 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12200 11048 603 41 0 12159 0
vsize: 48800
[startup+790.224 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 11279 0 0 0 78984 46 0 0 25 0 1 0 483942593 49971200 11048 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12200 11048 603 41 0 12159 0
vsize: 48800
[startup+800.224 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 12134 0 0 0 79982 48 0 0 25 0 1 0 483942593 53456896 11903 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13051 11903 603 41 0 13010 0
vsize: 52204
[startup+810.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 12227 0 0 0 80982 48 0 0 25 0 1 0 483942593 53862400 11996 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13150 11996 603 41 0 13109 0
vsize: 52600
[startup+820.224 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 12312 0 0 0 81982 48 0 0 25 0 1 0 483942593 54267904 12081 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13249 12081 603 41 0 13208 0
vsize: 52996
[startup+830.224 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 12381 0 0 0 82982 49 0 0 25 0 1 0 483942593 54538240 12150 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13315 12150 603 41 0 13274 0
vsize: 53260
[startup+840.224 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 12503 0 0 0 83981 49 0 0 25 0 1 0 483942593 55074816 12272 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13446 12272 603 41 0 13405 0
vsize: 53784
[startup+850.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 12584 0 0 0 84981 50 0 0 25 0 1 0 483942593 55345152 12353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13512 12353 603 41 0 13471 0
vsize: 54048
[startup+860.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 12706 0 0 0 85982 50 0 0 25 0 1 0 483942593 55885824 12475 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13644 12475 603 41 0 13603 0
vsize: 54576
[startup+870.224 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 12788 0 0 0 86981 50 0 0 25 0 1 0 483942593 56156160 12557 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13710 12557 603 41 0 13669 0
vsize: 54840
[startup+880.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 13080 0 0 0 87980 51 0 0 25 0 1 0 483942593 57368576 12849 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14006 12849 603 41 0 13965 0
vsize: 56024
[startup+890.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 13176 0 0 0 88980 51 0 0 25 0 1 0 483942593 57774080 12945 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14105 12945 603 41 0 14064 0
vsize: 56420
[startup+900.226 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 13275 0 0 0 89980 52 0 0 25 0 1 0 483942593 58179584 13044 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14204 13044 603 41 0 14163 0
vsize: 56816
[startup+910.226 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 13348 0 0 0 90980 52 0 0 25 0 1 0 483942593 58449920 13117 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14270 13117 603 41 0 14229 0
vsize: 57080
[startup+920.227 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 13552 0 0 0 91980 52 0 0 25 0 1 0 483942593 59260928 13321 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14468 13321 603 41 0 14427 0
vsize: 57872
[startup+930.227 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 13809 0 0 0 92979 53 0 0 25 0 1 0 483942593 60338176 13578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14731 13578 603 41 0 14690 0
vsize: 58924
[startup+940.227 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 13897 0 0 0 93979 53 0 0 25 0 1 0 483942593 60739584 13666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14829 13666 603 41 0 14788 0
vsize: 59316
[startup+950.228 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 14007 0 0 0 94979 54 0 0 25 0 1 0 483942593 61140992 13776 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14927 13776 603 41 0 14886 0
vsize: 59708
[startup+960.229 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 14102 0 0 0 95978 54 0 0 25 0 1 0 483942593 61546496 13871 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15026 13871 603 41 0 14985 0
vsize: 60104
[startup+970.229 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 14589 0 0 0 96976 56 0 0 25 0 1 0 483942593 63565824 14358 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15519 14358 603 41 0 15478 0
vsize: 62076
[startup+980.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 14785 0 0 0 97976 57 0 0 25 0 1 0 483942593 64368640 14554 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15715 14554 603 41 0 15674 0
vsize: 62860
[startup+990.229 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 14879 0 0 0 98976 57 0 0 25 0 1 0 483942593 64770048 14648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15813 14648 603 41 0 15772 0
vsize: 63252
[startup+1000.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 15000 0 0 0 99976 57 0 0 25 0 1 0 483942593 65175552 14769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15912 14769 603 41 0 15871 0
vsize: 63648
[startup+1010.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 15181 0 0 0 100976 58 0 0 25 0 1 0 483942593 65986560 14950 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16110 14950 603 41 0 16069 0
vsize: 64440
[startup+1020.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 15321 0 0 0 101975 58 0 0 25 0 1 0 483942593 66527232 15090 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16242 15090 603 41 0 16201 0
vsize: 64968
[startup+1030.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 15516 0 0 0 102975 59 0 0 25 0 1 0 483942593 67334144 15285 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16439 15285 603 41 0 16398 0
vsize: 65756
[startup+1040.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 16137 0 0 0 103973 61 0 0 25 0 1 0 483942593 69894144 15906 4294967295 134512640 134672761 3221224544 3221223720 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17064 15906 603 41 0 17023 0
vsize: 68256
[startup+1050.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 17088 0 0 0 104971 63 0 0 25 0 1 0 483942593 73666560 16857 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17985 16857 603 41 0 17944 0
vsize: 71940
[startup+1060.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 17630 0 0 0 105970 64 0 0 25 0 1 0 483942593 75833344 17399 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18514 17399 603 41 0 18473 0
vsize: 74056
[startup+1070.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18095 0 0 0 106969 66 0 0 25 0 1 0 483942593 77705216 17864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18971 17864 603 41 0 18930 0
vsize: 75884
[startup+1080.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 107969 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223280 134565848 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1090.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 108969 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1100.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 109969 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1110.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 110969 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1120.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 111969 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1130.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 112969 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1140.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 113970 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1150.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 114970 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1160.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 115970 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1170.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 116970 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1180.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 117970 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1190.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 118971 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
[startup+1200.24 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20293
Raw data (stat): 20293 (minisat+) R 20292 25285 25284 0 -1 0 18237 0 0 0 119971 66 0 0 25 0 1 0 483942593 78245888 18006 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19103 18006 603 41 0 19062 0
vsize: 76412
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.27 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 20293
Raw data (stat): 20293 (minisat+) Z 20292 25285 25284 0 -1 12 18239 0 0 0 119971 69 0 0 25 0 1 0 483942593 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.27
CPU time (s): 1200.41
CPU user time (s): 1199.71
CPU system time (s): 0.698893
CPU usage (%): 100.012
Max. virtual memory (Kb): 76412
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####