PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-fit1d.opb
MD5SUM	de6e9dcd85d0fedc70e76c82543d6a33
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	11514
Biggest coefficient in the objective function	2949120
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	462466666
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	3870720
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	580921206
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.18
Number of variables	11514
Total number of constraints	1050
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1050
Minimum length of a constraint	11
Maximum length of a constraint	11514
Trace number 23002

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-22 04:08:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=10787 boxname=wulflinc6 idbench=830 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  de6e9dcd85d0fedc70e76c82543d6a33  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-fit1d.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-fit1d.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-fit1d.opb
IDLAUNCH: 10787
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        526308 kB
Buffers:         28008 kB
Cached:         459036 kB
SwapCached:        516 kB
Active:          78796 kB
Inactive:       410304 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        526056 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13560 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 04:28:02 (client local time) WITH STATUS 0 IN 1200.63 SECONDS
stats: 10787 7 1200.63 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1051 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): (none)
c ---[1050]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1049]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1048]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1047]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1046]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1045]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1044]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1043]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1042]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1041]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1040]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1039]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1038]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1037]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1036]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1035]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1034]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1033]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1032]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1031]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1030]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1029]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1028]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1027]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1026]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1025]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1024]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1023]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1022]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1021]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1020]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1019]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1018]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1017]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1016]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1015]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1014]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1013]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1012]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1011]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1010]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1009]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1008]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1007]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1006]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1005]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1004]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1003]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1002]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1001]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[1000]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 999]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 998]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 997]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 996]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 995]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 994]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 993]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 992]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 991]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 990]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 989]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 988]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 987]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 986]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 985]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 984]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 983]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 982]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 981]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 980]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 979]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 978]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 977]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 976]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 975]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 974]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 973]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 972]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 971]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 970]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 969]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 968]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 967]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 966]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 965]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 964]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 963]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 962]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 961]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 960]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 959]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 958]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 957]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 956]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 955]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 954]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 953]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 952]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 951]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 950]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 949]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 948]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 947]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 946]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 945]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 944]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 943]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 942]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 941]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 940]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 939]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 938]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 937]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 936]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 935]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 934]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 933]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 932]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 931]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 930]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 929]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 928]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 927]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 926]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 925]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 924]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 923]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 922]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 921]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 920]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 919]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 918]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 917]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 916]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 915]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 914]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 913]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 912]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 911]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 910]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 909]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 908]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 907]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 906]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 905]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 904]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 903]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 902]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 901]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 900]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 899]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 898]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 897]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 896]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 895]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 894]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 893]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 892]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 891]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 890]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 889]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 888]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 887]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 886]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 885]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 884]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 883]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 882]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 881]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 880]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 879]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 878]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 877]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 876]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 875]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 874]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 873]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 872]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 871]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 870]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 869]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 868]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 867]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 866]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 865]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 864]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 863]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 862]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 861]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 860]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 859]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 858]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 857]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 856]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 855]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 854]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 853]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 852]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 851]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 850]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 849]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 848]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 847]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 846]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 845]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 844]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 843]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 842]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 841]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 840]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 839]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 838]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 837]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 836]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 835]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 834]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 833]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 832]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 831]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 830]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 829]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 828]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 827]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 826]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 825]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 824]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 823]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 822]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 821]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 820]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 819]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 818]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 817]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 816]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 815]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 814]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 813]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 812]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 811]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 810]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 809]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 808]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 807]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 806]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 805]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 804]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 803]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 802]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 801]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 800]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 799]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 798]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 797]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 796]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 795]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 794]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 793]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 792]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 791]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 790]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 789]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 788]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 787]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 786]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 785]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 784]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 783]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 782]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 781]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 780]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 779]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 778]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 777]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 776]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 775]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 774]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 773]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 772]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 771]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 770]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 769]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 768]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 767]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 766]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 765]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 764]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 763]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 762]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 761]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 760]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 759]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 758]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 757]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 756]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 755]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 754]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 753]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 752]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 751]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 750]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 749]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 748]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 747]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 746]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 745]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 744]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 743]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 742]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 741]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 740]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 739]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 738]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 737]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 736]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 735]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 734]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 733]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 732]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 731]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 730]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 729]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 728]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 727]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 726]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 725]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 724]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 723]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 722]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 721]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 720]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 719]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 718]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 717]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 716]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 715]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 714]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 713]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 712]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 711]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 710]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 709]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 708]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 707]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 706]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 705]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 704]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 703]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 702]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 701]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 700]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 699]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 698]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 697]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 696]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 695]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 694]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 693]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 692]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 691]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 690]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 689]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 688]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 687]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 686]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 685]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 684]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 683]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 682]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 681]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 680]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 679]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 678]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 677]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 676]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 675]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 674]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 673]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 672]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 671]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 670]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 669]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 668]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 667]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 666]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 665]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 664]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 663]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 662]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 661]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 660]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 659]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 658]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 657]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 656]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 655]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 654]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 653]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 652]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 651]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 650]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 649]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 648]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 647]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 646]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 645]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 644]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 643]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 642]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 641]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 640]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 639]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 638]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 637]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 636]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 635]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 634]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 633]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 632]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 631]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 630]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 629]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 628]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 627]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 626]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 625]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 624]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 623]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 622]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 621]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 620]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 619]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 618]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 617]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 616]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 615]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 614]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 613]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 612]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 611]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 610]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 609]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 608]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 607]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 606]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 605]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 604]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 603]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 602]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 601]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 600]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 599]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 598]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 597]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 596]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 595]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 594]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 593]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 592]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 591]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 590]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 589]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 588]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 587]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 586]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 585]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 584]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 583]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 582]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 581]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 580]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 579]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 578]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 577]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 576]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 575]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 574]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 573]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 572]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 571]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 570]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 569]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 568]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 567]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 566]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 565]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 564]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 563]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 562]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 561]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 560]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 559]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 558]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 557]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 556]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 555]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 554]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 553]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 552]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 551]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 550]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 549]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 548]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 547]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 546]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 545]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 544]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 543]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 542]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 541]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 540]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 539]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 538]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 537]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 536]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 535]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 534]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 533]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 532]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 531]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 530]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 529]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 528]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 527]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 526]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 525]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 524]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 523]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 522]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 521]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 520]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 519]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 518]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 517]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 516]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 515]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 514]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 513]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 512]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 511]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 510]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 509]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 508]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 507]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 506]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 505]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 504]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 503]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 502]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 501]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 500]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 499]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 498]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 497]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 496]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 495]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 494]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 493]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 492]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 491]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 490]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 489]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 488]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 487]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 486]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 485]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 484]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 483]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 482]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 481]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 480]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 479]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 478]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 477]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 476]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 475]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 474]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 473]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 472]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 471]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 470]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 469]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 468]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 467]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 466]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 465]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 464]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 463]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 462]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 461]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 460]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 459]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 458]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 457]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 456]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 455]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 454]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 453]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 452]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 451]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 450]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 449]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 448]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 447]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 446]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 445]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 444]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 443]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 442]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 441]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 440]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 439]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 438]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 437]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 436]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 435]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 434]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 433]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 432]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 431]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 430]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 429]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 428]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 427]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 426]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 425]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 424]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 423]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 422]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 421]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 420]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 419]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 418]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 417]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 416]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 415]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 414]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 413]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 412]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 411]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 410]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 409]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 408]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 407]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 406]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 405]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 404]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 403]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 402]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 401]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 400]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 399]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 398]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 397]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 396]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 395]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 394]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 393]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 392]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 391]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 390]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 389]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 388]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 387]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 386]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 385]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 384]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 383]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 382]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 381]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 380]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 379]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 378]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 377]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 376]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 375]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 374]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 373]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 372]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 371]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 370]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 369]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 368]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 367]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 366]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 365]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 364]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 363]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 362]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 361]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 360]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 359]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 358]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 357]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 356]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 355]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 354]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 353]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 352]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 351]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 350]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 349]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 348]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 347]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 346]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 345]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 344]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 343]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 342]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 341]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 340]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 339]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 338]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 337]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 336]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 335]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 334]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 333]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 332]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 331]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 330]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 329]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 328]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 327]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 326]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 325]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 324]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 323]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 322]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 321]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 320]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 319]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 318]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 317]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 316]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 315]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 314]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 313]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 312]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 311]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 310]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 309]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 308]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 307]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 306]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 305]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 304]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 303]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 302]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 301]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 300]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 299]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 298]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 297]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 296]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 295]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 294]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 293]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 292]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 291]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 290]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 289]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 288]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 287]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 286]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 285]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 284]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 283]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 282]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 281]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 280]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 279]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 278]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 277]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 276]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 275]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 274]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 273]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 272]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 271]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 270]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 269]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 268]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 267]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 266]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 265]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 264]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 263]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 262]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 261]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 260]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 259]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 258]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 257]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 256]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 255]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 254]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 253]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 252]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 251]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 250]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 249]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 248]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 247]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 246]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 245]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 244]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 243]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 242]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 241]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 240]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 239]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 238]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 237]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 236]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 235]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 234]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 233]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 232]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 231]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 230]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 229]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 228]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 227]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 226]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 225]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 224]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 223]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 222]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 221]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 220]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 219]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 218]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 217]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 216]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 215]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 214]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 213]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 212]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 211]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 210]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 209]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 208]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 207]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 206]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 205]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 204]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 203]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 202]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 201]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 200]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 199]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 198]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 197]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 196]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 195]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 194]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 193]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 192]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 191]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 190]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 189]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 188]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 187]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 186]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 185]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 184]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 183]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 182]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 181]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 180]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 179]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 178]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 177]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 176]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 175]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 174]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 173]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 172]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 171]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 170]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 169]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 168]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 167]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 166]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 165]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 164]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 163]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 162]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 161]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 160]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 159]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 158]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 157]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 156]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 155]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 154]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 153]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 152]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 151]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 150]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 149]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 148]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 147]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 146]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 145]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 144]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 143]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 142]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 141]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 140]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 139]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 138]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 137]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 136]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 135]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 134]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 132]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 131]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 130]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 129]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 127]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 126]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 125]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 124]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 123]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 122]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 121]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 120]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 119]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 118]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 117]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 116]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 115]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 114]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 113]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 112]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 111]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 110]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 109]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 108]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 107]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 106]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 105]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 104]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 103]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 102]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 101]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 100]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  99]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  98]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  97]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  96]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  95]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  94]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  92]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  91]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  90]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  89]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  88]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  87]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  86]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  85]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  83]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  82]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  80]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  79]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  78]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  77]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  76]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  75]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  74]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  73]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  72]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  71]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  70]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  69]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  68]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  67]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  66]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  65]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  64]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  63]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  62]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  61]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  60]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  59]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  58]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  57]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  56]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  55]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  54]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  53]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  52]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  51]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  50]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  49]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  48]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  47]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  46]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  45]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  44]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  42]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  41]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  40]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  39]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  38]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  37]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  36]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  35]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  34]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  33]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  32]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  31]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  30]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  29]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  28]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  27]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[  23]---> Adder-cost: 22993   maxlim: 816753   bits: 21/20
c ---[  22]---> Adder-cost: 48143   maxlim: 53250657   bits: 27/26
c ---[  21]---> Adder-cost: 24490   maxlim: 37410971   bits: 27/26
c ---[  20]---> Adder-cost: 18532   maxlim: 62407570   bits: 27/26
c ---[  19]---> Adder-cost: 64462   maxlim: 396293572   bits: 30/29
c ---[  18]---> Adder-cost: 9918   maxlim: 1625605   bits: 21/21
c ---[  17]---> Adder-cost: 39824   maxlim: 26785026   bits: 26/25
c ---[  16]---> Adder-cost: 60627   maxlim: 27028587   bits: 26/25
c ---[  15]---> Adder-cost: 50627   maxlim: 58642455   bits: 27/26
c ---[  14]---> Adder-cost: 19026   maxlim: 1373536   bits: 22/21
c ---[  13]---> Adder-cost: 25006   maxlim: 4696498   bits: 23/23
c ---[  12]---> Adder-cost: 69126   maxlim: 389685799   bits: 30/29
c ---[  11]---> Adder-cost: 2804   maxlim: 712518   bits: 20/20
c ---[  10]---> Adder-cost: 11416   maxlim: 36659016   bits: 26/26
c ---[   9]---> Adder-cost: 39511   maxlim: 31990515   bits: 26/25
c ---[   8]---> Adder-cost: 5682   maxlim: 513869   bits: 20/19
c ---[   7]---> Adder-cost: 5867   maxlim: 245639   bits: 19/18
c ---[   6]---> Adder-cost: 6404   maxlim: 282485   bits: 20/19
c ---[   5]---> Adder-cost: 11426   maxlim: 540407   bits: 21/20
c ---[   4]---> Adder-cost: 5814   maxlim: 585536   bits: 20/20
c ---[   3]---> Adder-cost: 4529   maxlim: 200605   bits: 19/18
c ---[   2]---> Adder-cost: 2945   maxlim: 126913   bits: 18/17
c ---[   1]---> Adder-cost: 7696   maxlim: 753405   bits: 21/20
c ---[   0]---> Adder-cost: 5242   maxlim: 276344   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 4101040 14684190 | 1367013       0        0     nan |  0.000 % |
c |       100 | 4101040 14684190 | 1503714     100      344     3.4 |  1.737 % |
c |       250 | 4101040 14684190 | 1654085     250      817     3.3 |  1.737 % |
c |       475 | 4101040 14684190 | 1819494     475     1565     3.3 |  1.737 % |
c |       812 | 4101040 14684190 | 2001443     812     2742     3.4 |  1.737 % |
c |      1318 | 4101040 14684190 | 2201588    1318     4561     3.5 |  1.737 % |
c |      2077 | 4101040 14684190 | 2421746    2077     7182     3.5 |  1.737 % |
c |      3217 | 4101040 14684190 | 2663921    3217    11685     3.6 |  1.737 % |
c |      4925 | 4101040 14684190 | 2930313    4925    18241     3.7 |  1.737 % |
c |      7487 | 4101034 14684173 | 3223345    7486    27699     3.7 |  1.737 % |
c |     11331 | 4101034 14684173 | 3545679   11330    44364     3.9 |  1.737 % |
c |     17097 | 4101034 14684173 | 3900247   17096    75190     4.4 |  1.737 % |
c |     25746 | 4101034 14684173 | 4290272   25745   130776     5.1 |  1.737 % |
c |     38720 | 4101027 14684150 | 4719299   38718   203663     5.3 |  1.737 % |
c |     58182 | 4101011 14684098 | 5191229   58178   386260     6.6 |  1.738 % |
c |     87374 | 4101011 14684098 | 5710352   87370  1128913    12.9 |  1.738 % |
c |    131163 | 4101011 14684098 | 6281387  131159  1374250    10.5 |  1.738 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 1.01 0.94 2/54 4956
Raw data (stat): 4956 (runsolver) R 4955 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 492497147 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+9.99998 s]
Raw data (loadavg): 0.94 1.01 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 40366 0 0 0 906 92 0 0 25 0 1 0 492497147 183357440 37598 4294967295 134512640 134672761 3221224544 3221217352 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44765 37599 603 41 0 44724 0
vsize: 179060
[startup+20.0011 s]
Raw data (loadavg): 0.95 1.01 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 68000 0 0 0 1845 154 0 0 25 0 1 0 492497147 305803264 65232 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74659 65232 603 41 0 74618 0
vsize: 298636
[startup+30.0019 s]
Raw data (loadavg): 0.96 1.01 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 68513 0 0 0 2844 155 0 0 25 0 1 0 492497147 307965952 65745 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75187 65745 603 41 0 75146 0
vsize: 300748
[startup+40.0024 s]
Raw data (loadavg): 0.96 1.01 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 68890 0 0 0 3843 156 0 0 25 0 1 0 492497147 309587968 66122 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75583 66122 603 41 0 75542 0
vsize: 302332
[startup+50.0025 s]
Raw data (loadavg): 0.97 1.01 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 69213 0 0 0 4841 158 0 0 25 0 1 0 492497147 310804480 66445 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75880 66445 603 41 0 75839 0
vsize: 303520
[startup+60.003 s]
Raw data (loadavg): 0.97 1.01 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 69538 0 0 0 5841 158 0 0 25 0 1 0 492497147 312152064 66770 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76209 66770 603 41 0 76168 0
vsize: 304836
[startup+70.0028 s]
Raw data (loadavg): 0.98 1.01 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 69813 0 0 0 6840 159 0 0 25 0 1 0 492497147 313380864 67045 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76509 67045 603 41 0 76468 0
vsize: 306036
[startup+80.003 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 70081 0 0 0 7839 161 0 0 25 0 1 0 492497147 314462208 67313 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76773 67313 603 41 0 76732 0
vsize: 307092
[startup+90.0039 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 70324 0 0 0 8839 161 0 0 25 0 1 0 492497147 315408384 67556 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 67556 603 41 0 76963 0
vsize: 308016
[startup+100.004 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 70502 0 0 0 9839 162 0 0 25 0 1 0 492497147 316084224 67734 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77169 67734 603 41 0 77128 0
vsize: 308676
[startup+110.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 70682 0 0 0 10839 162 0 0 25 0 1 0 492497147 316895232 67914 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77367 67914 603 41 0 77326 0
vsize: 309468
[startup+120.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 70848 0 0 0 11839 163 0 0 25 0 1 0 492497147 317571072 68080 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77532 68080 603 41 0 77491 0
vsize: 310128
[startup+130.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 70955 0 0 0 12839 163 0 0 25 0 1 0 492497147 317976576 68187 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77631 68187 603 41 0 77590 0
vsize: 310524
[startup+140.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71080 0 0 0 13839 163 0 0 25 0 1 0 492497147 318382080 68312 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77730 68312 603 41 0 77689 0
vsize: 310920
[startup+150.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71205 0 0 0 14839 164 0 0 25 0 1 0 492497147 318922752 68437 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77862 68437 603 41 0 77821 0
vsize: 311448
[startup+160.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71303 0 0 0 15839 164 0 0 25 0 1 0 492497147 319455232 68535 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77992 68535 603 41 0 77951 0
vsize: 311968
[startup+170.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71420 0 0 0 16839 165 0 0 25 0 1 0 492497147 319995904 68652 4294967295 134512640 134672761 3221224544 3221223696 134565143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78124 68652 603 41 0 78083 0
vsize: 312496
[startup+180.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71524 0 0 0 17839 165 0 0 25 0 1 0 492497147 320401408 68756 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78223 68756 603 41 0 78182 0
vsize: 312892
[startup+190.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71605 0 0 0 18839 165 0 0 25 0 1 0 492497147 320671744 68837 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78289 68837 603 41 0 78248 0
vsize: 313156
[startup+200.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71689 0 0 0 19839 166 0 0 25 0 1 0 492497147 321077248 68921 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78388 68921 603 41 0 78347 0
vsize: 313552
[startup+210.05 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71757 0 0 0 20843 166 0 0 25 0 1 0 492497147 321212416 68989 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78421 68989 603 41 0 78380 0
vsize: 313684
[startup+220.066 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71829 0 0 0 21845 166 0 0 25 0 1 0 492497147 321617920 69061 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78520 69061 603 41 0 78479 0
vsize: 314080
[startup+230.066 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71922 0 0 0 22845 166 0 0 25 0 1 0 492497147 321888256 69154 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78586 69154 603 41 0 78545 0
vsize: 314344
[startup+240.066 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 71986 0 0 0 23845 167 0 0 25 0 1 0 492497147 322158592 69218 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78652 69218 603 41 0 78611 0
vsize: 314608
[startup+250.069 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72091 0 0 0 24845 167 0 0 25 0 1 0 492497147 322564096 69323 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78751 69323 603 41 0 78710 0
vsize: 315004
[startup+260.073 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72157 0 0 0 25846 167 0 0 25 0 1 0 492497147 322834432 69389 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78817 69389 603 41 0 78776 0
vsize: 315268
[startup+270.073 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72221 0 0 0 26846 167 0 0 25 0 1 0 492497147 323104768 69453 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78883 69453 603 41 0 78842 0
vsize: 315532
[startup+280.079 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72286 0 0 0 27847 167 0 0 25 0 1 0 492497147 323375104 69518 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78949 69518 603 41 0 78908 0
vsize: 315796
[startup+290.09 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72339 0 0 0 28848 167 0 0 25 0 1 0 492497147 323645440 69571 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79015 69571 603 41 0 78974 0
vsize: 316060
[startup+300.09 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72410 0 0 0 29848 168 0 0 25 0 1 0 492497147 323915776 69642 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79081 69642 603 41 0 79040 0
vsize: 316324
[startup+310.091 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72460 0 0 0 30848 168 0 0 25 0 1 0 492497147 324050944 69692 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79114 69692 603 41 0 79073 0
vsize: 316456
[startup+320.091 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72515 0 0 0 31848 168 0 0 25 0 1 0 492497147 324321280 69747 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79180 69747 603 41 0 79139 0
vsize: 316720
[startup+330.091 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72601 0 0 0 32848 169 0 0 25 0 1 0 492497147 324587520 69833 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79245 69833 603 41 0 79204 0
vsize: 316980
[startup+340.092 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72661 0 0 0 33848 169 0 0 25 0 1 0 492497147 324857856 69893 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79311 69893 603 41 0 79270 0
vsize: 317244
[startup+350.092 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 72811 0 0 0 34848 169 0 0 25 0 1 0 492497147 325394432 70043 4294967295 134512640 134672761 3221224544 3221223648 134560523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79442 70043 603 41 0 79401 0
vsize: 317768
[startup+360.092 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 73514 0 0 0 35847 171 0 0 25 0 1 0 492497147 328626176 70746 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80231 70746 603 41 0 80190 0
vsize: 320924
[startup+370.093 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 73608 0 0 0 36847 171 0 0 25 0 1 0 492497147 328896512 70840 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80297 70840 603 41 0 80256 0
vsize: 321188
[startup+380.092 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 73691 0 0 0 37847 171 0 0 25 0 1 0 492497147 329302016 70923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80396 70923 603 41 0 80355 0
vsize: 321584
[startup+390.093 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 73760 0 0 0 38847 171 0 0 25 0 1 0 492497147 329572352 70992 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80462 70992 603 41 0 80421 0
vsize: 321848
[startup+400.094 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 73820 0 0 0 39847 172 0 0 25 0 1 0 492497147 329842688 71052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80528 71052 603 41 0 80487 0
vsize: 322112
[startup+410.094 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 73858 0 0 0 40848 172 0 0 25 0 1 0 492497147 329977856 71090 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80561 71090 603 41 0 80520 0
vsize: 322244
[startup+420.094 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 73912 0 0 0 41848 172 0 0 25 0 1 0 492497147 330113024 71144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80594 71144 603 41 0 80553 0
vsize: 322376
[startup+430.094 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 73985 0 0 0 42848 172 0 0 25 0 1 0 492497147 330383360 71217 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80660 71217 603 41 0 80619 0
vsize: 322640
[startup+440.094 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74021 0 0 0 43848 173 0 0 25 0 1 0 492497147 330518528 71253 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80693 71253 603 41 0 80652 0
vsize: 322772
[startup+450.095 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74056 0 0 0 44848 173 0 0 25 0 1 0 492497147 330653696 71288 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80726 71288 603 41 0 80685 0
vsize: 322904
[startup+460.096 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74106 0 0 0 45849 173 0 0 25 0 1 0 492497147 330924032 71338 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80792 71338 603 41 0 80751 0
vsize: 323168
[startup+470.097 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74151 0 0 0 46848 173 0 0 25 0 1 0 492497147 331059200 71383 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80825 71383 603 41 0 80784 0
vsize: 323300
[startup+480.097 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74181 0 0 0 47849 173 0 0 25 0 1 0 492497147 331194368 71413 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80858 71413 603 41 0 80817 0
vsize: 323432
[startup+490.098 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74212 0 0 0 48849 173 0 0 25 0 1 0 492497147 331329536 71444 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80891 71444 603 41 0 80850 0
vsize: 323564
[startup+500.098 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74242 0 0 0 49849 173 0 0 25 0 1 0 492497147 331464704 71474 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80924 71474 603 41 0 80883 0
vsize: 323696
[startup+510.099 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74268 0 0 0 50849 174 0 0 25 0 1 0 492497147 331464704 71500 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80924 71500 603 41 0 80883 0
vsize: 323696
[startup+520.1 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74298 0 0 0 51850 174 0 0 25 0 1 0 492497147 331599872 71530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80957 71530 603 41 0 80916 0
vsize: 323828
[startup+530.1 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74334 0 0 0 52850 174 0 0 25 0 1 0 492497147 331735040 71566 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80990 71566 603 41 0 80949 0
vsize: 323960
[startup+540.1 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74364 0 0 0 53850 174 0 0 25 0 1 0 492497147 331870208 71596 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81023 71596 603 41 0 80982 0
vsize: 324092
[startup+550.101 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74391 0 0 0 54850 174 0 0 25 0 1 0 492497147 332005376 71623 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81056 71623 603 41 0 81015 0
vsize: 324224
[startup+560.102 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74416 0 0 0 55851 174 0 0 25 0 1 0 492497147 332140544 71648 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81089 71648 603 41 0 81048 0
vsize: 324356
[startup+570.103 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74439 0 0 0 56851 174 0 0 25 0 1 0 492497147 332140544 71671 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81089 71671 603 41 0 81048 0
vsize: 324356
[startup+580.103 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74461 0 0 0 57851 174 0 0 25 0 1 0 492497147 332275712 71693 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81122 71693 603 41 0 81081 0
vsize: 324488
[startup+590.105 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74493 0 0 0 58851 175 0 0 25 0 1 0 492497147 332410880 71725 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81155 71725 603 41 0 81114 0
vsize: 324620
[startup+600.105 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74522 0 0 0 59851 175 0 0 25 0 1 0 492497147 332410880 71754 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81155 71754 603 41 0 81114 0
vsize: 324620
[startup+610.106 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74547 0 0 0 60852 175 0 0 25 0 1 0 492497147 332546048 71779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81188 71779 603 41 0 81147 0
vsize: 324752
[startup+620.107 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74576 0 0 0 61852 175 0 0 25 0 1 0 492497147 332681216 71808 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81221 71808 603 41 0 81180 0
vsize: 324884
[startup+630.108 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74601 0 0 0 62852 176 0 0 25 0 1 0 492497147 332816384 71833 4294967295 134512640 134672761 3221224544 3221223760 134557489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81254 71833 603 41 0 81213 0
vsize: 325016
[startup+640.108 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74625 0 0 0 63852 176 0 0 25 0 1 0 492497147 332816384 71857 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81254 71857 603 41 0 81213 0
vsize: 325016
[startup+650.109 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74653 0 0 0 64853 176 0 0 25 0 1 0 492497147 332951552 71885 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81287 71885 603 41 0 81246 0
vsize: 325148
[startup+660.11 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74672 0 0 0 65852 176 0 0 25 0 1 0 492497147 333086720 71904 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81320 71904 603 41 0 81279 0
vsize: 325280
[startup+670.111 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74700 0 0 0 66852 177 0 0 25 0 1 0 492497147 333086720 71932 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81320 71932 603 41 0 81279 0
vsize: 325280
[startup+680.111 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74719 0 0 0 67852 177 0 0 25 0 1 0 492497147 333221888 71951 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81353 71951 603 41 0 81312 0
vsize: 325412
[startup+690.113 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74739 0 0 0 68853 177 0 0 25 0 1 0 492497147 333221888 71971 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81353 71971 603 41 0 81312 0
vsize: 325412
[startup+700.113 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74766 0 0 0 69853 177 0 0 25 0 1 0 492497147 333357056 71998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81386 71998 603 41 0 81345 0
vsize: 325544
[startup+710.113 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74782 0 0 0 70853 177 0 0 25 0 1 0 492497147 333357056 72014 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81386 72014 603 41 0 81345 0
vsize: 325544
[startup+720.114 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74802 0 0 0 71854 177 0 0 25 0 1 0 492497147 333492224 72034 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81419 72034 603 41 0 81378 0
vsize: 325676
[startup+730.115 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74818 0 0 0 72854 177 0 0 25 0 1 0 492497147 333627392 72050 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81452 72050 603 41 0 81411 0
vsize: 325808
[startup+740.115 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74842 0 0 0 73854 178 0 0 25 0 1 0 492497147 333627392 72074 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81452 72074 603 41 0 81411 0
vsize: 325808
[startup+750.116 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74858 0 0 0 74854 178 0 0 25 0 1 0 492497147 333762560 72090 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81485 72090 603 41 0 81444 0
vsize: 325940
[startup+760.116 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74876 0 0 0 75854 178 0 0 25 0 1 0 492497147 333762560 72108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81485 72108 603 41 0 81444 0
vsize: 325940
[startup+770.116 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74890 0 0 0 76855 178 0 0 25 0 1 0 492497147 333897728 72122 4294967295 134512640 134672761 3221224544 3221223712 134564734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81518 72122 603 41 0 81477 0
vsize: 326072
[startup+780.117 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74905 0 0 0 77855 178 0 0 25 0 1 0 492497147 333897728 72137 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81518 72137 603 41 0 81477 0
vsize: 326072
[startup+790.118 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74927 0 0 0 78855 178 0 0 25 0 1 0 492497147 333897728 72159 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81518 72159 603 41 0 81477 0
vsize: 326072
[startup+800.119 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74944 0 0 0 79856 178 0 0 25 0 1 0 492497147 334032896 72176 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81551 72176 603 41 0 81510 0
vsize: 326204
[startup+810.135 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74961 0 0 0 80857 179 0 0 25 0 1 0 492497147 334032896 72193 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81551 72193 603 41 0 81510 0
vsize: 326204
[startup+820.135 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74976 0 0 0 81858 179 0 0 25 0 1 0 492497147 334168064 72208 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81584 72208 603 41 0 81543 0
vsize: 326336
[startup+830.136 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 74993 0 0 0 82858 179 0 0 25 0 1 0 492497147 334168064 72225 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81584 72225 603 41 0 81543 0
vsize: 326336
[startup+840.136 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75012 0 0 0 83858 179 0 0 25 0 1 0 492497147 334303232 72244 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81617 72244 603 41 0 81576 0
vsize: 326468
[startup+850.137 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75024 0 0 0 84858 179 0 0 25 0 1 0 492497147 334303232 72256 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81617 72256 603 41 0 81576 0
vsize: 326468
[startup+860.138 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75037 0 0 0 85859 179 0 0 25 0 1 0 492497147 334303232 72269 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81617 72269 603 41 0 81576 0
vsize: 326468
[startup+870.139 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75049 0 0 0 86859 179 0 0 25 0 1 0 492497147 334438400 72281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81650 72281 603 41 0 81609 0
vsize: 326600
[startup+880.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75063 0 0 0 87860 179 0 0 25 0 1 0 492497147 334438400 72295 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81650 72295 603 41 0 81609 0
vsize: 326600
[startup+890.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75083 0 0 0 88860 179 0 0 25 0 1 0 492497147 334573568 72315 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81683 72315 603 41 0 81642 0
vsize: 326732
[startup+900.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75101 0 0 0 89860 179 0 0 25 0 1 0 492497147 334573568 72333 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81683 72333 603 41 0 81642 0
vsize: 326732
[startup+910.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75116 0 0 0 90860 179 0 0 25 0 1 0 492497147 334708736 72348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81716 72348 603 41 0 81675 0
vsize: 326864
[startup+920.139 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75132 0 0 0 91860 180 0 0 25 0 1 0 492497147 334708736 72364 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81716 72364 603 41 0 81675 0
vsize: 326864
[startup+930.139 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75144 0 0 0 92861 180 0 0 25 0 1 0 492497147 334708736 72376 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81716 72376 603 41 0 81675 0
vsize: 326864
[startup+940.139 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75155 0 0 0 93861 180 0 0 25 0 1 0 492497147 334843904 72387 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81749 72387 603 41 0 81708 0
vsize: 326996
[startup+950.138 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75169 0 0 0 94861 180 0 0 25 0 1 0 492497147 334843904 72401 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81749 72401 603 41 0 81708 0
vsize: 326996
[startup+960.137 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75184 0 0 0 95861 180 0 0 25 0 1 0 492497147 334979072 72416 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81782 72416 603 41 0 81741 0
vsize: 327128
[startup+970.137 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75197 0 0 0 96861 180 0 0 25 0 1 0 492497147 334979072 72429 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81782 72429 603 41 0 81741 0
vsize: 327128
[startup+980.136 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75214 0 0 0 97861 180 0 0 25 0 1 0 492497147 334979072 72446 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81782 72446 603 41 0 81741 0
vsize: 327128
[startup+990.136 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75229 0 0 0 98862 180 0 0 25 0 1 0 492497147 335114240 72461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81815 72461 603 41 0 81774 0
vsize: 327260
[startup+1000.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75241 0 0 0 99862 181 0 0 25 0 1 0 492497147 335114240 72473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81815 72473 603 41 0 81774 0
vsize: 327260
[startup+1010.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75258 0 0 0 100862 181 0 0 25 0 1 0 492497147 335249408 72490 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81848 72490 603 41 0 81807 0
vsize: 327392
[startup+1020.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75270 0 0 0 101862 181 0 0 25 0 1 0 492497147 335249408 72502 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81848 72502 603 41 0 81807 0
vsize: 327392
[startup+1030.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75285 0 0 0 102862 181 0 0 25 0 1 0 492497147 335384576 72517 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81881 72517 603 41 0 81840 0
vsize: 327524
[startup+1040.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75302 0 0 0 103862 181 0 0 25 0 1 0 492497147 335384576 72534 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81881 72534 603 41 0 81840 0
vsize: 327524
[startup+1050.14 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75314 0 0 0 104863 181 0 0 25 0 1 0 492497147 335384576 72546 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81881 72546 603 41 0 81840 0
vsize: 327524
[startup+1060.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75325 0 0 0 105863 182 0 0 25 0 1 0 492497147 335519744 72557 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81914 72557 603 41 0 81873 0
vsize: 327656
[startup+1070.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75341 0 0 0 106863 182 0 0 25 0 1 0 492497147 335519744 72573 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81914 72573 603 41 0 81873 0
vsize: 327656
[startup+1080.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75360 0 0 0 107863 182 0 0 25 0 1 0 492497147 335654912 72592 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81947 72592 603 41 0 81906 0
vsize: 327788
[startup+1090.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75373 0 0 0 108863 182 0 0 25 0 1 0 492497147 335654912 72605 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81947 72605 603 41 0 81906 0
vsize: 327788
[startup+1100.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75387 0 0 0 109863 182 0 0 25 0 1 0 492497147 335654912 72619 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81947 72619 603 41 0 81906 0
vsize: 327788
[startup+1110.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75400 0 0 0 110864 182 0 0 25 0 1 0 492497147 335790080 72632 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81980 72632 603 41 0 81939 0
vsize: 327920
[startup+1120.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75413 0 0 0 111864 182 0 0 25 0 1 0 492497147 335790080 72645 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81980 72645 603 41 0 81939 0
vsize: 327920
[startup+1130.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75427 0 0 0 112864 182 0 0 25 0 1 0 492497147 335925248 72659 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82013 72659 603 41 0 81972 0
vsize: 328052
[startup+1140.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75439 0 0 0 113864 182 0 0 25 0 1 0 492497147 335925248 72671 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82013 72671 603 41 0 81972 0
vsize: 328052
[startup+1150.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75453 0 0 0 114865 182 0 0 25 0 1 0 492497147 335925248 72685 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82013 72685 603 41 0 81972 0
vsize: 328052
[startup+1160.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75466 0 0 0 115865 182 0 0 25 0 1 0 492497147 336060416 72698 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82046 72698 603 41 0 82005 0
vsize: 328184
[startup+1170.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75481 0 0 0 116865 182 0 0 25 0 1 0 492497147 336060416 72713 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82046 72713 603 41 0 82005 0
vsize: 328184
[startup+1180.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75495 0 0 0 117865 182 0 0 25 0 1 0 492497147 336195584 72727 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82079 72727 603 41 0 82038 0
vsize: 328316
[startup+1190.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75515 0 0 0 118865 183 0 0 25 0 1 0 492497147 336719872 72747 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82207 72747 603 41 0 82166 0
vsize: 328828
[startup+1200.13 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 4956
Raw data (stat): 4956 (minisat+) R 4955 29653 29652 0 -1 0 75528 0 0 0 119865 183 0 0 25 0 1 0 492497147 336719872 72760 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82207 72760 603 41 0 82166 0
vsize: 328828
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.28 s]
Raw data (loadavg): 0.99 1.00 0.94 1/54 4956
Raw data (stat): 4956 (minisat+) Z 4955 29653 29652 0 -1 12 75530 0 0 0 119865 197 0 0 25 0 1 0 492497147 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.28
CPU time (s): 1200.63
CPU user time (s): 1198.66
CPU system time (s): 1.9737
CPU usage (%): 100.03
Max. virtual memory (Kb): 328828
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####