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:100.opb
MD5SUM	ac4ddb996334a0834a018e09e97d1ecb
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	76
Optimality of the best value was proved	NO
Number of terms in the objective function	4617
Biggest coefficient in the objective function	2642
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	13340
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	2642
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	13340
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.06984
Number of variables	4617
Total number of constraints	9896
Number of constraints which are clauses	4395
Number of constraints which are cardinality constraints (but not clauses)	5501
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	23
Trace number 5314

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        853400 kB
Buffers:         33588 kB
Cached:         110744 kB
SwapCached:       3160 kB
Active:          50308 kB
Inactive:       100044 kB
HighTotal:      131008 kB
HighFree:        16828 kB
LowTotal:       903652 kB
LowFree:        836572 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25376 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:41:08 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3754 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5279 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 890]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 889]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 888]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 887]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 886]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 885]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 884]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 883]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 882]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 881]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 880]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 879]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 878]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 877]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 874]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 873]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 872]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 871]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 870]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 869]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 868]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 867]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 866]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 865]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 864]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 862]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 861]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 860]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 859]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 858]---> Adder-cost: 11   maxlim: 2   bits: 3/2
c ---[ 857]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 856]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 855]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 854]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 853]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 852]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 851]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 850]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 849]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 847]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 846]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 845]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 844]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 843]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 842]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 841]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 840]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 839]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 838]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 837]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 836]---> Adder-cost: 17   maxlim: 1   bits: 2/1
c ---[ 835]---> Adder-cost: 14   maxlim: 1   bits: 2/1
c ---[ 834]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 833]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 832]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 831]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 830]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 829]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 828]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 827]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 826]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 825]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 824]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 823]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 822]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 821]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 820]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 819]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 818]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 817]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 816]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 815]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 814]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 813]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 812]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 811]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 810]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 809]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 806]---> Adder-cost: 20   maxlim: 1   bits: 2/1
c ---[ 805]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 804]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 803]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 802]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 801]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 800]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 799]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 798]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 797]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 796]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 795]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 794]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 793]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 792]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 791]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 790]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 789]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 788]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 787]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 786]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 785]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 784]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 783]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 782]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 781]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 780]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 779]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 778]---> Adder-cost: 17   maxlim: 1   bits: 2/1
c ---[ 777]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 776]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 775]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 774]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 773]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 772]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 771]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 770]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 769]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 768]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 767]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 766]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 765]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 764]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 763]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 762]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 761]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 760]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 759]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 758]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 757]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 756]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 755]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 754]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 753]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 752]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 751]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 750]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 749]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 748]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 747]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 746]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 745]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 744]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 743]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 742]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 741]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 740]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 739]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 738]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 737]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 736]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 735]---> Adder-cost: 20   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: 20   maxlim: 2   bits: 3/2
c ---[ 729]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 728]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 727]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 726]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 725]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 724]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 723]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 722]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 721]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 720]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 719]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 718]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 717]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 716]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 715]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 714]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 713]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 712]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 711]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 710]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 709]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 708]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 707]---> Adder-cost: 22   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: 15   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: 15   maxlim: 2   bits: 3/2
c ---[ 698]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 697]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 696]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 695]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 694]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 693]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 692]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 691]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 690]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 689]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 688]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 687]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 686]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 685]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 684]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 683]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 682]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 681]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 680]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 679]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 678]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 677]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 676]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 675]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 674]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 673]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 672]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 671]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 670]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 669]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 668]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 667]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 666]---> Adder-cost: 22   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: 22   maxlim: 2   bits: 3/2
c ---[ 662]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 661]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 660]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 659]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 658]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 657]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 656]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 655]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 654]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 653]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 652]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 651]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 650]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 649]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 648]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 647]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 646]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 645]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 644]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 643]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 642]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 641]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 640]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 639]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 638]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 637]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 636]---> Adder-cost: 25   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: 27   maxlim: 2   bits: 3/2
c ---[ 632]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 631]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 630]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 629]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 628]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 627]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 626]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 625]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 624]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 623]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 622]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 621]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 620]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 619]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 618]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 617]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 616]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 615]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 614]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 613]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 612]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 611]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 610]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 609]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 608]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 607]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 606]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 605]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 604]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 603]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 602]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 601]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 600]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 599]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 598]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 597]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 596]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 595]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 594]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 593]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 592]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 591]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 590]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 589]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 588]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 587]---> Adder-cost: 20   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: 13   maxlim: 2   bits: 3/2
c ---[ 583]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 582]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 581]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 580]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 579]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 578]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 577]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 576]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 575]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 574]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 573]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 572]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 571]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 570]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 569]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 568]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 567]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 566]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 565]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 564]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 563]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 562]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 561]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 560]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 559]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 558]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 557]---> Adder-cost: 20   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: 13   maxlim: 2   bits: 3/2
c ---[ 553]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 552]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 551]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 550]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 549]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 548]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 547]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 546]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 545]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 544]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 543]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 542]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 541]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 540]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 539]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 538]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 537]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 536]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 535]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 534]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 533]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 532]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 531]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 530]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 529]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 528]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 527]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 526]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 525]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 524]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 523]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 522]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 521]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 520]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 519]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 518]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 517]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 516]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 515]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 514]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 513]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 512]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 511]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 510]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 509]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 508]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 507]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 506]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 505]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 504]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 503]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 502]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 501]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 500]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 499]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 498]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 497]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 496]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 495]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 494]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 493]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 492]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 491]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 490]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 489]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 488]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 487]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 486]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 485]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 484]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 483]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 482]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 481]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 480]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 479]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 478]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 477]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 476]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 475]---> Adder-cost: 20   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: 27   maxlim: 2   bits: 3/2
c ---[ 470]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 469]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 468]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 467]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 466]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 465]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 464]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 463]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 462]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 461]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 460]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 459]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 458]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 457]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 456]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 455]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 454]---> Adder-cost: 22   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: 22   maxlim: 2   bits: 3/2
c ---[ 450]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 449]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 448]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 447]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 446]---> Adder-cost: 11   maxlim: 2   bits: 3/2
c ---[ 445]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 444]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 443]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 442]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 441]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 440]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 439]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 438]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 437]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 436]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 435]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 434]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 433]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 432]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 431]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 430]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 429]---> Adder-cost: 20   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: 27   maxlim: 2   bits: 3/2
c ---[ 425]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 424]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 423]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 422]---> Adder-cost: 20   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: 11   maxlim: 2   bits: 3/2
c ---[ 418]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 417]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 416]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 415]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 414]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 413]---> Adder-cost: 22   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: 22   maxlim: 2   bits: 3/2
c ---[ 409]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 408]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 407]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 406]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 405]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 404]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 403]---> Adder-cost: 22   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: 29   maxlim: 2   bits: 3/2
c ---[ 398]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 397]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 396]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 395]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 394]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 393]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 392]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 391]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 390]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 389]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 388]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 387]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 386]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 385]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 384]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 383]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 382]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 381]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 380]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 379]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 378]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 377]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 376]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 375]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 374]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 373]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 372]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 371]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 370]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 369]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 368]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 367]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 366]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 365]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 364]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 363]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 362]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 361]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 360]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 359]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 358]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 357]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 356]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 355]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 354]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 353]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 352]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 351]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 350]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 349]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 348]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 347]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 346]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 345]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 344]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 343]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 342]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 341]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 340]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 339]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 338]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 337]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 336]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 335]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 334]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 333]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 332]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 331]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 330]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 329]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 328]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 327]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 326]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 325]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 324]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 323]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 322]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 321]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 320]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 319]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 318]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 317]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 316]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 315]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 314]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 313]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 312]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 311]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 310]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 309]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 308]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 307]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 306]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 305]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 304]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 303]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 302]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 301]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 300]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 299]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 298]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 297]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 296]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 295]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 294]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 293]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 292]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 291]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 290]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 289]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 288]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 287]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 286]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 285]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 284]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 283]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 282]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 281]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 280]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 279]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 278]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 277]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 276]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 275]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 274]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 273]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 272]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 271]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 270]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 269]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 268]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 267]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 266]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 265]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 264]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 263]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 262]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 261]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 260]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 259]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 258]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 257]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 256]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 255]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 254]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 253]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 252]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 251]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 250]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 249]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 248]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 247]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 246]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 245]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 244]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 243]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 242]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 241]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 240]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 239]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 238]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 237]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 236]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 235]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 234]---> Adder-cost: 15   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: 13   maxlim: 2   bits: 3/2
c ---[ 230]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 229]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 228]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 227]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 226]---> Adder-cost: 15   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: 27   maxlim: 2   bits: 3/2
c ---[ 222]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 221]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 220]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 219]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 218]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 217]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 216]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 215]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 214]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 213]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 212]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 211]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 210]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 209]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 208]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 207]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 206]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 205]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 204]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 203]---> Adder-cost: 15   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: 11   maxlim: 2   bits: 3/2
c ---[ 199]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 198]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 197]---> Adder-cost: 15   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: 22   maxlim: 2   bits: 3/2
c ---[ 193]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 192]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 191]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 190]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 189]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 188]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 187]---> Adder-cost: 25   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: 22   maxlim: 2   bits: 3/2
c ---[ 183]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 182]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 181]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 180]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 179]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 178]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 177]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 176]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 175]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 174]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 173]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 172]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 171]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 170]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 169]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 168]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 167]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 166]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 165]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 164]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 163]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 162]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 161]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 160]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 159]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 158]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 157]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 156]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 155]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 154]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 153]---> Adder-cost: 20   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: 15   maxlim: 2   bits: 3/2
c ---[ 149]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 147]---> Adder-cost: 13   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: 15   maxlim: 2   bits: 3/2
c ---[ 143]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 142]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 141]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 140]---> Adder-cost: 8   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: 15   maxlim: 2   bits: 3/2
c ---[ 136]---> Adder-cost: 15   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: 15   maxlim: 2   bits: 3/2
c ---[ 132]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 131]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 130]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 129]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 128]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 127]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 126]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 125]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 124]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 123]---> Adder-cost: 15   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: 13   maxlim: 2   bits: 3/2
c ---[ 118]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 117]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 116]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 115]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 114]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 113]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 111]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 110]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 109]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 108]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 107]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 106]---> Adder-cost: 11   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 104]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 103]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 102]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  98]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  97]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  96]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  94]---> Adder-cost: 20   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: 15   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  89]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  87]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  86]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  73]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  72]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  67]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  66]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  63]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  62]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  61]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  59]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  58]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  53]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  48]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  45]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  39]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  38]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  36]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  35]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  34]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  33]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  31]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  30]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  29]---> Adder-cost: 6   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 ---[  26]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  25]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  24]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  22]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  21]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  20]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  18]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  17]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  15]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  13]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  12]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  11]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  10]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   9]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   8]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   7]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   6]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   5]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   4]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   3]---> Adder-cost: 13   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 |   94942   330198 |   31647       0        0     nan |  0.000 % |
c |       100 |   94930   330164 |   34811      98      397     4.1 |  8.026 % |
c |       250 |   94930   330164 |   38292     248     1032     4.2 |  8.026 % |
c |       475 |   94930   330164 |   42122     473     2117     4.5 |  8.026 % |
c |       812 |   94924   330147 |   46334     809     3506     4.3 |  8.031 % |
c |      1318 |   94912   330113 |   50967    1312     5949     4.5 |  8.040 % |
c |      2077 |   94906   330096 |   56064    2070     9618     4.6 |  8.045 % |
c |      3217 |   94906   330096 |   61671    3210    14972     4.7 |  8.045 % |
c |      4926 |   94906   330096 |   67838    4919    23533     4.8 |  8.045 % |
c |      7488 |   94906   330096 |   74621    7481    36370     4.9 |  8.045 % |
c |     11332 |   94906   330096 |   82084   11325    56233     5.0 |  8.045 % |
c ==============================================================================
c [1mFound solution: 1056[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11262   maxlim: 7000   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11892 |  173682   611437 |   57894   11885    59289     5.0 |  8.045 % |
c |     11992 |  173682   611437 |   63683   11985    59709     5.0 |  5.332 % |
c |     12142 |  173682   611437 |   70051   12135    60434     5.0 |  5.332 % |
c |     12367 |  173682   611437 |   77056   12360    61637     5.0 |  5.332 % |
c |     12704 |  173682   611437 |   84762   12697    63467     5.0 |  5.332 % |
c |     13210 |  173682   611437 |   93238   13203    66171     5.0 |  5.332 % |
c |     13969 |  173673   611406 |  102562   13955    70310     5.0 |  5.335 % |
c |     15108 |  173673   611406 |  112819   15094    78386     5.2 |  5.335 % |
c |     16816 |  173673   611406 |  124100   16802   101922     6.1 |  5.335 % |
c |     19378 |  173667   611389 |  136511   19363   122537     6.3 |  5.338 % |
c |     23222 |  173658   611358 |  150162   23204   145912     6.3 |  5.341 % |
c ==============================================================================
c [1mFound solution: 832[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7224   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28501 |  173668   611425 |   57889   28483   180304     6.3 |  5.341 % |
c |     28601 |  173668   611425 |   63677   28583   180807     6.3 |  5.355 % |
c |     28751 |  173668   611425 |   70045   28733   181750     6.3 |  5.355 % |
c |     28976 |  173668   611425 |   77050   28958   184465     6.4 |  5.355 % |
c |     29313 |  173668   611425 |   84755   29295   186164     6.4 |  5.355 % |
c |     29819 |  173668   611425 |   93230   29801   188533     6.3 |  5.355 % |
c |     30578 |  173668   611425 |  102553   30560   192302     6.3 |  5.355 % |
c |     31717 |  173668   611425 |  112809   31699   198475     6.3 |  5.355 % |
c |     33425 |  173659   611394 |  124090   33405   207838     6.2 |  5.358 % |
c |     35987 |  173653   611377 |  136499   35965   224094     6.2 |  5.361 % |
c |     39831 |  173653   611377 |  150149   39809   250675     6.3 |  5.361 % |
c |     45597 |  173644   611346 |  165164   45573   294136     6.5 |  5.364 % |
c |     54247 |  173644   611346 |  181680   54223   371656     6.9 |  5.364 % |
c |     67222 |  173635   611315 |  199848   67191   659648     9.8 |  5.367 % |
c |     86683 |  173635   611315 |  219833   86652  1290597    14.9 |  5.367 % |
c |    115875 |  173635   611315 |  241816  115844  3429060    29.6 |  5.367 % |
c |    159664 |  173635   611315 |  265998  159633  6716831    42.1 |  5.367 % |
c ==============================================================================
c [1mFound solution: 824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7232   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    179663 |  173638   611341 |   57879  179632  7125213    39.7 |  5.367 % |
c |    179764 |  173638   611341 |   63666   22241   255157    11.5 |  5.372 % |
c |    179915 |  173638   611341 |   70033   22392   255962    11.4 |  5.372 % |
c |    180140 |  173638   611341 |   77036   22617   257374    11.4 |  5.372 % |
c |    180477 |  173638   611341 |   84740   22954   259420    11.3 |  5.372 % |
c |    180983 |  173638   611341 |   93214   23460   262424    11.2 |  5.372 % |
c |    181742 |  173638   611341 |  102536   24219   267440    11.0 |  5.372 % |
c |    182881 |  173638   611341 |  112789   25358   277263    10.9 |  5.372 % |
c |    184589 |  173638   611341 |  124068   27066   287563    10.6 |  5.372 % |
c |    187151 |  173638   611341 |  136475   29628   302657    10.2 |  5.372 % |
c ==============================================================================
c [1mFound solution: 755[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7301   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    188547 |  173647   611398 |   57882   31024   310846    10.0 |  5.372 % |
c |    188647 |  173647   611398 |   63670   31124   311616    10.0 |  5.381 % |
c |    188797 |  173647   611398 |   70037   31274   312447    10.0 |  5.381 % |
c |    189022 |  173647   611398 |   77040   31499   313749    10.0 |  5.381 % |
c |    189359 |  173647   611398 |   84745   31836   315898     9.9 |  5.381 % |
c |    189865 |  173647   611398 |   93219   32342   319204     9.9 |  5.381 % |
c |    190624 |  173647   611398 |  102541   33101   323690     9.8 |  5.381 % |
c |    191763 |  173647   611398 |  112795   34240   330734     9.7 |  5.381 % |
c |    193474 |  173647   611398 |  124075   35951   341750     9.5 |  5.381 % |
c |    196036 |  173647   611398 |  136482   38513   358688     9.3 |  5.381 % |
c ==============================================================================
c [1mFound solution: 673[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7383   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    196525 |  173652   611434 |   57884   39002   361957     9.3 |  5.381 % |
c |    196625 |  173652   611434 |   63672   39102   362526     9.3 |  5.389 % |
c |    196775 |  173652   611434 |   70039   39252   363384     9.3 |  5.389 % |
c |    197000 |  173652   611434 |   77043   39477   366287     9.3 |  5.389 % |
c |    197337 |  173652   611434 |   84747   39814   368162     9.2 |  5.389 % |
c |    197843 |  173652   611434 |   93222   40320   372310     9.2 |  5.389 % |
c |    198602 |  173652   611434 |  102545   41079   377650     9.2 |  5.389 % |
c |    199741 |  173652   611434 |  112799   42218   389352     9.2 |  5.389 % |
c |    201449 |  173652   611434 |  124079   43926   412161     9.4 |  5.389 % |
c |    204012 |  173652   611434 |  136487   46489   442291     9.5 |  5.389 % |
c ==============================================================================
c [1mFound solution: 653[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7403   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    205362 |  173655   611469 |   57885   47839   454290     9.5 |  5.389 % |
c |    205462 |  173655   611469 |   63673   47939   454990     9.5 |  5.398 % |
c |    205612 |  173655   611469 |   70040   48089   456041     9.5 |  5.398 % |
c |    205837 |  173655   611469 |   77044   48314   457509     9.5 |  5.398 % |
c |    206174 |  173655   611469 |   84749   48651   459790     9.5 |  5.398 % |
c |    206680 |  173655   611469 |   93224   49157   463201     9.4 |  5.398 % |
c |    207439 |  173655   611469 |  102546   49916   467963     9.4 |  5.398 % |
c |    208579 |  173655   611469 |  112801   51056   477554     9.4 |  5.398 % |
c |    210287 |  173655   611469 |  124081   52764   489293     9.3 |  5.398 % |
c |    212849 |  173655   611469 |  136489   55326   508813     9.2 |  5.398 % |
c |    216693 |  173655   611469 |  150138   59170   550438     9.3 |  5.398 % |
c |    222459 |  173655   611469 |  165152   64936   596642     9.2 |  5.398 % |
c |    231109 |  173655   611469 |  181667   73586   711174     9.7 |  5.398 % |
c |    244083 |  173655   611469 |  199834   86560   920317    10.6 |  5.398 % |
c ==============================================================================
c [1mFound solution: 626[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7430   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    245771 |  173665   611538 |   57888   88248   938008    10.6 |  5.398 % |
c |    245872 |  173665   611538 |   63676   22238   188596     8.5 |  5.409 % |
c |    246022 |  173665   611538 |   70044   22388   189621     8.5 |  5.409 % |
c |    246247 |  173665   611538 |   77048   22613   190929     8.4 |  5.409 % |
c |    246584 |  173665   611538 |   84753   22950   192834     8.4 |  5.409 % |
c |    247091 |  173665   611538 |   93229   23457   199631     8.5 |  5.409 % |
c |    247850 |  173665   611538 |  102552   24216   204721     8.5 |  5.409 % |
c |    248989 |  173665   611538 |  112807   25355   211553     8.3 |  5.409 % |
c |    250697 |  173665   611538 |  124088   27063   223027     8.2 |  5.409 % |
c |    253259 |  173665   611538 |  136496   29625   307792    10.4 |  5.409 % |
c |    257103 |  173665   611538 |  150146   33469   332254     9.9 |  5.409 % |
c |    262869 |  173665   611538 |  165161   39235   379976     9.7 |  5.409 % |
c |    271518 |  173665   611538 |  181677   47884   697822    14.6 |  5.409 % |
c |    284493 |  173665   611538 |  199845   60859  1131351    18.6 |  5.409 % |
c |    303954 |  173665   611538 |  219829   80320  1555313    19.4 |  5.409 % |
c |    333146 |  173665   611538 |  241812  109512  4303021    39.3 |  5.409 % |
c |    376937 |  173665   611538 |  265993  153303 10054297    65.6 |  5.409 % |
c |    442621 |  173665   611538 |  292593  218987 15319194    70.0 |  5.409 % |
c |    541147 |  173665   611538 |  321852   42586  1562112    36.7 |  5.409 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v4075 v3895 v668 -v176 v4076 -v180 v3894 -v2907 -v1568 v1450 -v671 v3178 v1573 -v1454 -v672 v3900 v3177 -v2876 v1572 v3898 -v2881 -v1265 v3179 -v2880 v1575 -v1264 -v1034 v78 v3899 v3181 v1576 -v1266 -v1038 -v3903 -v2883 -v1579 v1267 -v1009 v77 v3182 -v2884 -v1577 v1268 v1013 -v81 v3920 v3184 -v2887 -v1578 -v1275 -v7 v3185 -v2885 v1269 -v82 -v11 v3923 -v2886 -v2380 v1270 v196 v3924 -v3071 v1271 v4616 -v3070 -v3454 -v2333 -v1615 v199 -v3570 v2332 -v1620 v200 v4286 -v3569 -v3078 v2334 -v1637 v1619 -v203 -v4290 -v4117 -v3571 v3072 v2337 -v1636 -v201 -v4116 -v3572 -v3311 v3073 v2336 -v1638 v1622 -v202 -v4118 v3573 -v3310 v3074 -v2559 v2341 -v1954 v1641 v1623 -v4119 v3580 v3312 -v2558 v2340 -v1953 v1640 v1626 v4120 v3574 -v3315 -v2560 v2338 v1645 v1624 -v4127 v3575 v3314 -v2561 v2339 -v1955 v1644 -v1625 v4121 v3576 v3318 v2562 -v1957 v1642 v4122 v3316 v2567 v1643 -v625 v4123 v3317 v2563 -v1958 -v3380 -v3384 -v4140 v4077 -v3890 -v2903 v667 -v175 -v179 v3896 -v2906 v2670 v1449 -v673 -v236 -v3173 v1567 -v1453 v240 -v4080 v3901 -v3172 v1569 -v2875 v1574 -v3904 v3180 -v2877 v1571 -v1033 -v676 -v3902 v3183 -v2882 v1580 -v1037 v3187 -v2879 v1278 -v1008 v79 v3186 -v2888 v1279 v1012 -v83 v3919 -v1274 -v760 -v6 -v10 v3925 -v2379 -v1272 v85 v195 v86 -v3450 v197 v3928 -v3453 -v3081 -v3082 -v1614 -v204 v4285 -v3077 v2384 -v1616 v4289 v2335 v1621 -v3583 -v3075 v2349 v1618 -v3584 v2345 -v1949 -v1639 v1627 -v4130 -v3579 v2344 -v1948 -v1653 v4131 v3313 v1649 -v4126 -v3577 v3326 -v2570 -v1956 v1648 -v621 -v3322 v2571 -v1959 -v4124 -v3321 v2566 v1960 v624 v1961 -v4136 -v3379 -v3111 -v663 -v3383 -v3115 -v4139 v4078 -v2902 v2671 -v1903 v669 -v177 -v3889 v2669 -v181 -v4456 -v4081 -v3891 -v2908 -v2216 v1451 -v674 v235 -v4079 v3897 -v2220 -v1455 v239 v3893 -v677 v183 v3905 -v3174 v1570 -v675 v184 -v73 -v4390 -v3175 v2911 v1588 -v1457 -v1277 -v1035 v72 v3176 -v2878 v1584 -v1458 v1276 -v1039 -v3915 v3191 -v2896 -v1980 v1583 -v1010 -v756 v80 -v2892 v1014 -v84 v3921 -v3093 -v2891 -v2376 -v1041 -v759 v88 v8 -v1042 v87 -v12 v3926 -v2772 -v2381 -v1273 -v1016 -v1017 v3929 -v3449 -v3080 v14 v3927 -v3079 v198 v15 v3455 v2385 v212 v2383 v208 v4287 -v3582 -v2346 v207 v4291 -v3581 v2348 v1617 -v4129 -v3458 -v3076 -v1650 v1635 -v382 -v265 -v4128 -v1652 v1631 -v386 -v4293 v3323 -v2569 v2342 v1630 -v4294 v3325 -v2568 -v1950 -v3578 v2343 v1951 v1646 -v620 -v334 v1952 v338 -v4125 -v3949 -v3319 v2564 -v1965 v1647 v626 -v4135 -v4074 -v3381 v3110 -v2898 -v1899 -v172 -v3385 v3114 v2672 -v1445 -v662 -v4457 -v4141 v3030 -v2904 -v1902 -v1499 -v1444 -v664 -v178 -v4455 -v4082 -v1503 v670 v182 -v3387 -v3003 -v2909 -v2215 v1452 v666 v237 v186 -v3892 -v3388 -v3007 -v2219 -v1456 -v1029 -v678 v241 v185 -v4386 -v4144 -v3913 v2912 -v1585 -v1460 -v1059 -v1028 -v3909 v2910 v1587 -v1459 -v1063 -v1004 -v4389 -v3908 v3194 -v2893 -v1976 -v1036 -v1003 -v243 v3195 -v2895 -v1040 -v244 v74 -v2 v3190 v3089 v1979 v1581 -v1044 -v1011 -v755 -v361 v75 -v1 -v3914 -v1043 v1015 v76 -v3916 -v3188 -v3092 -v2889 -v2768 v1582 v1019 -v761 v92 v9 v3922 -v2375 v1018 -v13 v3918 -v3445 -v2890 -v2771 v2377 v17 v3930 -v2382 v16 v3451 -v764 -v209 -v4281 v2386 v211 -v4280 v3456 -v1789 -v2347 v4288 v3459 v1632 -v261 v205 v4292 -v3457 -v1651 v1634 -v4296 -v3479 v381 -v264 v206 -v4295 v3324 -v385 v1628 -v616 -v3945 v1968 -v1629 -v1355 -v1238 -v622 v333 v1969 -v1359 v337 v3948 -v3320 v2565 -v1964 v627 -v4137 -v3382 v3112 v3026 v2680 -v1932 -v1898 -v4458 -v4073 -v3386 v3116 v2897 -v2676 -v231 -v171 -v4142 v4090 -v3390 v3029 v2899 -v2675 -v1904 -v1498 -v230 -v173 -v4086 -v3389 v2905 v1502 -v1446 v665 v174 -v4145 -v4085 -v3910 -v3118 -v3002 v2901 v2217 -v1447 -v686 v238 v190 -v4143 -v3912 -v3119 -v3006 v2913 v2221 -v1586 v1448 -v682 v242 -v4385 v4012 v3193 -v1907 -v1464 -v1058 -v681 -v246 v3192 -v2894 -v1062 -v1030 -v245 -v4391 -v4315 -v3906 -v2223 -v1975 -v1031 -v751 -v357 -v2224 -v1032 -v1005 -v3907 v3088 -v2096 v1981 -v1048 -v1006 -v757 -v360 -v95 -v2100 v1007 -v96 v3 -v4394 -v3189 v3094 -v2767 -v1023 -v762 v91 v4 -v3917 v5 v3938 -v2773 -v1984 -v765 v89 v21 -v3934 -v3444 v2378 -v763 -v210 -v3933 -v3446 -v3097 v2394 v1785 v3452 v2390 v3448 -v3295 -v2776 v2389 -v1788 v4282 v3460 v1633 v4283 -v3983 -v3475 -v260 v4284 -v3987 v4300 -v3478 -v1876 v383 -v266 v1880 -v387 v4265 -v1967 -v1234 -v1966 -v615 -v3944 -v1354 -v1237 v617 -v389 v335 -v269 -v1358 v623 -v390 v339 v3950 -v1962 v619 v628 -v4466 v4133 -v4087 -v3378 v3113 v3025 -v2679 -v1931 -v1900 v4462 -v4138 -v4089 -v3377 v3117 -v2211 v4461 v4134 -v3394 -v3121 v3031 -v2673 -v2210 -v1905 -v1500 -v683 -v313 v193 -v4146 -v3911 -v3120 v2900 v1504 -v685 v232 v194 -v4381 -v4083 -v4008 v3004 v2921 -v2674 -v2401 v2218 v1908 -v1467 v233 -v189 -v3008 -v2917 v2405 v2222 -v1906 -v1468 v234 -v4387 -v4311 -v4084 v4011 -v3034 -v2916 -v2226 -v1971 -v1760 -v1506 -v1463 -v1060 -v679 v250 -v187 -v2225 -v1764 -v1507 -v1064 -v4392 -v4314 -v3084 -v3010 -v1977 -v1461 -v1051 -v680 -v356 -v94 -v3011 -v1052 -v750 -v93 -v4395 v3090 -v2763 -v2095 v1982 -v1066 -v1047 -v1026 -v752 v362 -v4393 -v2099 -v1067 -v1027 -v758 v3935 v3095 -v2769 v1985 -v1045 -v1022 -v754 -v24 v3937 -v1983 -v766 -v25 -v3098 -v2774 v2391 -v1020 -v365 v90 v20 -v3096 v2393 -v3931 -v3291 v2777 v1784 v18 -v3447 -v2775 -v3932 v3468 -v3294 -v2387 v1790 -v571 v256 v3464 -v575 -v377 v4303 -v3982 -v3474 v3463 -v2388 -v376 v262 v4304 -v3986 -v4299 -v4261 v3480 -v1875 -v1793 -v525 v384 -v267 v1879 v388 v329 -v4297 v4264 -v4186 v3940 -v1233 -v392 v328 -v270 -v4190 -v391 -v268 -v3946 v3483 -v1356 -v1239 v336 -v32 v1360 v618 v340 -v36 v3951 -v1963 -v636 v341 v632 v342 -v4465 -v4088 -v3397 -v3109 v3027 -v2677 -v2288 v1933 -v1896 -v1495 -v309 -v192 v4132 -v3398 v3108 -v2998 -v2292 v1901 -v684 -v191 -v4459 -v4154 -v3393 v3125 v3032 -v2997 v2918 v1897 -v1501 -v1466 -v312 -v4150 v2920 -v2212 v1909 v1505 -v1465 -v1054 -v4460 -v4149 v4007 -v3391 -v3035 v3005 -v2400 -v2213 v1937 v1509 -v1053 -v253 -v4380 -v3033 -v3009 v2404 v2214 -v1508 -v254 -v4382 v4310 v4013 -v3013 -v2914 v2230 -v1759 v1061 -v1050 -v352 -v249 -v188 -v4388 -v3012 -v1970 -v1763 -v1065 -v1049 -v4384 -v4316 -v2915 v1972 -v1462 -v1069 -v1025 v358 -v247 -v4396 -v3083 -v1978 -v1068 -v1024 -v4016 v3085 v2097 v1974 v363 -v23 -v3936 v3091 -v2762 -v2101 v1986 -v753 -v22 -v4319 v3087 v2764 -v1046 -v774 -v366 -v3099 -v2770 v2392 -v770 -v364 v2766 -v2103 -v1780 -v1021 -v769 v2778 -v2104 -v3465 -v3290 v1786 v19 v3467 -v4302 -v3470 -v3296 v1791 -v570 -v4301 -v574 v255 v3984 v3476 -v3461 v1794 -v521 v257 -v3988 -v1792 v378 v263 v4260 -v3637 v3481 -v3462 -v3299 -v1877 -v1229 -v524 v379 v259 v1881 v1350 v380 -v271 -v4298 v4266 -v4185 -v3990 v3484 v1349 -v1235 v396 -v4189 -v3991 v3939 v3482 v330 v3941 v3778 v1883 -v1357 v1240 -v633 v331 -v31 v3947 v1884 v1361 -v635 v332 -v35 -v4269 v3943 v1362 -v1241 v346 -v3952 v1363 -v1242 v631 -v4463 -v4151 -v3395 v3128 v3023 -v2678 -v2287 v1934 -v308 -v4153 v3129 v3028 -v2919 -v2291 -v1895 -v1494 -v4003 -v3124 v3024 v1938 -v1917 v1496 -v808 -v314 -v252 -v3036 -v2999 v1936 v1913 v1497 -v251 -v4306 -v4147 v4009 -v3392 -v3122 v3000 -v2402 -v2233 -v1912 v1513 v3001 v2406 -v2234 -v1055 v4312 -v4148 v4014 v3017 v2229 -v1761 -v1056 -v317 -v4383 -v2091 -v1765 v1057 v351 -v4404 -v4317 -v4017 -v2408 -v2227 -v2090 v1073 -v947 v353 -v248 -v4400 -v4015 -v2409 v1973 v359 -v4399 -v4320 -v3658 v2098 v1994 v1767 -v771 v355 -v4318 v3662 v3086 -v2102 -v1990 v1768 -v773 -v367 -v3107 v2106 -v1989 v3103 v2765 v2105 -v3286 v3102 v2786 -v767 -v3466 v2782 -v1779 v3292 v2781 -v1781 -v768 v3978 v1787 v3977 v3297 v1783 -v572 v3469 -v1871 v1795 -v576 -v4256 v3985 -v3633 v3471 v3300 -v1870 -v520 -v3989 v3477 v3298 v258 v4262 -v3993 -v3802 -v3636 v3473 -v1878 v578 -v526 -v399 v279 -v3992 v3485 v1882 -v1228 -v579 -v400 -v275 v4267 v4187 -v3774 v1886 -v1230 -v647 v395 -v274 -v4191 v1885 v1351 v1236 -v634 -v4270 v3777 v1352 v1232 -v529 v393 v349 -v33 -v4268 v3942 v1353 v1243 v350 -v37 -v4193 -v3960 v1367 v345 -v4194 -v3956 v629 -v4464 -v4152 -v3396 -v3126 v2289 v1935 -v1914 -v804 -v402 -v310 v3022 -v2396 -v2293 v1939 -v1916 v3044 -v2395 -v2232 -v1851 v1516 -v807 -v315 -v4002 v3040 -v2231 -v1855 -v1755 v1517 -v4361 -v4004 -v3123 v3039 v3020 v2403 -v2295 -v1910 -v1754 -v1512 -v318 -v4365 -v4305 v4010 v3021 v2407 -v2296 -v316 -v4401 v4307 -v4211 v4006 v3016 -v2654 v2411 -v1911 -v1762 -v1510 -v1076 -v943 -v4403 v4313 -v4215 v4018 -v2410 -v1766 -v1077 v4309 v3014 -v2228 v1991 v1770 -v1072 -v946 -v4321 -v2092 v1993 v1769 -v772 v354 -v4397 -v3657 -v3104 -v2093 -v1685 -v1070 v375 v3661 -v3106 v2094 -v1689 v371 -v4398 v2783 v2110 -v1987 -v1404 -v370 v2785 v3100 -v1988 v3285 -v566 v3287 v3101 v2779 v565 v3293 -v1782 v3289 -v2780 v1803 v573 -v516 v3979 v3301 v1799 -v577 v3980 -v3798 v3632 v1798 -v833 v581 -v522 -v398 v276 -v4255 -v4181 v3981 v3472 -v1872 v580 -v397 v278 -v4257 -v4180 v3997 -v3801 -v3638 -v3493 -v1873 -v643 -v527 v4263 v3489 v1874 -v27 v4259 v4188 -v3773 v3488 v1890 -v646 -v530 -v348 -v272 -v26 -v4271 -v4192 -v1231 -v528 -v347 -v4196 -v3957 v3779 -v3641 -v1370 -v1251 -v394 -v273 -v34 -v4195 -v3959 -v1371 -v1247 -v38 v1366 -v1290 -v1246 v343 -v219 -v39 -v3955 -v630 -v223 -v40 -v3133 -v3127 -v3041 v2290 v1947 -v1915 -v1515 v803 -v401 -v306 -v3137 v3043 v2294 v1943 v1514 -v311 -v3019 -v2298 -v1942 v1850 -v809 -v307 -v3018 v2397 -v2297 -v1854 -v319 -v4360 -v3037 v2650 v2398 -v1075 -v4402 -v4364 -v4005 v2399 -v1756 -v1074 -v4210 -v4026 -v3038 -v2653 v2415 -v1757 -v1511 -v942 -v812 v4308 -v4214 v4022 v1992 v1758 -v4329 v4021 -v3015 -v1774 v948 -v372 -v4325 -v3105 v374 -v4324 -v3659 v2113 -v1684 -v1400 -v1071 v3663 v2784 v2114 -v1688 v2109 -v1403 -v951 -v368 v3665 -v3595 -v2107 -v369 v3666 v1800 v3288 v1802 v567 v3628 v3309 -v829 v568 -v3305 v569 -v515 v277 v4000 -v3797 v3634 -v3490 -v3304 -v1796 -v832 -v585 -v517 v4001 -v3492 -v523 -v3996 v3803 -v3769 -v3639 -v1893 -v1797 -v642 -v519 -v4258 -v4182 v1894 -v531 -v4279 -v4183 -v3994 -v3775 v3642 -v3486 v2982 v1889 -v1425 -v1369 -v1248 -v648 -v4275 v4184 -v3958 -v3640 v1429 -v1368 -v1250 v28 -v4274 -v4200 -v3806 v3780 -v3487 -v1887 -v1286 v29 v30 v3781 -v3274 v1364 -v1289 -v1244 -v651 v344 -v218 v44 -v3953 v3782 -v3278 -v222 -v3132 -v3042 -v2286 v1946 v805 -v403 -v3136 v2285 -v305 v2302 -v1940 v1852 -v810 -v327 -v1856 -v323 -v4362 -v4023 v2649 -v2418 -v1941 v938 -v813 v407 -v322 v4366 -v4025 v2419 -v811 -v4326 v4212 -v2655 -v2414 -v2071 -v1858 v1777 v944 -v4328 v4216 -v3653 v2075 -v1859 v1778 -v373 -v4368 v4019 -v3652 -v2412 -v2112 -v1773 v1138 v949 -v4369 -v2111 -v4322 -v4218 v4020 v3660 -v3333 -v2658 -v1771 -v1686 -v1399 -v952 -v4219 v3664 -v3337 -v1690 -v950 -v4323 v3668 -v3591 v2001 v1405 v3667 -v2005 v4415 -v3594 -v2108 -v1692 v1801 -v1693 v3306 -v1408 v3308 v3999 -v3793 -v828 v588 v3998 v3627 -v3491 v589 -v3845 -v3799 v3629 -v3302 -v1892 -v1664 -v834 v638 -v584 -v3849 v3635 -v1891 -v518 -v4276 v3804 v3631 -v3303 -v2978 -v644 -v582 -v539 -v4278 v3768 v3643 -v1249 -v535 -v4203 -v3995 -v3807 v3770 v2981 -v1424 -v837 -v649 -v534 -v4204 -v3805 v3776 v1428 -v4272 -v4199 v3772 -v1888 -v1285 v736 -v652 -v47 v3783 -v650 v48 -v4273 -v4197 -v3273 -v1365 -v1291 -v1245 -v220 v43 -v3954 v3277 -v224 -v3134 v2305 v1944 -v1847 -v801 v404 -v324 -v4356 -v3138 v2306 v806 -v326 -v4355 -v3253 -v2645 -v2417 v2301 v1853 v802 v408 v4206 -v4024 -v2416 -v1857 -v814 v406 v4363 v4205 -v3140 v2651 v2299 -v2270 v1861 -v1776 -v320 v4367 -v4327 -v3141 v1860 v1775 v937 -v4371 v4213 -v3230 -v2656 -v2070 -v1134 v939 -v918 -v321 -v4370 v4217 v2074 -v1680 v945 -v922 -v4221 -v2659 -v2539 -v2413 -v1679 -v1395 v1137 -v1088 v941 -v4220 -v3654 -v2657 -v2543 -v953 -v3655 -v3332 -v1772 -v1687 -v1401 -v1334 v3656 -v3336 v1691 -v4411 -v3672 v3590 v2000 -v1695 v1406 -v2004 -v1694 v4414 -v3596 v2928 -v1409 v3307 -v2932 -v1407 v4161 -v824 v587 -v4165 v586 -v3599 -v2313 -v1660 -v830 -v3792 -v2317 -v3844 -v3794 -v1663 -v835 -v536 -v4277 -v3848 -v3800 v3630 v637 -v538 -v4597 -v4202 v3796 v3651 -v2977 v838 v639 -v583 -v4601 -v4201 -v3808 v3647 -v836 v645 -v3646 v2983 -v1426 -v1281 -v732 v641 -v532 -v286 -v131 -v46 v3771 v1430 v653 -v290 -v214 -v45 -v3791 -v1287 v735 -v533 -v213 -v3787 -v4198 -v3786 -v3275 -v2986 v1432 v1292 -v221 -v41 v3279 v1433 -v225 v3249 -v3135 v2303 v1945 v405 -v325 -v3139 -v1846 v800 v409 -v3252 -v3143 -v2266 -v1848 v822 -v4357 -v3142 -v2644 v1849 v818 -v4358 v3226 -v2646 v2300 -v2269 v1865 v817 v4359 v4207 v2652 v4375 v4208 -v3229 v2648 -v2072 -v1133 -v1084 -v917 v4209 -v2660 v2076 v940 -v921 v4225 -v2538 -v1330 v1139 -v1087 -v961 -v2542 -v1681 -v1394 v957 -v4527 -v3675 -v3586 -v3334 -v2078 v1682 -v1396 -v1333 -v956 -v3676 -v3338 -v2079 v1683 -v1402 -v4410 -v3671 v3592 v2002 v1699 v1398 -v1142 -v984 -v2006 -v1410 v988 v4416 -v3669 -v3597 -v3504 -v3340 v2927 -v3341 -v2931 v4160 v3600 -v2195 -v2008 -v4164 -v3598 -v2009 -v823 -v4419 -v2312 -v1659 -v825 -v2316 v831 -v537 v3846 -v3648 -v2973 -v2430 -v1665 v827 -v3850 -v3795 v3650 -v1420 v839 -v4596 -v3816 v2979 -v1419 -v127 -v4600 -v3812 v640 -v3852 -v3811 -v3788 -v3644 v2984 -v1668 v1427 -v731 v661 -v285 -v130 -v3853 -v3790 -v3269 v1431 -v1280 v657 -v289 -v3645 -v3268 -v2987 v1435 -v1282 v737 v656 -v2985 v1434 v1288 -v215 -v3784 -v3276 -v2030 v1284 -v216 -v42 v3280 v1293 -v217 v3248 -v3131 v2304 v1805 -v819 -v417 -v3130 v821 -v413 -v3254 -v3147 -v2265 -v1868 -v412 v2066 -v1869 -v4378 v3225 -v2271 v2065 -v1864 -v1129 -v815 -v4379 -v2647 v4374 -v4228 -v3257 -v3231 -v2668 -v2073 -v1862 v1135 -v1083 -v958 v919 -v816 -v4229 -v3328 v2664 v2077 -v960 v923 -v4523 -v4372 v4224 -v3674 -v3327 v2663 -v2540 -v2274 v2081 -v1329 v1140 v1089 -v3673 -v2544 v2080 -v1996 -v4526 -v4406 -v4222 v3335 v3234 -v1995 -v1702 v1335 -v1143 -v954 -v925 -v3585 v3339 -v1703 -v1397 -v1141 -v926 -v4412 -v3587 -v3500 -v3343 -v2546 -v2514 v2003 v1698 v1418 -v1092 -v983 -v955 v3593 -v3342 -v2547 v2518 -v2007 -v1414 v987 v4417 -v3670 v3589 -v3503 v2929 -v2191 -v2011 -v1696 -v1413 -v1338 v3601 v2933 -v2010 v4420 v4162 -v2194 -v1655 -v471 v4418 v4166 v3840 -v475 v3839 v2935 -v2426 -v2314 -v1661 -v3649 v2936 -v2318 -v826 -v4168 v3847 -v3813 -v2429 v1666 -v847 -v4169 v3851 -v3815 -v2972 v843 -v4598 -v3855 v2974 v2320 -v2170 -v1669 -v842 -v727 v658 -v126 -v4602 -v3854 -v3789 v2980 -v2321 -v1667 v1421 v660 -v3809 v2976 v1422 v733 -v287 -v132 -v2988 v1423 -v291 -v4604 -v3810 -v2026 v1439 v738 v654 -v4605 -v3270 -v1283 -v3785 -v3271 v2125 -v2029 -v1301 -v739 -v655 v293 -v228 -v135 v3272 v1297 -v740 -v294 -v229 v3250 -v3150 v2261 -v1867 v1804 -v820 -v416 -v3151 -v1866 -v4377 v3255 v3221 -v3146 -v2267 -v876 -v410 -v4376 -v913 -v880 -v4227 -v3258 v3227 -v3144 -v2665 v2272 -v1079 -v912 -v411 -v4226 -v3256 -v2667 -v2534 v2067 -v1128 -v959 v3232 -v2793 -v2533 -v2275 v2068 -v1863 -v1325 -v1130 -v1085 v920 -v785 -v2797 -v2273 v2069 v1136 v924 -v4522 -v4373 v3235 v2661 -v2541 v2085 -v1701 -v1331 v1132 v1090 v928 -v3329 v3233 -v2545 -v1700 v1144 v927 -v4528 -v4223 v3330 -v2662 -v2549 -v1415 v1336 -v1093 -v4405 v3331 v2923 -v2548 v1997 -v1417 -v1091 v4407 -v3499 -v3347 v2922 -v2513 v1998 -v1339 -v985 -v4413 -v4156 -v3588 v2517 v1999 -v1337 v989 -v4531 v4409 -v4155 v3609 v3505 v2930 -v2190 v2015 -v1697 -v1411 v4421 v3605 v2934 -v2308 v4163 -v3604 v2938 -v2307 -v2196 -v1412 -v991 -v470 v4167 v2937 -v1654 -v992 -v474 v4171 -v3508 -v2425 -v2315 -v1656 -v844 -v4592 v4170 v3841 -v3814 -v2319 -v1662 -v846 -v4591 v3842 -v3683 -v2431 v2323 -v2199 -v2166 -v1831 v1658 -v122 v3843 v3687 v2322 -v1670 v659 -v281 -v4599 -v3859 -v3055 v2169 -v840 -v280 -v128 -v4603 v2975 v726 -v4607 -v2996 -v2434 -v1442 -v841 v728 -v288 v133 -v4606 -v2992 -v1443 v734 v292 -v2991 -v2121 -v2025 v1438 -v1298 v730 v296 -v227 v136 -v55 -v1300 v741 v295 -v226 v134 -v59 -v3283 v2124 -v2031 v1436 -v3284 v1296 -v3246 -v3148 v1806 v710 -v414 v3251 v2260 v3247 v2262 -v875 -v3259 v3220 -v2666 -v2268 -v879 v3222 -v3145 v2264 v1810 v781 v3228 -v2276 -v1078 -v914 -v4518 -v4058 v3224 -v2792 -v2088 v1080 v915 -v784 v3236 -v2796 -v2535 -v2089 -v1324 -v1131 -v1086 v916 -v4524 -v2536 v2084 v1326 v1152 v1082 v932 -v2537 -v1416 -v1332 -v1148 -v1094 -v979 v4529 -v3495 v3350 -v2553 v2082 v1328 -v1147 v978 v3351 v1340 -v4532 -v3606 -v3501 -v3346 v2515 -v2186 v2018 -v986 -v4530 v4408 -v3608 v2924 v2519 v2019 v990 -v4429 v3506 -v3344 v2925 -v2192 v2014 -v994 v4425 v4157 v2926 -v993 v4436 v4424 v4158 -v3602 -v3509 v2942 -v2521 -v2421 -v2197 -v2012 v472 -v4440 v4159 -v3507 -v2522 v2309 -v845 -v476 -v4175 -v3603 -v2427 v2310 -v2200 -v1827 v2311 -v2198 v1657 -v3862 -v3682 -v3051 -v2432 v2327 -v2165 -v1830 -v1714 v1678 -v1209 v478 -v4593 -v3863 v3686 v1674 -v1213 -v479 v121 -v4594 -v3858 -v3054 -v2993 -v2435 v2171 v1673 -v1441 v123 -v4595 -v2995 -v2433 -v1440 -v282 -v129 -v4611 -v3856 -v2021 v283 v125 -v1299 v729 v284 v137 -v3282 -v2989 -v2174 -v2120 -v2027 v749 v300 v54 -v3281 -v745 -v58 -v2990 -v2582 v2126 v2032 v1437 -v744 v1294 -v3149 v1807 -v1305 v709 -v415 v3245 -v1309 -v3267 v1811 -v877 v3263 v2263 v1809 -v881 -v4054 -v3262 v2284 -v2087 v780 v3223 v2280 -v2086 -v4057 -v3550 v3244 -v2794 -v2279 v1149 -v935 -v883 -v786 -v4517 -v3554 v3240 -v2798 v1151 v1081 -v936 -v884 -v4519 -v3349 v3239 -v2556 v1102 v931 v4525 -v3348 -v2557 -v2509 v1327 v1098 v4521 -v2800 -v2552 v2508 v2083 -v2017 -v1348 -v1145 v1097 v929 -v789 v4533 -v3607 -v3494 -v2801 -v2016 -v1344 v980 -v4426 -v3496 -v2550 v2516 -v1343 -v1146 v981 -v4428 -v3502 v2520 -v2185 v982 -v466 v3498 -v3345 -v2953 -v2945 -v2524 v2187 -v998 -v465 -v3510 -v2957 -v2946 -v2523 -v2193 v4435 v4422 -v4178 v2941 -v2604 -v2451 v2189 -v2013 v473 -v4439 -v4179 -v2455 -v2420 -v2201 -v477 v4423 -v4236 -v4174 -v3861 -v3728 -v2939 -v2422 -v2330 -v2161 -v1826 v1710 -v1675 v481 -v4240 -v3860 -v2428 -v2331 -v1677 v480 -v4172 -v3684 -v3050 -v2424 v2326 v2167 v1832 -v1713 -v1208 v3688 -v2994 -v2436 -v1212 -v4614 -v4336 -v3529 -v3056 -v2324 v2172 -v1671 -v4615 -v4340 v124 -v4610 -v3857 v3690 -v2175 -v2116 -v1835 -v1672 v746 -v596 -v303 v145 v3691 -v2173 -v2020 v748 v600 -v304 -v141 -v4608 -v3059 -v2578 v2122 -v2022 -v299 -v140 v56 -v2028 -v60 v2581 v2127 v2024 -v742 -v297 v2033 v1295 -v3264 v1808 -v1304 -v872 v711 -v3266 v1812 -v1308 -v2281 -v878 v776 -v2788 v2283 -v882 -v4053 -v3260 -v3241 -v2787 -v934 -v886 v782 -v715 v3243 v1150 -v933 -v885 -v4059 -v3549 -v3261 -v2795 -v2555 -v2277 -v1184 -v1099 v787 -v3553 -v2799 -v2554 v1188 v1101 v3237 v2803 -v2278 -v1345 -v790 -v4520 v2802 -v1347 -v788 -v4541 -v4062 v3238 v1095 v930 v4537 -v4427 v2510 -v4552 v4536 -v2944 -v2551 v2511 -v1341 v1096 -v1001 v3497 -v2943 v2512 -v1002 -v4177 v3518 -v2952 -v2600 -v2528 -v1342 -v997 -v156 -v4176 -v3514 v2956 v2188 -v467 v4437 -v3724 -v3513 -v2603 v2450 -v2356 -v2329 v2209 -v1822 -v995 -v468 -v4441 -v3678 -v2454 -v2360 -v2328 -v2205 -v1676 v469 -v4235 v3727 -v3677 -v3046 -v2940 -v2709 -v2204 -v1828 v1709 v485 v4239 -v2713 -v2423 -v2160 -v4613 -v4443 -v4173 -v3685 -v3525 -v3052 -v2444 -v2162 v1833 -v1715 -v1210 -v4612 -v4444 v3689 -v2440 v2168 -v1214 v4335 v3693 -v3528 -v3057 -v2439 -v2325 v2164 -v1836 -v1479 -v302 v142 -v4339 v3692 v2176 -v1834 v747 -v301 v144 -v50 v3060 -v1718 -v1216 -v595 -v550 -v49 -v3058 -v2115 -v1217 v599 -v4609 -v2577 -v2117 -v138 v57 v2123 v2023 -v61 v2583 v2119 v2041 -v743 -v298 -v139 v62 -v2128 v2037 v63 -v3265 v1820 v1306 v712 -v2282 v1816 v1310 -v871 -v4049 v1815 -v873 v716 -v3242 -v874 v775 v714 v4055 v1312 -v890 v777 -v2789 v1313 -v1100 v783 -v4060 v3551 -v2790 v1183 v779 -v3555 v2791 -v1346 v1187 -v791 -v4538 -v4063 -v2807 -v4540 -v4061 -v4548 v3557 -v1524 -v1000 -v3558 -v1528 -v999 v4551 -v4534 v3515 -v2531 -v1599 v152 -v4431 v3517 v2532 -v4535 -v4430 v2954 -v2625 -v2599 -v2527 -v2206 -v155 v2958 -v2629 -v2208 v4438 -v3723 -v3511 -v2605 -v2525 v2452 -v2355 -v1705 -v996 v488 -v4442 -v2456 -v2359 -v1821 -v1204 v489 v4446 v4237 v3729 -v3512 -v2960 -v2708 -v2441 -v2202 -v1823 v1711 -v1203 -v484 -v4445 v4241 -v3679 -v3045 -v2961 -v2712 -v2443 -v1829 -v3680 -v3524 -v3047 -v2860 -v2608 -v2458 -v2203 v1825 -v1716 -v1475 v1211 -v482 v3681 v3053 -v2459 -v2163 -v1837 -v1215 -v143 v4337 -v4243 -v3732 v3697 v3530 v3049 -v2437 -v2184 -v1719 -v1478 v1219 -v546 -v4341 -v4244 v3061 -v2180 -v1717 v1218 -v2573 -v2438 -v2179 v597 -v549 v601 -v51 -v4343 v3533 -v2579 -v2038 -v52 -v4344 -v2118 v2040 v53 v2584 v2136 -v901 -v603 v67 v2132 v2036 -v905 -v604 -v2731 v1819 v1307 v713 -v2735 v1311 v717 -v1813 v1315 -v893 -v4048 -v3545 v1314 -v894 -v4050 -v3544 -v1814 -v889 v4056 v778 v4052 v3552 -v2810 v1185 -v887 v799 -v4539 -v4064 -v3556 -v2811 v1189 v795 v3560 -v2806 v794 v3559 -v4547 -v2804 -v2530 v1595 -v1523 -v1191 v3516 -v2948 -v2529 -v1527 -v1192 v4553 -v4502 -v2947 -v2595 -v1598 v151 -v2446 -v2207 -v3719 v2955 v2624 -v2601 -v2445 v487 -v157 -v4432 -v4231 v2959 -v2628 v486 -v4556 -v4433 v4230 -v3870 -v3725 -v2963 -v2606 -v2526 v2453 -v2357 v4434 -v3874 -v2962 -v2457 -v2442 -v2361 -v1704 -v4450 v4238 v3730 -v3520 -v2856 -v2710 -v2609 -v2461 v1706 -v160 -v4331 v4242 -v2714 -v2607 -v2460 v1824 v1712 v1205 -v4330 -v4246 -v3733 -v3700 -v3526 -v2859 -v2363 -v2181 -v1845 v1708 v1474 v1206 -v1113 -v483 -v4245 -v3731 v3701 v3048 -v2364 -v2183 -v1841 -v1720 v1207 v591 v4338 -v3696 v3531 -v3069 -v2716 -v1840 -v1480 -v1223 v590 -v545 -v4342 -v3065 -v2717 v4346 -v3694 v3534 -v3064 -v2177 -v1159 v598 -v551 -v4345 v3532 -v2572 -v2039 -v1163 v602 v2574 -v2178 -v2143 -v2133 -v1483 v606 -v70 -v2580 -v2147 v2135 v605 v71 v2576 -v900 v697 -v554 v66 -v2585 v2131 v2034 -v904 -v2730 -v2684 v1817 v1303 -v892 v725 -v2734 v2688 v1302 -v891 v721 -v2050 -v1548 v1319 v720 v1552 -v1179 -v2809 -v1178 v796 -v4051 -v3546 -v2808 v798 -v4072 v3547 v1186 -v888 -v4068 v3548 v1190 -v4543 -v4067 v3564 -v1194 v792 -v1193 v4549 -v4498 -v2805 v1594 -v1525 v793 -v147 -v1529 v4554 -v4501 -v1600 v153 -v2949 -v2594 -v2351 -v4557 -v4473 v2950 v2626 -v2596 -v2350 -v1531 -v158 -v4555 -v4477 -v3718 v2951 -v2704 -v2630 -v2602 v2447 -v1532 -v4453 -v3869 -v3720 -v2967 -v2703 -v2598 v2448 v2358 -v1603 -v161 -v4454 v4232 -v3873 v3726 -v2610 v2449 -v2362 -v159 -v4449 v4233 v3722 -v3699 -v2855 -v2711 -v2632 -v2465 -v2366 -v1842 -v1470 -v1109 v4234 -v3734 -v3698 v3519 v2715 -v2633 -v2365 -v2182 -v1844 v1707 -v4447 v4250 v3521 -v3066 v2861 -v2719 -v1728 v1476 -v1226 -v1112 -v541 -v4332 -v3527 -v3068 -v2718 -v1724 v1227 v4333 v3523 -v1838 -v1723 v1481 -v1222 -v547 v4334 v3535 v592 -v4350 -v3695 -v3409 -v3062 -v2864 -v1839 v1484 -v1220 -v1158 v593 -v552 -v69 -v2134 v1482 v1162 v594 -v68 -v3063 -v2476 -v2142 v693 -v610 v555 v2575 -v2480 -v2146 -v553 -v3616 v2593 -v902 v696 v64 -v3620 -v2589 v2129 v2035 -v906 -v3820 -v2732 -v2683 -v2046 v1818 v1322 v724 v3824 -v2736 v2687 v1323 -v3201 -v2049 -v1547 v1318 -v718 v3205 v1551 -v797 -v4069 -v2738 -v1316 -v719 -v4071 -v2739 v1180 -v3567 -v2241 v1181 -v3568 -v2245 v1519 v1182 -v4065 v3563 -v1590 v1518 v1198 -v4542 -v4544 -v4497 -v4066 v3561 v1596 v1526 -v500 v4550 -v2620 v1530 -v146 v4546 -v4503 -v2619 -v1601 v1534 v148 v4558 -v1533 v154 -v4472 -v4452 -v2970 v2627 v1604 v150 -v4476 -v4451 -v2971 -v2631 -v2597 v2352 v1602 v162 -v4506 -v3871 -v2966 -v2851 v2635 -v2618 -v2468 v2353 v3875 -v3721 -v2705 -v2634 -v2614 -v2469 v2354 -v1843 -v4253 v3742 -v3362 -v2964 -v2857 -v2706 -v2613 -v2464 v2370 -v1725 -v1225 -v1108 -v4254 v3738 -v3067 v2707 -v1727 -v1469 -v1224 -v4448 -v4249 -v3877 v3737 v2862 -v2723 -v2462 -v1471 -v1114 -v3878 v3522 v1477 -v540 -v4353 -v4247 -v3543 v3405 -v2865 -v1721 v1473 -v542 v4354 -v3539 -v2863 v1485 -v548 -v4349 -v3538 -v3408 -v1722 -v1221 -v1160 v1117 v613 v544 v1164 -v896 v614 v556 -v4347 -v2590 -v2475 -v2144 v895 v692 -v609 v2592 -v2479 -v2148 -v3615 v1166 -v903 v698 -v607 v65 -v3619 -v2588 -v2130 v1167 -v907 -v3819 -v2733 v2685 -v2045 v1320 v722 v3823 -v2737 v2689 -v3200 v2741 -v2051 -v1549 -v856 -v4070 v3204 v2740 v1553 -v3566 -v2691 -v1317 -v3565 -v2692 -v2240 -v2054 v1555 v1201 -v2244 v1556 v1202 -v4493 v1197 -v496 -v1589 v1520 v4499 -v3562 v1591 v1521 v1195 -v499 -v4545 v1597 v1522 -v4566 -v4504 -v3753 -v2969 v1593 v1538 v4562 -v3865 -v2968 -v2621 v1605 v149 v4561 -v4507 -v4474 -v3864 v2622 -v2615 -v2467 -v450 -v170 -v4505 -v4478 v2623 -v2617 -v2466 -v166 -v4252 v3872 v3739 -v3358 -v2639 v2373 -v1104 -v165 -v4251 v3876 v3741 -v2850 v2374 -v1726 -v4480 -v3880 -v3361 -v2965 v2852 v2726 -v2611 -v2369 -v1110 -v4481 -v3879 -v2858 v2727 -v4352 -v3735 -v3540 v2854 -v2722 -v2612 -v2463 -v2367 -v1735 v1115 -v4351 -v3542 -v2866 v1739 -v1472 -v1154 -v4248 -v3736 v3404 -v2720 -v1493 -v1153 v1118 -v612 v2138 -v1489 v1116 v611 -v543 -v3536 -v3410 -v2822 v2137 -v1488 -v1161 -v688 -v564 -v2591 v1165 v560 -v4348 -v3537 -v2477 -v2145 v1169 v694 -v559 -v2481 -v2149 v1168 v897 -v3617 -v3413 -v2150 v898 v699 -v608 v3621 -v2586 -v2151 v899 -v4030 v3821 v2729 v2686 -v2047 -v1544 -v1321 -v852 v723 -v4034 v3825 v2728 v2690 -v3202 v2745 v2694 v2052 -v1550 -v855 v3206 -v2693 v1554 -v3827 v2055 v1558 v1200 -v3828 v2053 v1557 v1199 -v3208 v2242 -v3209 v2246 -v495 v4492 -v4563 v4494 -v3749 -v2248 v1541 v1196 -v501 -v4565 v4500 -v4468 -v2249 v1592 v1542 -v4577 v4496 -v4467 -v3752 v1613 v1537 -v446 -v167 v4508 -v2616 -v1609 -v169 v4559 v4475 -v2642 -v2372 -v1608 v1535 -v504 v449 v4479 -v3866 -v3740 -v2643 v2371 -v4560 v4483 v3867 -v3357 -v2725 -v2638 -v163 -v4482 v3868 -v2724 -v1103 -v3884 v3363 -v2636 v1105 -v164 -v3541 v2853 v1111 v3400 v2874 -v2368 -v1734 -v1490 v1107 -v2870 v1738 -v1492 v1119 v3406 -v3366 -v2869 -v2818 -v2721 -v561 -v107 -v2471 -v1155 -v563 -v4097 -v3411 -v2821 -v2470 -v1486 -v1156 -v4101 -v3611 v2139 v1157 -v687 -v3610 -v3414 v2478 v2140 -v1487 v1173 -v689 -v557 -v3412 -v2482 v2141 v695 -v3618 -v2483 v2155 v910 v691 -v558 v3622 -v2587 -v2484 v911 v700 -v4029 v3822 -v3197 v2751 v2748 -v2682 -v2043 -v851 -v4033 v3826 v2749 v2681 -v2048 -v1543 v3830 -v3203 v2744 v2698 v2044 -v1545 -v857 -v3829 v3207 -v2236 v2056 v1546 v3211 -v2742 -v2235 v1562 -v3210 v2243 v860 -v491 v2247 v2251 v1540 -v497 -v4564 v2250 v1539 -v4573 -v3748 v1610 v1378 -v502 v4495 v1612 -v1382 -v168 -v4576 v4516 -v3754 -v2641 -v505 -v445 v4512 v4469 -v2640 -v503 v4511 v4470 -v3353 -v1606 v1536 v451 v4471 v4487 -v3887 -v3757 v3359 -v1607 v3888 -v3883 v3364 v2871 -v2637 -v454 -v424 v2873 -v1491 v1106 -v428 -v3881 -v3434 v3367 -v1736 -v1127 -v103 v3399 -v3365 v1740 v1123 -v562 v3401 -v3162 -v2867 -v2817 v1122 -v106 v3407 -v4096 v3403 -v2868 -v2823 -v1742 v1176 -v4100 -v3415 v2472 -v1743 v1177 v2473 v2158 v1172 -v909 -v3612 v2474 v2159 -v908 -v690 v3712 -v3613 -v2826 -v2488 v2154 -v1170 v708 v3614 -v704 -v4031 v3818 v2750 v2746 -v2701 -v853 -v4035 v3817 -v3196 -v2702 -v2042 -v3834 -v3198 v2697 -v2064 v1565 -v858 v3199 v2060 v1566 v4037 v3215 -v2743 -v2695 -v2059 -v1926 v1561 v861 v4038 -v2237 v859 v2501 -v2238 v1559 v2239 -v490 v3744 v2255 -v492 v1611 -v498 -v4572 v4513 -v3750 v1377 -v1257 -v494 -v441 v4515 -v1381 -v506 -v4578 -v3755 -v447 v4509 v4490 -v3886 -v3758 v452 v4491 -v3885 -v3756 -v3352 -v4581 v4510 v4486 v3354 v455 v3360 -v2872 v1730 -v453 v4484 -v3430 v3356 v1729 -v1124 -v423 v3368 -v1126 v427 -v3882 -v3433 -v3158 v2813 v1737 -v102 v1741 v3161 -v2819 -v1745 -v1175 v1120 -v108 v3402 -v1744 -v1174 -v4098 v3423 v2824 -v2157 v1121 -v971 -v4102 -v3419 v2156 -v3967 v3708 -v3418 v2827 v2491 -v705 -v111 -v3971 -v2825 v2492 -v707 v4104 v3711 v3625 -v2846 -v2487 -v2152 -v1171 v4105 v3626 -v703 v4032 -v3837 v2752 v2747 -v2699 -v2061 -v1564 -v849 -v4036 v3838 -v2063 -v1563 -v854 v4040 -v3833 v3218 v1922 v850 v4039 v3219 v862 -v3831 v3214 -v2756 -v2696 -v2497 -v2057 -v1925 -v3212 v2500 -v2258 -v2058 v1560 -v2259 -v4568 -v2254 v1253 v4514 v3743 -v493 -v4574 v3745 -v2252 v1379 -v1256 -v514 v3751 -v1383 -v510 v440 -v4579 -v4489 v3747 -v509 v442 -v4488 v3759 v448 -v4582 v1385 v444 -v4580 v1386 v456 v3355 -v1125 -v4485 v3429 v3376 -v425 -v98 -v3372 v1731 v429 -v3435 -v3371 -v3157 v1732 -v104 -v4092 v2812 v1733 -v4091 v3420 v3163 v2814 v1749 -v967 -v431 v109 v3422 -v2820 -v432 -v4099 -v3438 v2816 v2490 -v970 -v112 -v4103 v2828 v2489 -v706 -v110 v4107 -v3966 v3707 -v3624 -v3416 -v3166 -v2842 v4106 v3970 -v3623 v3713 -v3417 -v2845 -v2485 -v2153 -v701 -v4028 -v3835 v3217 v2753 -v2700 -v2062 v4027 v3216 -v848 v4044 -v2757 v1921 v870 -v2755 v866 -v3832 -v2496 -v2257 -v1927 v865 -v2256 -v3213 v2502 v1373 -v1930 v1372 v1252 -v511 -v4567 -v513 -v4569 v2505 -v2253 v1380 v1258 -v4575 v3746 v1384 -v4571 v3767 v1388 -v507 -v4583 -v3763 v1387 v443 -v3762 v1261 -v508 v464 v460 v419 v3425 v3373 v459 v418 v3375 v3431 v3153 -v426 v430 -v97 -v3436 -v3369 -v3159 v1752 -v434 v99 v3421 v1753 -v433 -v105 -v3439 -v3370 v3164 v1748 -v966 v101 -v4093 -v3437 v2815 -v113 -v4094 v3703 -v3167 -v2836 v1746 -v972 v4095 -v3165 v2832 -v4111 -v3968 v3709 -v2841 v2831 v3972 v3714 -v2847 -v2486 v975 -v702 -v4045 -v3836 v2754 v1920 v867 -v4047 -v2758 v869 v4043 -v2495 v1923 v4041 v2498 -v1928 v863 v2503 v864 -v1929 -v512 v2506 v1254 v2504 v1374 -v3764 v1375 v1259 -#### 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.84 0.94 0.90 2/54 22301
Raw data (stat): 22301 (runsolver) R 22300 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479865856 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.0001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 2567 0 0 0 991 5 0 0 25 0 1 0 479865856 12996608 2534 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3173 2534 603 41 0 3132 0
vsize: 12692
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4021 0 0 0 1988 9 0 0 25 0 1 0 479865856 19591168 3887 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4783 3887 603 41 0 4742 0
vsize: 19132
[startup+30.0023 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4148 0 0 0 2987 10 0 0 25 0 1 0 479865856 20156416 4014 4294967295 134512640 134672761 3221224544 3221223724 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4921 4014 603 41 0 4880 0
vsize: 19684
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4201 0 0 0 3986 10 0 0 25 0 1 0 479865856 20422656 4067 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4986 4067 603 41 0 4945 0
vsize: 19944
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4249 0 0 0 4985 10 0 0 25 0 1 0 479865856 20557824 4115 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5019 4115 603 41 0 4978 0
vsize: 20076
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4297 0 0 0 5984 11 0 0 25 0 1 0 479865856 20828160 4163 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5085 4163 603 41 0 5044 0
vsize: 20340
[startup+70.003 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4403 0 0 0 6985 11 0 0 25 0 1 0 479865856 21061632 4243 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5142 4243 603 41 0 5101 0
vsize: 20568
[startup+80.0039 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4440 0 0 0 7985 11 0 0 25 0 1 0 479865856 21458944 4280 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5239 4280 603 41 0 5198 0
vsize: 20956
[startup+90.0037 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4475 0 0 0 8985 11 0 0 25 0 1 0 479865856 21458944 4315 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5239 4315 603 41 0 5198 0
vsize: 20956
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4536 0 0 0 9984 11 0 0 25 0 1 0 479865856 21729280 4376 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5305 4376 603 41 0 5264 0
vsize: 21220
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4603 0 0 0 10984 12 0 0 25 0 1 0 479865856 21995520 4443 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4443 603 41 0 5329 0
vsize: 21480
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4675 0 0 0 11984 12 0 0 25 0 1 0 479865856 22261760 4515 4294967295 134512640 134672761 3221224544 3221223648 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5435 4515 603 41 0 5394 0
vsize: 21740
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 4769 0 0 0 12983 12 0 0 25 0 1 0 479865856 22667264 4609 4294967295 134512640 134672761 3221224544 3221223668 134566024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5534 4609 603 41 0 5493 0
vsize: 22136
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 5022 0 0 0 13983 13 0 0 25 0 1 0 479865856 23609344 4862 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5764 4862 603 41 0 5723 0
vsize: 23056
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 5228 0 0 0 14982 14 0 0 25 0 1 0 479865856 24682496 5068 4294967295 134512640 134672761 3221224544 3221223744 134557965 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6026 5068 603 41 0 5985 0
vsize: 24104
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 5362 0 0 0 15982 15 0 0 25 0 1 0 479865856 25219072 5202 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5202 603 41 0 6116 0
vsize: 24628
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 5544 0 0 0 16982 15 0 0 25 0 1 0 479865856 26025984 5384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6354 5384 603 41 0 6313 0
vsize: 25416
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 6139 0 0 0 17980 17 0 0 25 0 1 0 479865856 28442624 5979 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6944 5979 603 41 0 6903 0
vsize: 27776
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 6832 0 0 0 18978 19 0 0 25 0 1 0 479865856 31133696 6672 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 6672 603 41 0 7560 0
vsize: 30404
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 7339 0 0 0 19976 20 0 0 25 0 1 0 479865856 33292288 7179 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8128 7179 603 41 0 8087 0
vsize: 32512
[startup+210.005 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 7945 0 0 0 20974 23 0 0 25 0 1 0 479865856 35713024 7785 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8719 7785 603 41 0 8678 0
vsize: 34876
[startup+220.005 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 8537 0 0 0 21973 24 0 0 25 0 1 0 479865856 38125568 8377 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9308 8377 603 41 0 9267 0
vsize: 37232
[startup+230.005 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 8705 0 0 0 22973 25 0 0 25 0 1 0 479865856 38797312 8545 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9472 8545 603 41 0 9431 0
vsize: 37888
[startup+240.005 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 8998 0 0 0 23972 26 0 0 25 0 1 0 479865856 40009728 8838 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9768 8838 603 41 0 9727 0
vsize: 39072
[startup+250.006 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 9361 0 0 0 24970 27 0 0 25 0 1 0 479865856 41881600 9201 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10225 9201 603 41 0 10184 0
vsize: 40900
[startup+260.006 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 9627 0 0 0 25969 29 0 0 25 0 1 0 479865856 42958848 9467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10488 9467 603 41 0 10447 0
vsize: 41952
[startup+270.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 10208 0 0 0 26968 30 0 0 25 0 1 0 479865856 45371392 10048 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11077 10048 603 41 0 11036 0
vsize: 44308
[startup+280.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 11323 0 0 0 27965 33 0 0 25 0 1 0 479865856 49913856 11163 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12186 11163 603 41 0 12145 0
vsize: 48744
[startup+290.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 11950 0 0 0 28964 35 0 0 25 0 1 0 479865856 52477952 11790 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 11790 603 41 0 12771 0
vsize: 51248
[startup+300.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 12324 0 0 0 29962 37 0 0 25 0 1 0 479865856 53944320 12164 4294967295 134512640 134672761 3221224544 3221223712 134560788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13170 12164 603 41 0 13129 0
vsize: 52680
[startup+310.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 12826 0 0 0 30961 37 0 0 25 0 1 0 479865856 55959552 12666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13662 12666 603 41 0 13621 0
vsize: 54648
[startup+320.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 12940 0 0 0 31961 38 0 0 25 0 1 0 479865856 56365056 12780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13761 12780 603 41 0 13720 0
vsize: 55044
[startup+330.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13009 0 0 0 32961 38 0 0 25 0 1 0 479865856 56635392 12849 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13827 12849 603 41 0 13786 0
vsize: 55308
[startup+340.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13106 0 0 0 33961 38 0 0 25 0 1 0 479865856 56840192 12895 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12895 603 41 0 13836 0
vsize: 55508
[startup+350.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13106 0 0 0 34961 38 0 0 25 0 1 0 479865856 56840192 12895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12895 603 41 0 13836 0
vsize: 55508
[startup+360.008 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 35961 38 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+370.009 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 36961 38 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+380.009 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 37961 38 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+390.009 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 38961 38 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+400.009 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 39962 38 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+410.009 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 40962 38 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+420.01 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 41962 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+430.01 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 42962 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+440.01 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 43962 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+450.01 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 44962 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+460.01 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 45962 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+470.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 46963 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+480.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 47963 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+490.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 48963 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+500.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 49963 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+510.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 50963 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+520.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 51963 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+530.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 52963 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+540.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 53963 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+550.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 54963 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223728 134557994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+560.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 55964 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+570.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 56964 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+580.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 57964 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+590.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 58964 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+600.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 59964 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+610.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 60964 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+620.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 61965 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+630.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 62965 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+640.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 63965 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+650.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 64965 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+660.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 65965 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+670.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 66965 39 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+680.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 67966 40 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+690.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 68966 40 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+700.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 69966 40 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134561097 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+710.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 70966 40 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+720.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13107 0 0 0 71966 40 0 0 25 0 1 0 479865856 56840192 12896 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13877 12896 603 41 0 13836 0
vsize: 55508
[startup+730.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 13713 0 0 0 72965 41 0 0 25 0 1 0 479865856 59396096 13502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14501 13502 603 41 0 14460 0
vsize: 58004
[startup+740.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 14463 0 0 0 73962 44 0 0 25 0 1 0 479865856 62488576 14252 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15256 14252 603 41 0 15215 0
vsize: 61024
[startup+750.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 15189 0 0 0 74960 46 0 0 25 0 1 0 479865856 65454080 14978 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15980 14979 603 41 0 15939 0
vsize: 63920
[startup+760.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 15809 0 0 0 75959 47 0 0 25 0 1 0 479865856 68009984 15598 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16604 15598 603 41 0 16563 0
vsize: 66416
[startup+770.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 16457 0 0 0 76958 49 0 0 25 0 1 0 479865856 70565888 16246 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17228 16246 603 41 0 17187 0
vsize: 68912
[startup+780.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 16637 0 0 0 77957 50 0 0 25 0 1 0 479865856 71372800 16426 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17425 16426 603 41 0 17384 0
vsize: 69700
[startup+790.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 17273 0 0 0 78954 53 0 0 25 0 1 0 479865856 73920512 17062 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18047 17062 603 41 0 18006 0
vsize: 72188
[startup+800.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 17977 0 0 0 79952 55 0 0 25 0 1 0 479865856 76869632 17766 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18767 17766 603 41 0 18726 0
vsize: 75068
[startup+810.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 18662 0 0 0 80950 57 0 0 25 0 1 0 479865856 79699968 18451 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19458 18451 603 41 0 19417 0
vsize: 77832
[startup+820.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 18858 0 0 0 81950 58 0 0 25 0 1 0 479865856 80388096 18647 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19626 18647 603 41 0 19585 0
vsize: 78504
[startup+830.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 18967 0 0 0 82950 58 0 0 25 0 1 0 479865856 80928768 18756 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19758 18756 603 41 0 19717 0
vsize: 79032
[startup+840.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 19039 0 0 0 83950 59 0 0 25 0 1 0 479865856 81199104 18828 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19824 18828 603 41 0 19783 0
vsize: 79296
[startup+850.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 19137 0 0 0 84949 59 0 0 25 0 1 0 479865856 81604608 18926 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19923 18926 603 41 0 19882 0
vsize: 79692
[startup+860.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 19566 0 0 0 85948 60 0 0 25 0 1 0 479865856 83357696 19355 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20351 19355 603 41 0 20310 0
vsize: 81404
[startup+870.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 19700 0 0 0 86948 61 0 0 25 0 1 0 479865856 83894272 19489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20482 19489 603 41 0 20441 0
vsize: 81928
[startup+880.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 20068 0 0 0 87947 63 0 0 25 0 1 0 479865856 85368832 19857 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20842 19857 603 41 0 20801 0
vsize: 83368
[startup+890.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 20364 0 0 0 88946 63 0 0 25 0 1 0 479865856 86585344 20153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21139 20153 603 41 0 21098 0
vsize: 84556
[startup+900.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 20849 0 0 0 89945 64 0 0 25 0 1 0 479865856 88473600 20638 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21600 20638 603 41 0 21559 0
vsize: 86400
[startup+910.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 21335 0 0 0 90944 66 0 0 25 0 1 0 479865856 90488832 21124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22092 21124 603 41 0 22051 0
vsize: 88368
[startup+920.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 21774 0 0 0 91942 68 0 0 25 0 1 0 479865856 92246016 21563 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22521 21563 603 41 0 22480 0
vsize: 90084
[startup+930.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 22183 0 0 0 92941 69 0 0 25 0 1 0 479865856 93999104 21972 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22949 21972 603 41 0 22908 0
vsize: 91796
[startup+940.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 22432 0 0 0 93940 70 0 0 25 0 1 0 479865856 94937088 22221 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23178 22221 603 41 0 23137 0
vsize: 92712
[startup+950.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 22781 0 0 0 94939 71 0 0 25 0 1 0 479865856 96419840 22570 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23540 22570 603 41 0 23499 0
vsize: 94160
[startup+960.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 22879 0 0 0 95939 71 0 0 25 0 1 0 479865856 96829440 22668 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23640 22668 603 41 0 23599 0
vsize: 94560
[startup+970.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 23002 0 0 0 96938 72 0 0 25 0 1 0 479865856 97234944 22791 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23739 22791 603 41 0 23698 0
vsize: 94956
[startup+980.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 23130 0 0 0 97938 72 0 0 25 0 1 0 479865856 97775616 22919 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23871 22919 603 41 0 23830 0
vsize: 95484
[startup+990.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 23205 0 0 0 98938 72 0 0 25 0 1 0 479865856 98045952 22994 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23937 22994 603 41 0 23896 0
vsize: 95748
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 23471 0 0 0 99937 73 0 0 25 0 1 0 479865856 99127296 23260 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24201 23260 603 41 0 24160 0
vsize: 96804
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 23994 0 0 0 100936 75 0 0 25 0 1 0 479865856 101281792 23783 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24727 23783 603 41 0 24686 0
vsize: 98908
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 24621 0 0 0 101935 76 0 0 25 0 1 0 479865856 103833600 24410 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25350 24410 603 41 0 25309 0
vsize: 101400
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 25218 0 0 0 102933 78 0 0 25 0 1 0 479865856 106262528 25007 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25943 25007 603 41 0 25902 0
vsize: 103772
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 25998 0 0 0 103931 80 0 0 25 0 1 0 479865856 110391296 25787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26951 25787 603 41 0 26910 0
vsize: 107804
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 26524 0 0 0 104929 82 0 0 25 0 1 0 479865856 112541696 26313 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27476 26313 603 41 0 27435 0
vsize: 109904
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 27048 0 0 0 105927 84 0 0 25 0 1 0 479865856 114688000 26837 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28000 26837 603 41 0 27959 0
vsize: 112000
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 27500 0 0 0 106926 86 0 0 25 0 1 0 479865856 116584448 27289 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28463 27289 603 41 0 28422 0
vsize: 113852
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 27911 0 0 0 107925 87 0 0 25 0 1 0 479865856 118243328 27700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28868 27700 603 41 0 28827 0
vsize: 115472
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 28295 0 0 0 108923 88 0 0 25 0 1 0 479865856 119885824 28084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29269 28084 603 41 0 29228 0
vsize: 117076
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 28677 0 0 0 109921 90 0 0 25 0 1 0 479865856 121368576 28466 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29631 28466 603 41 0 29590 0
vsize: 118524
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29008 0 0 0 110920 92 0 0 25 0 1 0 479865856 122720256 28797 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29961 28797 603 41 0 29920 0
vsize: 119844
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29257 0 0 0 111919 92 0 0 25 0 1 0 479865856 123809792 29046 4294967295 134512640 134672761 3221224544 3221223744 134557892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30227 29046 603 41 0 30186 0
vsize: 120908
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29268 0 0 0 112920 92 0 0 25 0 1 0 479865856 123809792 29057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30227 29057 603 41 0 30186 0
vsize: 120908
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29268 0 0 0 113920 92 0 0 25 0 1 0 479865856 123809792 29057 4294967295 134512640 134672761 3221224544 3221223696 134565140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30227 29057 603 41 0 30186 0
vsize: 120908
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29268 0 0 0 114920 93 0 0 25 0 1 0 479865856 123809792 29057 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30227 29057 603 41 0 30186 0
vsize: 120908
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29268 0 0 0 115919 93 0 0 25 0 1 0 479865856 123809792 29057 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30227 29057 603 41 0 30186 0
vsize: 120908
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29268 0 0 0 116918 93 0 0 25 0 1 0 479865856 123809792 29057 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30227 29057 603 41 0 30186 0
vsize: 120908
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29268 0 0 0 117918 93 0 0 25 0 1 0 479865856 123809792 29057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30227 29057 603 41 0 30186 0
vsize: 120908
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29268 0 0 0 118919 93 0 0 25 0 1 0 479865856 123809792 29057 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30227 29057 603 41 0 30186 0
vsize: 120908
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 22301
Raw data (stat): 22301 (minisat+) R 22300 18865 18864 0 -1 0 29268 0 0 0 119919 93 0 0 25 0 1 0 479865856 123809792 29057 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30227 29057 603 41 0 30186 0
vsize: 120908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 22301
Raw data (stat): 22301 (minisat+) Z 22300 18865 18864 0 -1 12 29271 0 0 0 119920 98 0 0 25 0 1 0 479865856 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.1
CPU time (s): 1200.19
CPU user time (s): 1199.2
CPU system time (s): 0.989849
CPU usage (%): 100.008
Max. virtual memory (Kb): 120908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####