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/radar/normalized-30:30:4.5:0.95:98.opb
MD5SUM	5f5bedf3690a537deb8cc97cc5d565ae
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	94
Optimality of the best value was proved	NO
Number of terms in the objective function	4624
Biggest coefficient in the objective function	2577
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	13335
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	2577
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	13335
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07084
Number of variables	4624
Total number of constraints	9886
Number of constraints which are clauses	4404
Number of constraints which are cardinality constraints (but not clauses)	5482
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	22
Trace number 5319

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-13 23:22:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3758 boxname=wulflinc15 idbench=374 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5f5bedf3690a537deb8cc97cc5d565ae  /oldhome/oroussel/tmp/wulflinc15/normalized-30:30:4.5:0.95:98.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc15/normalized-30:30:4.5:0.95:98.opb /oldhome/oroussel/tmp/wulflinc15/normalized-30:30:4.5:0.95:98.opb
IDLAUNCH: 3758
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        905032 kB
Buffers:         34960 kB
Cached:          73328 kB
SwapCached:       2144 kB
Active:          63320 kB
Inactive:        49924 kB
HighTotal:      131008 kB
HighFree:        53900 kB
LowTotal:       903652 kB
LowFree:        851132 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10892 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:42:48 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 3758 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5262 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 870]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 869]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 868]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 867]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 866]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 865]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 864]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 863]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 862]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 861]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 860]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 859]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 858]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 857]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 856]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 855]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 854]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 853]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 852]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 851]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 850]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 849]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 848]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 843]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 842]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 841]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 840]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 839]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 838]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 837]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 836]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 835]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 834]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 833]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 832]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 831]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 830]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 829]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 828]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 827]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 826]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 825]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 824]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 823]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 821]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 817]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 816]---> Adder-cost: 20   maxlim: 1   bits: 2/1
c ---[ 815]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 814]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 813]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 812]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 811]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 810]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 809]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 808]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 807]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 806]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 805]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 804]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 803]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 802]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 801]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 800]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 799]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 798]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 797]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 796]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 795]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 794]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 793]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 792]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 789]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 788]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 787]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 786]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 785]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 784]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 783]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 782]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 781]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 780]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 779]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 778]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 777]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 776]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 775]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 774]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 773]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 772]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 771]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 770]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 769]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 768]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 767]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 766]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 765]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 764]---> Adder-cost: 14   maxlim: 1   bits: 2/1
c ---[ 763]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 762]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 761]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 760]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 759]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 758]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 757]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 756]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 755]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 754]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 753]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 752]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 751]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 750]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 749]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 748]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 747]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 746]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 745]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 744]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 743]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 742]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 741]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 740]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 739]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 738]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 737]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 736]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 735]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 734]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 733]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 732]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 731]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 730]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 729]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 728]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 727]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 726]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 725]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 724]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 723]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 722]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 721]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 720]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 719]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 718]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 717]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 716]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 715]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 714]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 713]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 712]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 711]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 710]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 709]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 708]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 707]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 706]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 705]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 704]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 703]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 702]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 701]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 700]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 699]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 698]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 697]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 696]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 695]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 694]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 693]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 692]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 691]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 690]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 689]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 688]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 687]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 686]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 685]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 684]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[ 683]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 682]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 681]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 680]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 679]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 678]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 677]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 676]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 675]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 674]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 673]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 672]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 671]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 670]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 669]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 668]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 667]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 666]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 665]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 664]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 663]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 662]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 661]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 660]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 659]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 658]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 657]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 656]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 655]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 654]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 653]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 652]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 651]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 650]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 649]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 648]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 647]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 646]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 645]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 644]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 643]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 642]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 641]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 640]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 639]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 638]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 637]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 636]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 635]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 634]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 633]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 632]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 631]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 630]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 629]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 628]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 627]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 626]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 625]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 624]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 623]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 622]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 621]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 620]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 619]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 618]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 617]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 616]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[ 615]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 614]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 613]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 612]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 611]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 610]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 609]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 608]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 607]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 606]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 605]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 604]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 603]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 602]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 601]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 600]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 599]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 598]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 597]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 596]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 595]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 594]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 593]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 592]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 591]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 590]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 589]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 588]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 587]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 586]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 585]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 584]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 583]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 582]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 581]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 580]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 579]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 578]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 577]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 576]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 575]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 574]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 573]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 572]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 571]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 570]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 569]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 568]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 567]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 566]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 565]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 564]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 563]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 562]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 561]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 560]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 559]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 558]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 557]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 556]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 555]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 554]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 553]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 552]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 551]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 550]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 549]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 548]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 547]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 546]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 545]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 544]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 543]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 542]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 541]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 540]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 539]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 538]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 537]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 536]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 535]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 534]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 533]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 532]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 531]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 530]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 529]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 528]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 527]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 526]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 525]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 524]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 523]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 522]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 521]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 520]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 519]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 518]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 517]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 516]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 515]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 514]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 513]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 512]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 511]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 510]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 509]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 508]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 507]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 506]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 505]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 504]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 503]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 502]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 501]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 500]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 499]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 498]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 497]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 496]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 495]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 494]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 493]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 492]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 491]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 490]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 489]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 488]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 487]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 486]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 485]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 484]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 483]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 482]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 481]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 480]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 479]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 478]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 477]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 476]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 475]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 474]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 473]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 472]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 471]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 470]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 469]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 468]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 467]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 466]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 465]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 464]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 463]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 462]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 461]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 460]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 459]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 458]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 457]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 456]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 455]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 454]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 453]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 452]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 451]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 450]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 449]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 448]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 447]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 446]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 445]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 444]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 443]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 442]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 441]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 440]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 439]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 438]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 437]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 436]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 435]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 434]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 433]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 432]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 431]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 430]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 429]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 428]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 427]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 426]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 425]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 424]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 423]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 422]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 421]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 420]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 419]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 418]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 417]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 416]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 415]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 414]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 413]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 412]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 411]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 410]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 409]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 408]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 407]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 406]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 405]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 404]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 403]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 402]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 401]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 400]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 399]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 398]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 397]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 396]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 395]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 394]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 393]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 392]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 391]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 390]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 389]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 388]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 387]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 386]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 385]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 384]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 383]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 382]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 381]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 380]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 379]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 378]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 377]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 376]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 375]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 374]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 373]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 372]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 371]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 370]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 369]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 368]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 367]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 366]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 365]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 364]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 363]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 362]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 361]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 360]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 359]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 358]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 357]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 356]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 355]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 354]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 353]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 352]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 351]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 350]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 349]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 348]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 347]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 346]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 345]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 344]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 343]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 342]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 341]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 340]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 339]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 338]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 337]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 336]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 335]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 334]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 333]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 332]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 331]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 330]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 329]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 328]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 327]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 326]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 325]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 324]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 323]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 322]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 321]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 320]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 319]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 318]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 317]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 316]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 315]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 314]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 313]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 312]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 311]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 310]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 309]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 308]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 307]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 306]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 305]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 304]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 303]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 302]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 301]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 300]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 299]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 298]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 297]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 296]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 295]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 294]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 293]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 292]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 291]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 290]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 289]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 288]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 287]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 286]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 285]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 284]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 283]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 282]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 281]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 280]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 279]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 278]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 277]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 276]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 275]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 274]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 273]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 272]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 271]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 270]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 269]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 268]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 267]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 266]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 265]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 264]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 263]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 262]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 261]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 260]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 259]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 258]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 257]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 256]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[ 255]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 254]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 253]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 252]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 251]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 250]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 249]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 248]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 247]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 246]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 245]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 244]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 243]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 242]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 241]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 240]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 239]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 238]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 237]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 236]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 235]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 234]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 233]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 232]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 231]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 230]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 229]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 228]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 227]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 226]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 225]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 224]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 223]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 222]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 221]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 220]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 219]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 218]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 217]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 216]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 215]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 214]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 213]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 212]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 211]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 210]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 209]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 208]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 207]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 206]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 205]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 204]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 203]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 202]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 201]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 200]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 199]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 198]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 197]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 196]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 195]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 194]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 193]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 192]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 191]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 190]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 189]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 188]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 187]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 186]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 185]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 184]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 183]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 182]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 181]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 180]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 179]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 178]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 177]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 176]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 175]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 174]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 173]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 172]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 171]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 170]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 169]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 168]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 167]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 166]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 165]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 164]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 163]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 162]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 161]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 160]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 159]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 158]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 157]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 156]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 155]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 154]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 153]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 152]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 151]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 150]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 149]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 147]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 146]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 145]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 144]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 143]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 142]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 141]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 140]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 139]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 138]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 137]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 136]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 135]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 134]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 133]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 132]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 131]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 130]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 129]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 128]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 127]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 126]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 125]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 124]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 123]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 122]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 121]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 120]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 119]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 118]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 117]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 116]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 115]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 114]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 113]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 111]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 110]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 109]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 108]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 107]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 106]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 104]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 103]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 102]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  98]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  97]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  96]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  94]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  93]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  91]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  89]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  87]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  86]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  84]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  82]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  73]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  72]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  67]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  66]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  63]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  62]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  61]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  59]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  58]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  53]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  52]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  48]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  45]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  39]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  38]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  36]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  35]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[  34]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  33]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  31]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  30]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  29]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  28]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  27]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  21]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  20]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  18]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  17]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  15]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  13]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  12]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  11]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  10]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[   9]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   8]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[   7]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   6]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[   5]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[   4]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[   3]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   2]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   1]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   0]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   93900   326742 |   31300       0        0     nan |  0.000 % |
c |       100 |   93882   326691 |   34430      96      386     4.0 |  7.915 % |
c |       251 |   93882   326691 |   37873     247     1242     5.0 |  7.915 % |
c |       476 |   93882   326691 |   41660     472     2276     4.8 |  7.915 % |
c |       813 |   93876   326674 |   45826     808     3811     4.7 |  7.920 % |
c |      1319 |   93876   326674 |   50408    1314     6266     4.8 |  7.920 % |
c |      2078 |   93876   326674 |   55449    2073     9771     4.7 |  7.920 % |
c |      3217 |   93876   326674 |   60994    3212    15317     4.8 |  7.920 % |
c |      4925 |   93870   326657 |   67094    4919    23706     4.8 |  7.924 % |
c |      7487 |   93870   326657 |   73803    7481    36536     4.9 |  7.924 % |
c |     11331 |   93864   326640 |   81184   11323    56223     5.0 |  7.929 % |
c ==============================================================================
c [1mFound solution: 893[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11306   maxlim: 7288   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14127 |  172932   609011 |   57644   14119    70937     5.0 |  7.929 % |
c |     14227 |  172932   609011 |   63408   14219    71380     5.0 |  5.227 % |
c |     14377 |  172932   609011 |   69749   14369    72105     5.0 |  5.227 % |
c |     14602 |  172932   609011 |   76724   14594    73203     5.0 |  5.227 % |
c |     14939 |  172932   609011 |   84396   14931    75067     5.0 |  5.227 % |
c |     15446 |  172932   609011 |   92836   15438    78344     5.1 |  5.227 % |
c |     16205 |  172932   609011 |  102119   16197    82693     5.1 |  5.227 % |
c |     17347 |  172932   609011 |  112331   17339    89418     5.2 |  5.227 % |
c |     19055 |  172932   609011 |  123565   19047   100304     5.3 |  5.227 % |
c |     21617 |  172932   609011 |  135921   21609   115114     5.3 |  5.227 % |
c |     25461 |  172923   608980 |  149513   25450   139735     5.5 |  5.230 % |
c |     31227 |  172923   608980 |  164465   31216   187769     6.0 |  5.230 % |
c |     39876 |  172923   608980 |  180911   39865   243764     6.1 |  5.230 % |
c |     52850 |  172914   608949 |  199002   52836   353991     6.7 |  5.233 % |
c ==============================================================================
c [1mFound solution: 752[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7429   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55122 |  172923   609005 |   57641   55108   372227     6.8 |  5.233 % |
c |     55222 |  172923   609005 |   63405   55208   372881     6.8 |  5.242 % |
c |     55372 |  172923   609005 |   69745   55358   373944     6.8 |  5.242 % |
c |     55598 |  172923   609005 |   76720   55584   380561     6.8 |  5.242 % |
c |     55935 |  172923   609005 |   84392   55921   384365     6.9 |  5.242 % |
c |     56442 |  172923   609005 |   92831   56428   389579     6.9 |  5.242 % |
c |     57201 |  172923   609005 |  102114   57187   402384     7.0 |  5.242 % |
c |     58340 |  172923   609005 |  112326   58326   412925     7.1 |  5.242 % |
c |     60048 |  172923   609005 |  123558   60034   430730     7.2 |  5.242 % |
c |     62610 |  172923   609005 |  135914   62596   452765     7.2 |  5.242 % |
c ==============================================================================
c [1mFound solution: 732[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7449   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65320 |  172926   609042 |   57642   65306   475540     7.3 |  5.242 % |
c |     65420 |  172926   609042 |   63406   17526   139909     8.0 |  5.250 % |
c |     65570 |  172926   609042 |   69746   17676   140725     8.0 |  5.250 % |
c |     65795 |  172926   609042 |   76721   17901   141998     7.9 |  5.250 % |
c |     66132 |  172926   609042 |   84393   18238   143918     7.9 |  5.250 % |
c |     66638 |  172926   609042 |   92833   18744   146679     7.8 |  5.250 % |
c |     67397 |  172926   609042 |  102116   19503   151142     7.7 |  5.250 % |
c |     68536 |  172926   609042 |  112327   20642   158126     7.7 |  5.250 % |
c |     70245 |  172926   609042 |  123560   22351   171158     7.7 |  5.250 % |
c |     72807 |  172926   609042 |  135916   24913   188823     7.6 |  5.250 % |
c |     76651 |  172926   609042 |  149508   28757   212619     7.4 |  5.250 % |
c |     82417 |  172926   609042 |  164459   34523   250408     7.3 |  5.250 % |
c |     91066 |  172920   609025 |  180905   43170   313636     7.3 |  5.253 % |
c |    104040 |  172920   609025 |  198995   56144   412601     7.3 |  5.253 % |
c |    123501 |  172920   609025 |  218895   75605   618016     8.2 |  5.253 % |
c |    152693 |  172920   609025 |  240784  104797  1946487    18.6 |  5.253 % |
c |    196484 |  172920   609025 |  264863  148588  7646271    51.5 |  5.253 % |
c ==============================================================================
c [1mFound solution: 690[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7491   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    237345 |  172923   609049 |   57641  189449  9602699    50.7 |  5.253 % |
c |    237445 |  172923   609049 |   63405   25041   248664     9.9 |  5.259 % |
c |    237595 |  172923   609049 |   69745   25191   249512     9.9 |  5.259 % |
c |    237822 |  172923   609049 |   76720   25418   250763     9.9 |  5.259 % |
c |    238159 |  172923   609049 |   84392   25755   252923     9.8 |  5.259 % |
c |    238666 |  172923   609049 |   92831   26262   256126     9.8 |  5.259 % |
c |    239426 |  172923   609049 |  102114   27022   260456     9.6 |  5.259 % |
c |    240565 |  172923   609049 |  112326   28161   267609     9.5 |  5.259 % |
c |    242273 |  172923   609049 |  123558   29869   277575     9.3 |  5.259 % |
c |    244835 |  172923   609049 |  135914   32431   303311     9.4 |  5.259 % |
c |    248679 |  172923   609049 |  149505   36275   326571     9.0 |  5.259 % |
c |    254446 |  172923   609049 |  164456   42042   371281     8.8 |  5.259 % |
c |    263096 |  172923   609049 |  180902   50692   703724    13.9 |  5.259 % |
c |    276070 |  172923   609049 |  198992   63666   810696    12.7 |  5.259 % |
c |    295531 |  172923   609049 |  218891   83127  1029081    12.4 |  5.259 % |
c |    324724 |  172923   609049 |  240780  112320  3889344    34.6 |  5.259 % |
c |    368513 |  172914   609018 |  264858  156106  8165056    52.3 |  5.262 % |
c |    434199 |  172914   609018 |  291344  221792  9892754    44.6 |  5.262 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v4221 -v3659 -v4226 -v3780 -v3680 v3132 -v2610 v4225 -v3895 -v3779 -v3679 -v2609 v334 -v4026 -v3781 -v3133 v2615 v1996 v335 -v4228 -v4025 v3894 -v3782 -v3681 -v3135 v2614 -v1405 -v1103 -v559 -v338 -v4229 v4031 -v3898 v3783 -v3683 -v3136 v2616 -v1997 -v1108 -v336 -v4232 v4030 v3790 -v2620 -v1999 -v1408 v1107 -v558 -v416 -v337 -v4230 v4032 -v3899 v3784 -v3684 -v2619 -v2000 -v1409 -v1083 -v562 -v4476 -v4285 -v4231 v4036 v3785 -v3724 -v3686 -v2617 -v1359 -v1225 v1110 -v1082 v4035 v3786 -v3723 -v3687 -v2618 v1230 -v1111 -v1088 -v563 -v4479 -v4284 -v4033 -v3725 -v3310 v1229 v1114 v1087 -v4480 -v4034 v3728 -v1112 v1089 -v654 v4290 v3727 -v3309 -v2165 v1232 -v1113 v1093 -v989 -v653 -v4335 v4288 v3732 -v1233 v1092 -v655 v4334 v3731 -v3315 -v2164 -v1236 -v1090 -v992 -v656 -v387 -v4289 v3729 -v3313 -v1234 -v1091 -v993 v657 -v391 -v4359 v4336 -v4293 -v3730 v2170 -v1235 -v853 v664 v4338 -v3314 -v2168 v858 v658 v4362 -v3318 v857 v659 v4363 v4339 -v2169 v660 -v4341 v3572 -v2173 v860 -v52 -v4342 v3571 -v1979 v861 v56 -v3708 v3573 -v1978 -v1336 -v864 v316 v4621 v1983 -v862 v3634 v1982 -v1335 -v863 -v319 -v3638 v4622 -v320 v3655 -v3148 -v3130 -v1993 -v3658 -v1992 -v4220 -v3675 v3134 -v4222 -v3674 -v3138 -v1938 v4227 -v3137 -v2611 v1998 -v339 v4224 v3896 -v3793 v3682 -v2612 -v2002 -v1404 -v638 -v412 v4233 -v4027 -v3900 v3794 -v3685 v2613 -v2001 -v1102 -v4028 v3789 v3689 v2624 -v2451 -v1410 -v1355 -v1104 -v560 -v415 v4029 v3688 v2455 v1109 -v564 -v4475 -v4280 -v4040 -v3902 -v3787 v1358 v1106 -v3903 -v1224 v1115 -v1084 -v4481 -v4286 -v3305 -v1413 -v1226 -v1085 -v833 -v566 -v3726 v1231 v1086 v837 -v567 v4291 -v3740 -v3311 -v2160 v1228 v1097 -v988 -v4330 v3736 -v1237 -v4484 -v4329 -v4294 v3735 v3316 v2166 v994 -v667 -v386 -v4292 -v668 -v390 -v4358 v4337 v3319 v2171 v663 v4340 -v3317 -v852 v4364 -v4344 -v2174 -v997 v854 v661 -v4343 -v2172 v859 -v3704 v856 v51 -v865 v55 -v4367 -v3707 v315 -v224 v3574 -v1980 -v228 v3633 v3582 -v1981 -v1337 v321 -v3637 v3578 v3577 v1987 v1459 v3654 -v3147 -v3129 v3660 -v3131 -v1934 -v3890 v1994 v4268 -v3889 -v3792 -v3142 v1995 -v1937 -v1400 -v634 v347 -v4223 -v3791 v3676 -v554 -v343 -v4241 v3897 v3677 -v3663 v3456 -v2627 -v2006 v1406 -v637 -v553 -v411 -v342 v4237 -v3901 v3678 -v2628 -v4471 -v4236 -v4043 v3905 v3693 -v3285 -v2623 -v2450 -v1411 v1354 -v561 -v417 -v4044 -v3904 -v3289 v2454 -v1105 -v565 -v4477 -v4039 -v3788 -v2621 -v1414 v1360 -v1123 v569 -v4279 -v1412 v1119 -v568 -v4482 v4281 -v4037 -v3737 v1118 v1100 -v984 -v832 v420 -v4287 -v3739 v3304 v1227 v1101 v836 -v4485 v4283 v3306 -v1363 v1245 v1096 -v990 -v666 -v512 -v4483 -v4295 -v3312 -v2159 v1241 -v665 -v516 -v4354 -v3733 v3308 v2161 v1240 -v1094 v995 -v491 -v388 -v4331 v3320 v2167 -v392 -v4360 -v4332 -v3734 v2163 -v998 v4333 v2175 -v996 v4365 v4348 v662 -v394 v855 -v395 v4368 -v3703 -v873 -v311 v53 -v4366 -v1332 -v869 v57 -v3709 -v3579 v1719 -v1331 -v868 v317 -v223 v3581 -v1723 -v227 v3635 -v1990 -v1455 -v1338 v322 -v59 -v3639 -v1991 -v60 -v3712 -v3575 v1986 v1458 v1339 -v541 -v323 v1340 -v324 v3656 v3149 -v2279 v4269 v3661 -v3145 -v1933 v344 v4267 -v3146 v346 -v4238 v3664 -v3452 -v3153 -v3141 -v2626 -v2194 -v2009 -v1939 -v633 -v407 -v4240 v3891 -v3662 -v2625 v2010 -v1399 -v4042 v3892 -v3696 v3455 -v3213 -v3139 -v2005 v1401 -v1350 -v639 v413 -v340 -v4041 v3893 -v3697 -v3217 v1407 -v555 -v4234 -v3909 -v3692 -v3284 -v2452 -v2003 -v1942 v1403 v1356 -v1120 -v556 -v418 -v341 -v4470 -v3288 v2456 -v1415 -v1122 v557 -v4472 -v4235 -v3690 -v2622 v1361 -v1099 -v642 -v573 v421 -v4478 -v3738 -v1098 v419 v4474 -v4038 -v2458 -v1364 v1242 v1116 v834 -v462 v4486 v4282 -v2459 -v1362 v1244 -v983 v838 -v466 v382 v4303 v1117 v985 -v511 -v487 v381 v4299 v3307 -v991 -v515 v4298 v3328 v1238 -v1095 v987 -v840 -v490 -v389 -v4353 v3324 v2162 -v999 -v841 -v393 v4355 -v4351 v3323 -v2183 -v1239 v397 -v4361 -v4352 v2179 v396 -v47 v4357 v4347 v3699 v2178 -v870 -v46 v4369 -v872 -v4345 -v3705 v54 v3629 -v3580 -v310 v58 -v3710 v3628 -v2263 -v1989 v1718 -v866 -v312 -v225 v62 -v1988 -v1722 v1333 v318 -v229 v61 -v3801 -v3713 v3636 -v1454 v1334 -v867 -v537 v314 -v3805 -v3711 v3640 v325 v3641 -v3576 v1984 v1460 v1344 -v540 v231 -v3642 v232 v3652 v3150 -v3144 v2278 -v1929 v4270 v3657 -v3143 -v345 v3653 -v3154 -v2190 -v2008 v1935 -v629 -v4239 v3665 -v3152 -v2007 -v3695 -v3451 -v2193 -v2046 -v1940 v635 -v3694 v2446 -v406 v3912 v3457 v3212 -v3140 -v2789 v2445 -v1943 -v640 -v408 v3913 -v3216 -v1941 v1402 -v1349 -v1121 v414 -v3908 -v3286 -v2453 -v2004 -v1423 -v1351 v643 -v576 v410 -v3290 v2457 v1419 v1357 -v828 -v641 v577 v422 -v3906 -v3691 -v3460 -v2461 -v1811 v1418 v1353 -v827 -v572 -v203 -v4473 -v2460 -v1815 -v1365 -v1243 -v4494 -v4300 -v3292 v835 -v570 -v461 v4490 -v4302 -v3293 v839 -v465 v4489 -v3325 -v2928 -v843 -v513 -v486 -v156 -v3327 v2932 v986 -v842 -v517 v383 -v4350 -v4296 -v2180 v1007 -v492 v384 -v4349 -v2182 v1003 v385 -v4297 -v3321 v1002 -v519 v401 v4356 -v871 -v520 v4377 -v3322 -v2176 v495 v4373 v3698 -v219 -v48 v4372 -v4346 v3700 -v2259 -v2177 -v218 -v49 -v3706 v50 v3702 -v2262 v1720 v1450 v226 -v66 v3714 v3630 -v1724 -v313 -v230 -v4579 -v3800 v3631 v1456 -v1347 -v536 v333 v234 -v3804 v3632 -v1348 -v329 v233 v3646 v1985 -v1726 v1461 v1343 -v542 -v328 -v1727 -v4278 v3151 v2280 -v808 -v294 v4274 v3651 -v3155 -v1928 -v812 -v4273 v3673 -v3613 -v3447 -v2189 -v2042 v1930 v3669 v1936 -v628 -v3911 v3668 -v3453 -v2839 -v2785 -v2284 v2195 -v2045 v1932 v630 -v3910 -v3280 -v1944 v636 v3458 -v3279 v3214 -v2788 -v1420 v632 -v575 -v3218 v2447 -v1422 v644 -v574 -v409 v3461 -v3287 v2448 -v2301 v2198 -v430 -v199 -v3459 -v3291 v2449 v2305 -v1352 -v426 -v4491 -v3907 -v3295 -v3220 v2465 -v1810 -v1416 v1373 -v425 -v202 -v4493 -v4301 -v3294 -v3221 -v1814 -v1369 -v829 v507 -v1417 -v1368 v830 -v571 v506 -v482 -v463 -v152 -v3326 v831 -v467 v4487 -v2927 -v1836 v1004 -v847 -v514 -v488 -v155 v2931 -v2181 -v1840 v1006 -v518 v4488 -v522 -v493 -v469 v404 -v521 -v470 v405 -v4374 v1000 v496 v400 -v4376 v494 v1001 v398 v1714 v4370 -v2258 v1713 -v69 v3701 -v220 -v70 -v4575 v4371 -v3722 -v2264 v1721 -v1346 v532 v330 -v221 -v65 v3718 -v1725 v1449 -v1345 v332 v222 -v4578 -v3802 v3717 v3649 v1729 v1451 -v538 -v238 -v63 -v3806 v3650 v1728 v1457 v3645 -v2267 v1453 v1341 -v543 -v326 -v1462 -v4277 v3670 -v3609 -v3163 v2281 -v2185 v807 -v293 v3672 v3159 -v811 -v4271 -v3612 v3158 -v2835 -v2285 v2191 -v2041 -v3446 -v3208 -v2283 v1931 -v4272 -v3666 -v3448 -v3207 -v2838 -v2784 v2196 -v2047 v1952 -v1573 -v3454 v1948 -v1421 v631 -v3667 v3450 v3215 -v2790 v2199 v1947 -v652 -v427 v3462 -v3281 -v3219 v2197 -v648 -v429 -v3282 -v3223 -v2468 -v2300 -v2050 v1370 -v647 -v198 -v4492 -v3283 -v3222 -v2469 v2304 v1372 v457 -v3299 v2793 v2464 -v1812 v1619 v456 -v423 -v204 -v1816 -v1623 -v4010 -v3357 v2462 -v1366 -v850 -v464 -v424 -v151 -v3361 -v1005 -v851 v508 -v481 -v468 -v2929 -v1835 -v1818 -v1367 -v846 v509 -v483 -v472 v403 -v207 -v157 v2933 -v1839 -v1819 v510 -v489 -v471 v402 -v844 v526 v485 -v4375 v497 -v2935 -v160 -v2936 -v2254 v399 -v68 -v67 -v3719 -v2260 v1786 -v3796 -v3721 -v1790 v1715 -v331 -v4574 -v3795 -v3648 -v2265 v1716 v241 -v3647 v1717 v531 v242 -v4580 -v3803 -v3715 -v2268 -v1911 -v1733 v533 -v237 -v64 -v3807 -v2266 -v1915 v1452 -v539 v3808 -v3716 -v3643 v1470 -v1342 v535 -v327 -v235 -v3809 v1466 v544 -v4275 v3671 -v3608 -v3162 v2282 -v2037 v809 -v295 v2286 -v2184 -v813 -v3614 -v3156 -v2834 -v2780 -v2186 v2043 v1949 -v1569 v2192 v1951 -v3157 -v2840 -v2786 v2188 -v2095 v2048 -v1572 -v815 -v649 -v299 -v3449 -v3209 v2200 -v816 -v651 -v428 v3617 -v3470 v3210 -v2791 -v2467 -v2051 -v1945 -v194 -v3466 v3211 -v2466 -v2049 -v1806 v1371 -v3465 -v3302 v3227 -v2843 v2794 -v2302 -v1946 -v1805 -v645 -v200 -v3303 v2792 v2306 -v4006 -v3298 v1813 v1618 -v1434 -v849 -v646 v205 -v147 -v2923 -v1817 -v1622 -v848 v458 -v4009 -v3356 -v3296 -v2922 -v2463 -v2308 -v1821 v459 v208 -v153 -v3360 -v2309 -v1820 v460 -v206 -v2978 v2930 v1837 -v529 -v476 v158 v2982 v2934 v1841 -v530 -v484 v2938 -v845 -v720 v525 v505 v161 -v2937 -v724 -v501 -v159 v1843 v523 -v500 v1844 v2502 -v3720 -v2253 -v4570 v2764 -v2255 v1785 v240 -v2261 v1789 v239 -v4576 -v2257 -v1736 -v3797 -v2269 -v1737 -v4581 -v3798 -v1910 -v1732 -v1467 v3799 v1914 -v1469 v534 -v4582 v3813 -v3644 v3118 -v1730 -v552 -v236 -v34 -v4583 v3122 v1465 v548 -v4276 -v3610 -v3160 -v2830 -v2294 v810 v740 v296 v2290 -v2036 -v1950 v814 -v3615 v2836 -v2289 -v2091 -v2038 -v1568 -v818 v300 -v2779 -v2187 v2044 -v817 -v650 -v298 v3618 -v3467 -v2841 v2781 -v2326 -v2208 -v2094 v2040 -v1574 v3616 -v3469 v2787 -v2330 -v2296 v2204 v2052 -v3301 -v3230 v2844 v2783 -v2295 v2203 -v3300 -v3231 v2842 v2795 -v193 -v3463 -v3226 -v2430 -v2303 -v1577 -v1430 -v195 v2307 -v1807 -v201 -v4005 -v3464 -v3224 v2311 -v1808 v1620 -v1433 v197 v2310 -v1831 v1809 -v1624 v209 -v146 -v4011 v3358 -v3297 -v1959 -v1830 v1825 -v790 -v528 -v479 -v148 v3362 v2924 -v1963 -v527 -v480 v154 -v3751 v2977 v2925 v1838 -v1626 v502 -v475 v150 v2981 v2926 v1842 -v1627 v504 v162 -v4014 -v3386 v3364 -v2942 -v2116 v1846 -v719 -v473 v3365 -v2120 v1845 -v723 v2498 v524 -v498 v2760 v2501 -v499 v2763 v1787 -v1735 -v4569 -v2256 v1791 -v1734 -v4571 -v2277 v4577 -v2273 -v1468 v4573 v3816 -v2272 v1912 -v1793 -v549 -v30 -v4584 v3817 v1916 -v1794 -v551 v3812 v3117 -v1731 -v33 v3121 -v1463 -v547 v3606 -v3161 -v2293 -v1564 v806 v739 v297 -v3611 -v2829 v805 v301 v3607 -v2831 -v2287 -v2205 -v2090 v1570 -v822 v3619 -v3468 v2837 -v2207 -v2039 -v3229 v2833 -v2325 -v2288 -v2096 v2060 -v1575 -v3228 v2845 v2782 -v2329 v2056 v2803 v2426 v2201 v2055 -v1578 -v1180 -v81 -v2799 -v2297 -v1614 -v1576 -v1184 -v4001 -v3920 -v2798 -v2429 v2298 v2202 v2099 -v1673 -v1613 -v1429 -v3924 -v3352 v2299 v196 -v4007 -v3351 -v3225 -v2315 -v1828 v1621 -v1435 -v786 -v478 v217 v1829 -v1625 -v477 -v213 v4012 -v3747 v3359 -v1958 -v1824 -v1629 -v789 -v212 v3363 -v1962 -v1832 -v1628 -v503 -v149 -v4015 -v3750 -v3382 v3367 v2979 -v2945 -v1833 -v1822 -v1594 -v1438 v170 -v4013 v3366 v2983 -v2946 v1834 -v1598 -v166 -v3385 -v2941 -v2115 v1850 -v721 -v474 -v165 -v2119 v725 -v2985 -v2939 v2497 -v253 -v2986 -v1781 v2759 v2503 -v1780 v727 v728 v2765 -v2274 v1788 -v2276 v1906 v1792 v3815 -v2506 v1905 v1796 v4572 v3814 -v1795 -v550 v4592 v2768 -v2270 v1913 v29 -v7 v4588 v1917 -v11 v4587 v3810 v3119 -v2271 v1918 -v35 v3123 v1919 -v1464 -v545 -v2291 -v2086 -v1315 -v825 v741 v309 v3605 -v2206 v1563 v826 v305 v3627 -v2590 -v2092 -v2057 v1565 -v821 v304 -v3623 -v2832 -v2594 v2059 v1571 -v3622 -v2853 -v2800 v2327 v2097 -v2021 v1567 -v819 -v745 -v77 -v2849 v2802 -v2331 -v1579 -v4426 -v2848 v2425 v2100 -v2053 -v1669 -v1425 -v1179 v80 -v4430 v2098 -v1183 -v3919 -v2953 -v2796 v2431 -v2333 -v2318 -v2054 -v1827 -v1672 v1431 v214 -v4000 -v3923 -v2957 -v2334 v2319 -v1826 -v1615 v216 -v4130 v4002 -v2797 -v2314 -v1616 v1436 -v785 v4008 v3353 -v2973 v1617 v4004 -v3746 v3354 -v2972 -v2944 -v2635 -v2434 -v2312 -v1960 v1633 v1439 -v791 -v210 -v167 -v4016 v3355 -v2943 -v2639 v1964 -v1437 -v715 v169 -v3752 -v3381 v3371 v2980 -v1865 v1853 -v1823 -v1593 -v714 -v211 v2984 v1854 -v1597 v3387 -v2988 -v2493 -v2117 -v1966 -v1849 -v794 v722 -v249 -v163 -v2987 v2121 -v1967 v726 -v3755 -v2940 -v2755 v2499 -v1847 v730 -v252 -v164 v729 -v4155 v3390 v2761 v2504 -v2123 -v2275 -v2124 -v1782 v2766 v2507 v1783 -v2505 v1784 -v4589 -v4505 v2769 v1800 -v25 -v4591 -v3113 v2767 v1907 -v3112 v1908 v31 -v6 v1909 -v10 v4585 v3811 v3120 v1923 v370 -v36 v3124 -v546 v374 v3624 -v2292 -v1314 -v823 v742 v308 v3626 v2321 -v2085 -v2058 -v3019 -v2850 -v2589 v2320 -v2087 v2017 v746 -v302 -v3023 -v2852 -v2801 -v2593 -v2093 v1566 -v744 -v3620 -v2421 v2328 v2089 v2020 -v1587 -v820 -v303 -v76 -v2332 v2101 v1583 -v4425 -v3621 -v2846 v2427 -v2336 -v2317 -v1668 v1582 -v1181 v82 -v4429 -v2335 -v2316 -v1424 -v1185 v215 v4126 -v3921 -v2952 -v2847 v2432 -v1674 -v1426 -v781 -v3925 -v2956 -v1954 v1432 -v4129 -v3742 -v2435 -v1953 -v1636 v1428 -v1187 -v787 -v85 v4003 -v2433 -v1637 v1440 -v1188 -v168 v4024 -v3927 -v3748 -v3377 -v3374 -v2634 -v2313 v1961 -v1861 -v1852 -v1677 -v1632 -v792 v4020 -v3928 v3375 -v2974 -v2638 -v2111 v1965 -v1851 -v4019 -v3753 -v3383 v3370 -v2975 -v2110 v1969 v1864 -v1630 -v1595 -v795 v2976 -v1968 -v1599 -v793 -v716 -v3756 v3388 -v3368 v2992 v2118 v717 v613 -v248 -v3754 -v2492 v2122 v718 -v4151 v3391 -v2494 v2126 -v1848 v1601 v734 -v254 v3389 -v2754 v2500 -v2125 v1602 -v4154 v2756 v2664 v2496 v2762 v2508 -v4501 -v3044 v2758 v1803 -v1018 -v257 -v4590 -v3048 v2770 v1804 -v4504 v1799 -v24 -v1926 -v1797 v26 -v8 v3114 -v1927 v32 -v12 -v4586 v3115 v1922 v369 v28 v3116 v373 v37 v3625 -v1316 -v824 v743 v306 -v2851 v747 -v3018 -v2591 v2016 -v1584 -v72 -v3022 v2595 v2322 -v2088 -v1586 -v1175 v2323 v2109 v2022 -v1664 -v1320 -v1174 -v78 -v3915 -v2420 v2324 -v2105 -v4427 -v3981 -v3914 -v2597 -v2422 -v2340 -v2104 -v1670 v1580 -v1182 v83 -v4431 -v3985 -v2598 v2428 -v1186 v4125 v3922 -v2954 v2424 -v2025 -v1675 -v1635 v1581 v1519 -v1190 -v86 -v3926 v2958 -v2436 -v1634 -v1523 v1427 -v1189 -v780 -v84 -v4433 -v4131 -v4021 v3930 -v3373 -v1678 -v1448 -v782 -v4434 v4023 v3929 -v3741 -v3372 v1955 -v1676 -v1589 -v1444 -v788 -v3743 -v2960 -v2636 v1956 -v1860 -v1694 -v1588 -v1443 v784 v3749 -v3376 -v2961 -v2640 v1957 -v1698 v796 v4134 -v4017 v3745 v3378 v2995 -v1973 v1866 -v1631 -v1596 -v609 -v244 -v3757 -v3384 v2996 v2112 -v1600 -v4248 -v4018 v3380 -v3369 v2991 v2642 v2113 v1604 -v737 v612 -v250 -v4252 v3392 -v2643 v2114 v1603 -v738 -v4150 v2989 -v2660 -v2130 -v1869 v733 -v255 -v2495 -v4156 v2663 -v2516 -v1802 -v1014 -v731 -v258 v2757 -v2512 -v1801 -v256 -v4530 -v4500 v4451 -v3043 v2778 -v2511 -v1017 -v4455 -v3047 v2774 -v2 v4506 -v4159 -v2773 -v1925 v1380 v934 -v1 -v1924 v1384 -v1798 -v9 v27 -v13 -v4509 v3127 v2480 v1920 v371 v45 -v14 v3128 v375 -v41 -v15 -v3821 -v2586 -v2012 v1317 v755 v307 -v3825 -v1585 -v751 -v3020 -v2592 -v2106 v2018 v1321 -v750 -v4421 -v3024 v2596 v2108 -v1319 -v71 -v4420 v2600 -v2343 v2023 -v73 -v2948 -v2599 -v2344 -v1663 v1176 -v79 v4428 -v4121 -v3980 -v3556 -v3026 -v2947 -v2339 -v2102 -v2026 -v1665 v1177 v75 -v4432 -v3984 -v3916 -v3027 -v2423 -v2024 -v1671 v1178 v87 -v4436 v4127 -v3917 -v2955 -v2444 -v2337 -v2103 -v1667 v1518 -v1445 -v1205 v1194 -v4435 -v4022 v3918 v2959 -v2630 -v2440 -v1679 -v1522 -v1447 -v1209 v4132 v3934 v2963 -v2629 -v2439 -v1856 -v1063 v2962 -v1067 -v783 v4135 -v2994 v2637 v1976 -v1862 -v1693 -v1441 v804 v4133 -v3744 v2993 -v2641 v1977 -v1697 v1590 v800 -v3765 v2645 -v1972 v1867 v1591 -v1442 v799 -v736 -v608 v3761 v3379 v2644 v1592 -v735 -v243 -v4247 -v4146 v3760 -v3400 -v2133 -v1970 v1870 -v1608 v614 -v245 -v4251 -v3396 -v2134 -v1868 -v251 -v4152 -v3395 v2990 -v2659 -v2513 -v2129 -v247 -v2515 -v259 -v4526 -v4496 -v4157 -v2775 v2665 -v2127 -v1013 -v732 -v617 v2777 -v4529 -v4502 v4450 -v4160 -v3242 -v3045 v2566 -v2509 -v1019 -v930 -v4454 -v4158 v3049 -v2570 v4507 -v3097 -v2771 -v2668 -v2510 v1379 v933 v1383 -v365 -v3 v4510 -v3126 -v3051 -v2772 -v2476 v1022 -v364 -v42 -v4 -v4508 -v3125 -v3052 v44 -v5 v2479 -v1921 v372 v181 -v19 v376 -v40 v3820 -v3015 v1318 v754 -v3824 v2585 -v2107 -v2011 v1322 v3021 v2587 -v2342 -v2013 -v761 -v748 -v3025 v2588 -v2341 v2019 v765 -v3552 v3029 v2604 v2015 -v749 -v4422 -v3028 -v2027 -v74 -v4423 v3982 -v3555 -v2882 -v2441 v1197 -v95 v4424 -v4120 -v3986 -v2949 -v2443 -v1666 -v1446 v1198 v91 v4440 -v4122 v3937 -v2950 -v2338 -v1687 v1520 -v1204 v1193 -v441 v90 v4128 v3938 v2951 -v1683 -v1524 -v1208 v4124 -v3988 v3933 v2967 -v2437 -v1975 -v1682 -v1191 -v1062 -v801 v4136 -v3989 v2631 -v1974 -v1855 -v1066 -v803 v3931 -v3762 v2632 -v2438 -v1857 -v1695 -v1526 -v604 -v3764 v2633 -v1863 -v1699 -v1527 -v3397 v2649 -v2132 v1859 -v1611 v797 -v610 -v3399 -v2131 v1871 v1612 -v4249 -v3758 -v2655 -v1971 v1701 -v1607 v798 v615 v4253 -v4145 -v2514 v1702 -v246 -v4147 -v3759 -v3393 v2661 -v1605 -v1009 v618 -v267 -v4153 -v3039 -v2776 -v616 -v263 -v4525 -v4255 -v4149 -v3394 -v3238 -v3038 v2666 -v2128 -v1015 -v262 -v4495 -v4256 -v4161 -v4531 -v4497 v4452 -v3241 -v3093 -v3046 -v2669 v2565 -v1020 -v929 v4503 -v4456 v3050 -v2667 -v2569 v4499 -v3096 -v3054 -v1481 v1381 v1023 v935 v4511 -v3053 v1385 v1021 -v43 -v4534 -v4458 -v2475 -v177 -v22 -v4459 v366 -v23 v2481 v1387 -v938 v367 v180 -v18 -v1388 v368 -v38 v3822 v1330 v752 v3826 -v3014 v1326 -v3016 v2607 v1325 -v760 v3976 v3017 v2608 -v2014 v764 v3975 -v3828 -v3551 v3033 -v2878 -v2603 -v2035 -v1196 -v92 -v3829 -v2442 v2031 -v1514 -v1195 -v94 -v4443 v3983 -v3936 -v3557 -v2881 -v2601 v2030 -v1684 -v1513 -v437 v4444 -v3987 -v3935 -v1686 -v4439 v3991 -v2970 v1521 v1206 -v440 -v88 -v4123 v3990 -v2971 v1689 -v1525 -v1210 -v802 -v4437 -v4144 -v3560 v2966 v1688 -v1680 -v1529 -v1192 -v1064 -v89 -v4140 -v3763 -v1528 -v1068 -v4139 v3932 v2964 -v2652 -v1696 -v1681 -v1610 v1212 -v4243 -v3398 -v2653 -v1858 -v1700 -v1609 -v1213 v603 -v4242 v2648 -v1879 v1704 v1070 v605 -v1875 v1703 -v1071 v611 -v4250 v2646 -v1874 v607 -v264 v4254 -v2654 v619 -v266 v4521 v4258 -v4101 -v2656 -v1606 -v4446 v4257 -v4148 -v4105 v2662 -v1008 v4527 -v4445 -v4169 -v3237 v2658 -v1010 -v925 -v260 -v4165 -v3040 -v2670 -v1375 v1016 -v4532 v4453 -v4164 -v3407 -v3243 -v3092 -v3041 v2567 -v1477 -v1374 v1012 -v931 -v261 v4498 -v4457 -v3411 v3042 -v2571 v1024 -v4535 -v4519 -v4461 -v4310 -v3481 -v3098 -v3058 -v2471 -v1480 v1382 v936 -v21 -v4533 v4515 -v4460 -v4314 v1386 -v20 -v4514 -v3246 -v2573 -v2477 v1390 -v939 v176 -v2574 v1389 -v937 -v3101 v2482 v379 v182 -v16 v380 -v39 v3823 v2606 v1329 -v753 v3827 v2605 v3831 -v3547 -v3172 v3036 -v2032 -v1323 -v762 v3830 v3037 -v2034 v766 -v93 -v4442 -v3553 v3032 -v2877 -v1324 -v4441 v3977 -v1685 v1200 v3978 -v3558 -v3030 -v2969 -v2883 -v2602 v2028 -v1765 -v1544 v1199 -v768 -v436 v3979 -v2968 -v1548 -v1515 -v1058 -v769 -v4141 v3995 v3561 -v2029 -v1516 v1207 -v1057 -v442 -v4143 -v3559 v1517 -v1211 -v4438 -v2886 -v2651 v1533 v1215 -v1065 -v2650 v1690 v1214 -v1069 -v4137 -v2965 -v1876 v1691 v1073 -v445 -v1878 v1692 v1072 -v4138 v1708 -v675 -v4244 -v679 v606 -v265 -v4245 -v4051 v2647 -v1872 v627 v4246 -v4055 v623 v4262 -v4166 -v4100 -v3233 -v2215 -v1873 v622 v4520 -v4168 v4104 -v2657 -v2561 -v2219 v4522 v3239 -v3088 v2678 -v2560 v4528 -v4447 v2674 -v1011 -v924 v4524 -v4516 v4448 -v4162 -v3477 -v3406 -v3244 -v3094 v3061 v2673 v2568 -v1476 -v1032 -v926 v4536 -v4518 v4449 -v3410 v3062 -v2572 -v1376 -v1028 -v932 v4465 -v4309 -v4163 -v3480 -v3247 v3099 -v3057 v2576 -v1482 -v1377 -v1027 v928 -v172 -v4313 -v3245 -v2575 -v2470 v1378 -v940 -v4512 -v3875 -v3102 -v3055 v2472 v1394 -v378 v178 -v3100 v2478 -v377 -v4513 -v3339 -v3003 v2474 -v1485 v183 -v17 -v3007 v2483 v3819 -v3168 v3035 v1327 v757 v3818 v3034 -v2033 -v3835 -v3171 v2873 -v763 -v3546 v767 v3548 -v2879 -v1761 v771 -v432 -v3554 v770 v3998 v3550 -v3031 -v2884 -v1764 -v1543 -v438 -v4142 v3999 v3562 -v1547 v1201 v3994 -v2887 v1536 v1202 -v909 -v443 -v2885 v1537 v1203 -v1059 -v3992 v1532 v1219 -v1060 -v446 -v1877 v1061 -v444 v1711 v1530 v1077 v1712 v1707 -v674 -v624 -v678 v626 v4265 -v4050 v1705 v4266 -v4167 -v4054 v4261 v4102 -v2675 -v2214 -v620 v4106 -v3232 v2677 -v2218 -v4259 v3234 -v3060 -v1472 -v1029 -v621 v4523 -v4517 v3240 v3087 v3059 -v2562 -v1031 v4544 -v4468 -v4201 -v4108 -v3476 -v3408 v3236 v3089 -v2671 v2563 v1478 -v4540 -v4469 -v4205 -v4109 -v3412 -v3248 -v3095 v2564 -v927 -v4539 -v4464 -v4311 -v3871 -v3482 v3091 -v2672 v2580 -v1483 -v1397 -v1025 v948 -v4315 v3103 v1398 v944 -v171 -v4462 -v3874 v3414 -v3335 -v3056 -v2071 -v1486 v1393 -v1026 v943 -v173 -v3415 v2473 -v1484 v179 v4317 v3485 -v3338 -v3002 -v2491 v1391 v175 v4318 -v3006 v2487 v184 v3838 -v3260 -v3167 -v1739 v1328 v3839 -v3264 v756 -v3834 -v3173 v758 v2872 v759 -v3997 -v3832 v2874 -v1760 v775 -v3996 v3549 -v2880 -v431 -v3570 -v3176 v2876 -v1766 -v1545 -v1535 v905 -v433 v3566 -v2888 -v1549 -v1534 -v439 v3565 v1222 -v908 v435 v1223 -v447 -v3993 v2351 v1769 v1710 -v1551 v1218 -v1080 -v2355 v1709 -v1552 -v1081 v1531 v1216 v1076 -v625 v4264 v1074 -v676 v4263 v4096 -v680 v4095 -v4052 v1706 -v4056 -v2676 v4103 -v2216 v682 v4107 -v3402 -v2220 -v1030 v683 v4541 -v4467 -v4260 -v4111 -v4058 v3472 -v3401 v4543 -v4466 -v4305 -v4110 -v4059 v3235 -v1471 -v4304 -v4200 -v3478 -v3409 v3256 v2583 -v2222 v1473 -v1396 -v945 -v4204 -v3413 v3252 v3090 v2584 -v2223 v1479 -v1395 v947 -v4537 -v4312 -v3870 -v3483 v3417 v3251 v3111 v2579 -v2067 v1475 v4316 v3416 v3107 -v1487 -v4538 -v4463 v4320 -v3876 v3486 -v3334 v3106 v2577 -v2488 -v2070 v941 v4319 v3484 -v2490 -v174 -v3340 -v3004 v1392 v942 v192 -v3008 -v2486 v188 v3836 -v3259 v3169 -v1738 -v3263 -v3174 v1756 v778 -v1539 v779 -v3833 -v3567 -v3177 -v1762 -v1538 v774 -v3569 -v3175 v2875 -v2907 v2896 -v1767 -v1546 v1221 v904 v772 -v2892 -v1550 v1220 -v434 -v3563 -v2891 v1770 -v1554 -v1079 -v910 -v455 v1768 -v1553 -v1078 -v451 -v4384 -v3564 v2350 -v450 v4388 -v2354 -v670 v1217 v913 -v669 -v4046 -v4045 v2380 v1075 -v677 -v2210 -v681 -v4053 v2545 -v2209 v685 v4097 -v4057 v684 v4098 -v4061 -v2217 v1299 v4542 v4099 -v4060 -v2221 v4115 v3253 -v2582 -v2225 v3471 -v3403 v3255 -v2581 -v2224 -v946 -v4202 -v3866 v3473 -v3404 v3108 -v131 v4306 v4206 -v3479 v3405 v3110 v1474 v4307 -v3872 v3475 v3421 -v3330 v3249 -v2066 -v1495 -v102 v4308 v3487 -v2998 -v2489 v1491 -v106 v4324 -v4208 -v3877 -v3336 v3250 v3104 -v2997 v2578 v2072 v1490 v189 -v4209 v191 -v3878 -v3341 -v3105 -v3005 -v1502 -v3879 v3009 -v2484 -v1506 v187 -v4404 v3837 -v3261 v3165 v1740 -v964 -v777 -v3265 v3170 -v968 v776 v3166 -v3568 -v3178 v1755 v3502 -v3267 v2903 -v2893 v1757 -v1744 -v900 -v884 -v3506 -v3268 v2895 -v1763 -v1540 -v2906 -v2739 v1759 -v1541 v906 -v773 -v452 v1771 -v1542 -v454 -v2889 -v1558 -v911 -v4383 -v2890 v2352 v914 -v448 v4387 -v2356 v912 -v2376 -v449 -v671 v2541 v2379 -v2358 -v672 -v4047 -v2359 v673 -v4048 v2544 -v1295 -v689 -v4049 -v2211 -v4118 -v4065 -v2212 v1298 -v4196 -v4119 v3254 -v2213 v4195 v4114 -v2229 -v127 v3109 -v4203 v4112 -v3424 -v2062 -v1492 -v130 v4207 -v3865 v3474 -v3425 -v1494 v4327 -v4211 -v3867 -v3495 -v3420 -v2068 -v101 v4328 -v4210 -v3873 -v3491 -v3329 v190 -v105 v4323 -v3869 -v3490 -v3418 -v3331 -v3073 v2073 -v1488 -v3880 -v3337 -v2999 -v4321 -v3333 -v3000 v2074 -v1501 -v1489 -v3342 v3001 -v2485 v2075 -v1505 -v185 v4403 -v3262 v1741 -v963 -v3266 v3164 -v967 -v3270 -v3186 -v1745 -v880 -v3269 -v3182 -v2894 -v1743 v3501 -v3181 v2902 v2735 -v883 v3505 v1758 v899 -v453 v2908 -v2738 -v2401 -v1779 -v1561 v901 v2405 -v2346 v1775 -v1562 v907 -v2345 v1774 -v1557 v903 -v588 v915 -v4385 -v2911 v2810 v2353 -v1555 v4389 v2814 -v2357 v2375 -v2361 -v1648 -v2360 v4391 v2540 v2381 -v692 -v4392 -v693 -v4117 -v4068 v2546 -v1294 -v1270 -v688 v278 -v4116 -v4069 v1274 -v4064 -v2710 -v2384 -v2232 v1300 -v686 -v2714 -v2233 -v4062 -v3423 v2549 -v2228 -v1155 -v126 v4197 -v3422 -v1493 -v1159 -v4326 v4198 -v4113 -v4080 -v3492 -v2226 -v1303 v132 -v4325 v4199 -v3494 -v2061 v4215 v3069 -v2063 -v103 -v3868 -v2069 v107 -v3888 -v3488 -v3419 -v3072 v2065 v135 -v3884 -v3332 v2076 -v4322 -v3883 -v3489 -v3350 v3012 -v1503 -v109 -v3346 v3013 v1507 -v186 -v110 v4405 v3258 -v3183 v1742 v965 v3257 -v3185 v1746 v969 -v3274 -v2898 -v1038 -v879 -v1042 -v4409 v3503 -v3179 v2904 v2734 -v1776 -v1560 v971 -v885 v3507 -v1778 -v1559 v972 -v4176 -v3180 v2909 -v2740 -v2400 -v584 -v4379 -v4180 v2404 v902 -v4378 -v3509 v2912 v1772 -v923 -v888 v587 -v3510 v2910 -v2347 -v919 -v4386 v2809 -v2743 -v2371 -v2348 v1773 -v1644 -v1556 -v918 v4390 v2813 v2349 v4394 -v2536 v2377 -v2365 -v1647 -v691 v4393 -v690 -v4067 -v3846 v2542 v2382 v1290 -v274 -v4066 v3850 -v3531 v2547 v2385 -v2231 -v1296 -v1269 v277 v2383 -v2230 v1273 v2709 v2550 v1301 -v687 -v122 -v2713 v2548 -v4076 -v4063 -v1304 -v1154 v128 -v3493 -v1302 -v1158 v97 -v4218 -v4079 -v2227 v133 v96 v4219 v4214 -v3885 v3068 -v1886 v136 -v104 -v3887 -v2064 -v1890 -v1497 v134 v108 v4212 -v3347 v3074 v3011 v2084 v1496 v112 -v3349 v3010 v2080 v111 -v3881 v2079 v1504 -v3345 v1508 v4406 v3277 -v3184 v1754 v966 -v950 -v875 -v3497 v3278 -v1750 v970 v4410 -v3946 -v3496 -v3273 -v2730 -v1749 -v1037 v974 v881 -v4408 -v2897 -v1777 -v1041 v973 v3504 -v3271 -v2899 v2736 -v886 v3508 v2905 -v4175 -v3512 v2901 -v2741 v2402 -v920 -v889 v583 -v4179 -v3511 v2913 v2406 -v922 -v887 v2744 v589 -v4380 -v2742 -v4381 v2811 -v2408 v2368 -v1643 -v916 v4382 v2815 -v2409 -v2370 v2369 v4398 v2372 -v2364 -v2145 -v1649 -v917 -v592 -v2535 v2378 -v3845 -v3527 -v2817 v2537 v2374 -v2362 -v273 v3849 -v2818 v2543 v2386 v1289 -v3530 -v2685 v2539 -v1652 v1291 v1271 v279 -v2689 v2551 v1297 v1275 -v4555 v2711 v1293 -v2715 -v1305 -v121 -v4217 -v4075 -v1277 v1156 -v282 v123 -v4216 -v1278 v1160 v129 v4081 -v3064 -v2717 -v1130 v125 -v3886 -v2718 -v1134 v137 v98 v3070 v2081 -v1885 v1162 v99 -v3348 v2083 -v1889 v1163 v100 -v4213 -v4084 -v3589 v3075 v116 -v3593 v1498 -v3882 v3076 v2077 v1499 -v3343 v3077 v1500 v4407 -v3942 -v3275 v1753 v962 -v949 v4411 v961 -v874 -v3945 -v1747 v1039 v978 -v876 -v3498 -v2729 -v2396 v1043 v882 -v3499 -v3272 -v2731 -v2395 -v1748 v878 -v579 v3500 v2900 v2737 -v921 -v890 -v4177 v3516 -v2921 v2733 v2403 -v1045 v585 -v4181 v2917 -v2805 v2745 v2407 -v1046 v2916 -v2804 -v2411 -v2367 -v1639 v590 -v2410 v2366 -v4401 -v4183 v2812 -v2141 -v1645 v704 v593 v4402 -v4184 v2816 -v591 v4397 v2820 -v2144 -v1650 -v269 v2819 v2373 -v1265 -v4395 v3847 -v3526 v2394 -v2363 -v1653 -v1264 v275 v3851 -v2705 v2538 -v2390 -v1651 -v4551 -v3532 -v2704 -v2684 -v2559 -v2389 v1272 v280 -v2688 -v2555 v1292 v1276 -v1150 -v4554 -v4071 -v3853 v3436 v2712 -v2554 v1313 -v1280 -v1149 -v283 -v3854 -v2716 -v1309 -v1279 -v281 -v4077 -v3535 -v3197 -v2720 -v1308 v1157 -v2719 v1161 v124 v4082 v1165 -v1129 -v145 -v3063 -v2082 v1164 -v1133 -v141 -v4085 -v3065 v1887 -v140 v119 -v4083 v3071 -v1891 v120 -v3588 v3067 v2244 v115 -v3592 v3078 -v2078 -v1893 v1511 v113 -v3344 -v1894 v1512 v4419 -v3941 -v3276 v1751 -v1034 v981 -v951 v4415 v982 v4594 v4414 -v3947 v1040 v977 v4598 -v4171 v1044 -v877 -v4170 v3519 -v2918 v1048 -v975 -v954 -v898 v3520 -v2920 v2732 -v2397 -v1047 -v894 -v578 -v4178 v3950 v3515 v2753 -v2398 -v893 -v580 -v4182 -v2749 v2399 v586 -v4400 -v4186 v3513 v2914 -v2748 v2415 -v700 v582 -v4399 -v4185 v2806 -v1638 v594 -v3963 v2915 v2807 -v2140 -v1640 v703 -v3967 v3841 v2808 -v1646 v3840 -v3522 -v2824 -v2391 v2146 -v1642 v2393 -v1654 -v268 -v4396 v3848 v3528 -v2556 -v357 -v270 v3852 -v2558 -v1266 v276 -v4550 -v3856 v3533 -v3432 -v2686 -v2387 -v2149 v1310 v1267 v272 -v3855 v2706 v2690 v1312 v1268 v284 -v4556 v3536 v3435 -v3193 v2707 -v2552 -v2388 v1284 -v4070 v3534 v2708 v1151 -v4614 -v4072 -v3196 v2724 -v2692 -v2553 -v1306 -v1252 v1152 -v142 v4078 -v2693 -v1881 -v1256 v1153 -v144 -v4559 v4074 v2523 -v1880 -v1307 v1169 -v1131 -v118 v4086 -v2527 v1135 -v117 -v2860 -v2240 v1888 -v138 -v3066 -v2864 v1892 -v3590 v3086 v2243 -v1896 -v1510 -v1137 -v139 v3594 -v3082 -v1895 -v1509 -v1138 v3775 -v3081 v114 v4418 -v3943 v1752 -v979 -v952 -v1033 v4593 v4412 -v3948 v3518 -v1035 -v955 -v895 v4597 v3517 -v2919 v1036 -v953 -v897 -v4413 v3951 v2750 v1052 -v976 -v4172 v3949 v2752 -v4173 v2418 -v891 v4174 v2419 -v581 -v4190 v3514 -v2746 v2414 -v2136 -v892 -v699 v602 v598 -v3962 v2827 -v2747 -v2412 -v2142 v705 v597 -v3966 v2828 -v2392 -v1641 -v2823 v2147 -v1662 -v353 v3842 -v3521 -v2680 -v2557 -v1658 v4546 v3843 -v3523 -v2821 -v2679 v2150 -v1657 -v708 -v356 v3844 v3529 -v2148 v1311 -v271 -v4552 -v3860 v3525 -v3431 -v2687 v1287 v292 v3537 v2691 v1288 v288 -v4610 -v4557 v3437 -v3192 -v2727 -v2695 -v1283 v287 -v2728 -v2694 -v1125 -v143 -v4613 -v4560 -v3198 v2723 -v1281 -v1251 -v1172 -v1124 -v4558 -v4073 -v1255 -v1173 -v4094 -v3440 v2721 v2522 -v1168 v1132 v4090 -v3584 v2526 -v1882 v1136 v4089 -v3583 -v3201 v3083 -v2859 -v2239 -v1883 -v1166 -v1140 v3085 -v2863 v1884 -v1139 -v3771 -v3591 v2245 v1900 v3595 v3774 v3596 -v3079 v3597 -v4416 v3940 -v980 v3944 v956 -v896 v4595 v1055 v4599 v3952 -v2751 v1056 -v2417 -v1051 v2416 v4601 v4193 -v1049 -v695 v599 -v4602 v4194 v601 -v4189 v2826 v701 v2825 -v2135 -v4187 v3964 -v2413 -v2137 -v1659 v706 v595 v3968 -v2143 -v1661 v2139 v709 v596 v352 v2151 -v707 -v3970 v3863 -v3427 -v2822 -v1655 v1286 -v358 v289 v4545 -v3971 v3864 -v3524 -v2681 v1285 v291 v4547 -v3859 v3545 -v3433 -v3188 -v2726 v2682 -v1656 -v4553 v3541 -v2725 v2683 -v4609 v4549 -v3857 v3540 v3438 -v3194 v2699 -v1171 -v361 -v285 -v4561 -v1170 -v4615 -v4091 v3441 -v3199 -v1282 -v1253 -v286 -v4093 -v3439 -v1257 v1126 -v3202 v2722 v2524 -v2235 v1127 -v3200 v3084 v2528 v1128 -v4618 -v4087 v2861 -v2241 -v1903 -v1259 -v1167 -v1144 v3585 -v2865 -v1904 -v1260 -v4088 -v3770 v3586 -v2530 v2246 v1899 v3587 -v2531 v3776 v3600 -v3080 -v2867 v2247 v1897 -v2868 v2248 -v4417 v1054 v3939 v1053 v960 v4596 v959 v4600 v3956 v4604 v4192 v3955 v4603 v4191 v600 -v1050 v3958 -v694 v3957 v696 -v1660 v702 -v4188 v3965 v698 v350 v3969 -v2138 v710 v3973 -v3862 -v2158 v354 v3972 v3861 -v2155 v290 v3542 -v2154 v359 v3544 -v3426 -v4607 -v3428 v2702 -v362 v4548 v3434 #### 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.85 0.95 0.90 2/54 2498
Raw data (stat): 2498 (runsolver) R 2497 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421653822 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0012 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 2536 0 0 0 990 7 0 0 25 0 1 0 421653822 12898304 2503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3149 2503 603 41 0 3108 0
vsize: 12596
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 2602 0 0 0 1990 8 0 0 25 0 1 0 421653822 13164544 2569 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3214 2569 603 41 0 3173 0
vsize: 12856
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4082 0 0 0 2985 12 0 0 25 0 1 0 421653822 20037632 3949 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4892 3949 603 41 0 4851 0
vsize: 19568
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4128 0 0 0 3985 13 0 0 25 0 1 0 421653822 20172800 3995 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4925 3995 603 41 0 4884 0
vsize: 19700
[startup+50.0028 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4182 0 0 0 4985 13 0 0 25 0 1 0 421653822 20307968 4049 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4958 4049 603 41 0 4917 0
vsize: 19832
[startup+60.004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4225 0 0 0 5986 13 0 0 25 0 1 0 421653822 20574208 4092 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5023 4092 603 41 0 4982 0
vsize: 20092
[startup+70.0048 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4272 0 0 0 6986 13 0 0 25 0 1 0 421653822 20709376 4139 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5056 4139 603 41 0 5015 0
vsize: 20224
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4369 0 0 0 7986 13 0 0 25 0 1 0 421653822 21241856 4236 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5186 4236 603 41 0 5145 0
vsize: 20744
[startup+90.0048 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4382 0 0 0 8986 13 0 0 25 0 1 0 421653822 21241856 4249 4294967295 134512640 134672761 3221224544 3221223760 134557616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5186 4249 603 41 0 5145 0
vsize: 20744
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4424 0 0 0 9986 13 0 0 25 0 1 0 421653822 21377024 4291 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5219 4291 603 41 0 5178 0
vsize: 20876
[startup+110.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4476 0 0 0 10986 13 0 0 25 0 1 0 421653822 21647360 4343 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5285 4343 603 41 0 5244 0
vsize: 21140
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4531 0 0 0 11986 13 0 0 25 0 1 0 421653822 21782528 4398 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5318 4398 603 41 0 5277 0
vsize: 21272
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4595 0 0 0 12986 14 0 0 25 0 1 0 421653822 22052864 4462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5384 4462 603 41 0 5343 0
vsize: 21536
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4695 0 0 0 13985 14 0 0 25 0 1 0 421653822 22458368 4562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5483 4562 603 41 0 5442 0
vsize: 21932
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4837 0 0 0 14985 15 0 0 25 0 1 0 421653822 22921216 4678 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5596 4678 603 41 0 5555 0
vsize: 22384
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4899 0 0 0 15985 15 0 0 25 0 1 0 421653822 23191552 4740 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5662 4740 603 41 0 5621 0
vsize: 22648
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 4965 0 0 0 16985 15 0 0 25 0 1 0 421653822 23461888 4806 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5728 4806 603 41 0 5687 0
vsize: 22912
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 17984 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 18984 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 19984 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 20984 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 21985 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 22985 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 23985 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 24985 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 25985 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 26985 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 27986 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5095 0 0 0 28986 16 0 0 25 0 1 0 421653822 23711744 4879 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4879 603 41 0 5748 0
vsize: 23156
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5097 0 0 0 29986 16 0 0 25 0 1 0 421653822 23711744 4881 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5789 4881 603 41 0 5748 0
vsize: 23156
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5136 0 0 0 30986 16 0 0 25 0 1 0 421653822 23982080 4920 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5855 4920 603 41 0 5814 0
vsize: 23420
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5183 0 0 0 31986 16 0 0 25 0 1 0 421653822 24117248 4967 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5888 4967 603 41 0 5847 0
vsize: 23552
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5235 0 0 0 32986 17 0 0 25 0 1 0 421653822 24649728 5019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6018 5019 603 41 0 5977 0
vsize: 24072
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5349 0 0 0 33986 17 0 0 25 0 1 0 421653822 25055232 5133 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6117 5133 603 41 0 6076 0
vsize: 24468
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5439 0 0 0 34985 18 0 0 25 0 1 0 421653822 25456640 5223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6215 5223 603 41 0 6174 0
vsize: 24860
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5535 0 0 0 35985 18 0 0 25 0 1 0 421653822 25726976 5319 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6281 5319 603 41 0 6240 0
vsize: 25124
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5679 0 0 0 36984 19 0 0 25 0 1 0 421653822 26267648 5463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6413 5463 603 41 0 6372 0
vsize: 25652
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5792 0 0 0 37984 20 0 0 25 0 1 0 421653822 26804224 5576 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6544 5576 603 41 0 6503 0
vsize: 26176
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 5954 0 0 0 38983 20 0 0 25 0 1 0 421653822 27480064 5738 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6709 5738 603 41 0 6668 0
vsize: 26836
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 6159 0 0 0 39983 21 0 0 25 0 1 0 421653822 28286976 5943 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6906 5943 603 41 0 6865 0
vsize: 27624
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 6903 0 0 0 40981 23 0 0 25 0 1 0 421653822 31240192 6687 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7627 6687 603 41 0 7586 0
vsize: 30508
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 7514 0 0 0 41978 26 0 0 25 0 1 0 421653822 33783808 7298 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8248 7298 603 41 0 8207 0
vsize: 32992
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 8250 0 0 0 42975 29 0 0 25 0 1 0 421653822 36724736 8034 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8966 8034 603 41 0 8925 0
vsize: 35864
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 8861 0 0 0 43973 31 0 0 25 0 1 0 421653822 39284736 8645 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9591 8645 603 41 0 9550 0
vsize: 38364
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 9451 0 0 0 44971 34 0 0 25 0 1 0 421653822 41586688 9235 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10153 9235 603 41 0 10112 0
vsize: 40612
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 9988 0 0 0 45970 35 0 0 25 0 1 0 421653822 43876352 9772 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10712 9772 603 41 0 10671 0
vsize: 42848
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 10554 0 0 0 46967 38 0 0 25 0 1 0 421653822 46170112 10338 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11272 10338 603 41 0 11231 0
vsize: 45088
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 11080 0 0 0 47966 39 0 0 25 0 1 0 421653822 48865280 10864 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11930 10864 603 41 0 11889 0
vsize: 47720
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 11614 0 0 0 48965 41 0 0 25 0 1 0 421653822 51011584 11398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12454 11398 603 41 0 12413 0
vsize: 49816
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 12088 0 0 0 49963 42 0 0 25 0 1 0 421653822 52887552 11872 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12912 11872 603 41 0 12871 0
vsize: 51648
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 12592 0 0 0 50962 44 0 0 25 0 1 0 421653822 55029760 12376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13435 12376 603 41 0 13394 0
vsize: 53740
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 13097 0 0 0 51961 45 0 0 25 0 1 0 421653822 57049088 12881 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13928 12881 603 41 0 13887 0
vsize: 55712
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 13202 0 0 0 52961 46 0 0 25 0 1 0 421653822 57454592 12986 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14027 12986 603 41 0 13986 0
vsize: 56108
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 13333 0 0 0 53959 47 0 0 25 0 1 0 421653822 57987072 13117 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14157 13117 603 41 0 14116 0
vsize: 56628
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 13406 0 0 0 54958 48 0 0 25 0 1 0 421653822 58257408 13190 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14223 13190 603 41 0 14182 0
vsize: 56892
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 13544 0 0 0 55958 48 0 0 25 0 1 0 421653822 58793984 13328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14354 13328 603 41 0 14313 0
vsize: 57416
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 13938 0 0 0 56957 49 0 0 25 0 1 0 421653822 60403712 13722 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14747 13722 603 41 0 14706 0
vsize: 58988
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 14460 0 0 0 57956 51 0 0 25 0 1 0 421653822 62566400 14244 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15275 14244 603 41 0 15234 0
vsize: 61100
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 14951 0 0 0 58954 52 0 0 25 0 1 0 421653822 64610304 14735 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15774 14735 603 41 0 15733 0
vsize: 63096
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15318 0 0 0 59954 53 0 0 25 0 1 0 421653822 66105344 15102 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16139 15102 603 41 0 16098 0
vsize: 64556
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15489 0 0 0 60953 54 0 0 25 0 1 0 421653822 66777088 15273 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16303 15273 603 41 0 16262 0
vsize: 65212
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15605 0 0 0 61953 54 0 0 25 0 1 0 421653822 67182592 15389 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16402 15389 603 41 0 16361 0
vsize: 65608
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15720 0 0 0 62953 54 0 0 25 0 1 0 421653822 67723264 15504 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16534 15504 603 41 0 16493 0
vsize: 66136
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 63953 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 64954 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 65954 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 66954 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223736 134554697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 67953 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 68953 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 69953 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 70954 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 71954 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 72954 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+740.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 73954 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134553589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 74954 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+760.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 75955 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 76955 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 77955 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 78955 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 79955 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 80955 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 81956 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+830.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 82956 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223728 134559588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+840.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 83956 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 84956 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 85956 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 86957 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 87957 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 88957 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 89957 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+910.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 90957 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 91958 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 92958 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+940.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 93958 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+950.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 94958 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 95957 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 96957 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223684 134560629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 97957 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+990.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 98957 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 99958 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 100958 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223696 134565103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15849 0 0 0 101958 55 0 0 25 0 1 0 421653822 67944448 15582 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15582 603 41 0 16547 0
vsize: 66352
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15851 0 0 0 102958 55 0 0 25 0 1 0 421653822 67944448 15584 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15584 603 41 0 16547 0
vsize: 66352
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15855 0 0 0 103959 55 0 0 25 0 1 0 421653822 67944448 15588 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16588 15588 603 41 0 16547 0
vsize: 66352
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 15989 0 0 0 104958 56 0 0 25 0 1 0 421653822 68481024 15722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16719 15722 603 41 0 16678 0
vsize: 66876
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 16136 0 0 0 105958 56 0 0 25 0 1 0 421653822 69156864 15869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16884 15869 603 41 0 16843 0
vsize: 67536
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 16459 0 0 0 106957 57 0 0 25 0 1 0 421653822 70361088 16192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17178 16192 603 41 0 17137 0
vsize: 68712
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 16552 0 0 0 107957 58 0 0 25 0 1 0 421653822 70766592 16285 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17277 16285 603 41 0 17236 0
vsize: 69108
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 16693 0 0 0 108957 58 0 0 25 0 1 0 421653822 71307264 16426 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17409 16426 603 41 0 17368 0
vsize: 69636
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 16842 0 0 0 109956 58 0 0 25 0 1 0 421653822 71983104 16575 4294967295 134512640 134672761 3221224544 3221223784 134560737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17574 16575 603 41 0 17533 0
vsize: 70296
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 17119 0 0 0 110955 60 0 0 25 0 1 0 421653822 73064448 16852 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17838 16852 603 41 0 17797 0
vsize: 71352
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 17570 0 0 0 111954 61 0 0 25 0 1 0 421653822 74932224 17303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18294 17303 603 41 0 18253 0
vsize: 73176
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 18001 0 0 0 112952 63 0 0 25 0 1 0 421653822 76668928 17734 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18718 17734 603 41 0 18677 0
vsize: 74872
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 18289 0 0 0 113951 64 0 0 25 0 1 0 421653822 77746176 18022 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18981 18022 603 41 0 18940 0
vsize: 75924
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 18418 0 0 0 114951 64 0 0 25 0 1 0 421653822 78286848 18151 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19113 18151 603 41 0 19072 0
vsize: 76452
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 18997 0 0 0 115949 66 0 0 25 0 1 0 421653822 80711680 18730 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19705 18730 603 41 0 19664 0
vsize: 78820
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 19703 0 0 0 116947 69 0 0 25 0 1 0 421653822 83542016 19436 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20396 19436 603 41 0 20355 0
vsize: 81584
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 20044 0 0 0 117946 70 0 0 25 0 1 0 421653822 84881408 19777 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20723 19777 603 41 0 20682 0
vsize: 82892
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 20130 0 0 0 118946 70 0 0 25 0 1 0 421653822 86331392 19863 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21077 19863 603 41 0 21036 0
vsize: 84308
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2498
Raw data (stat): 2498 (minisat+) R 2497 29151 29150 0 -1 0 20300 0 0 0 119946 70 0 0 25 0 1 0 421653822 87007232 20033 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21242 20033 603 41 0 21201 0
vsize: 84968
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2498
Raw data (stat): 2498 (minisat+) Z 2497 29151 29150 0 -1 12 20303 0 0 0 119947 74 0 0 25 0 1 0 421653822 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: 10
Real time (s): 1200.09
CPU time (s): 1200.22
CPU user time (s): 1199.47
CPU system time (s): 0.747886
CPU usage (%): 100.011
Max. virtual memory (Kb): 84968
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####