PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-aflow30a.opb
MD5SUM	b74fb9cd57e8b4068255c4ac98aa23ca
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3191
Optimality of the best value was proved	NO
Number of terms in the objective function	421
Biggest coefficient in the objective function	500
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	72290
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	12800
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	416734
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.12
Number of variables	5932
Total number of constraints	1321
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	450
Number of constraints which are nor clauses,nor cardinality constraints	871
Minimum length of a constraint	1
Maximum length of a constraint	453
Trace number 18869

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        674004 kB
Buffers:          8916 kB
Cached:         326120 kB
SwapCached:        408 kB
Active:          49368 kB
Inactive:       288216 kB
HighTotal:      131008 kB
HighFree:        23968 kB
LowTotal:       903652 kB
LowFree:        650036 kB
SwapTotal:     2097892 kB
SwapFree:      2097056 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5856 kB
Slab:            17420 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:16:41 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 17404 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 958 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1020]---> Adder-cost: 26   maxlim: 4478   bits: 14/13
c ---[1019]---> Adder-cost: 37   maxlim: 766   bits: 11/10
c ---[1018]---> Adder-cost: 22   maxlim: 1662   bits: 12/11
c ---[1017]---> Adder-cost: 24   maxlim: 2302   bits: 13/12
c ---[1016]---> Adder-cost: 26   maxlim: 6398   bits: 14/13
c ---[1015]---> Adder-cost: 24   maxlim: 3838   bits: 13/12
c ---[1014]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[1013]---> Adder-cost: 43   maxlim: 2046   bits: 12/11
c ---[1012]---> Adder-cost: 43   maxlim: 3710   bits: 13/12
c ---[1011]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[1010]---> Adder-cost: 45   maxlim: 3966   bits: 13/12
c ---[1009]---> Adder-cost: 26   maxlim: 4990   bits: 14/13
c ---[1008]---> Adder-cost: 39   maxlim: 1406   bits: 12/11
c ---[1007]---> Adder-cost: 22   maxlim: 1918   bits: 12/11
c ---[1006]---> Adder-cost: 43   maxlim: 2046   bits: 12/11
c ---[1005]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[1004]---> Adder-cost: 26   maxlim: 7294   bits: 14/13
c ---[1002]---> Adder-cost: 26   maxlim: 6398   bits: 14/13
c ---[1001]---> Adder-cost: 26   maxlim: 4222   bits: 14/13
c ---[1000]---> Adder-cost: 24   maxlim: 2814   bits: 13/12
c ---[ 999]---> Adder-cost: 26   maxlim: 5374   bits: 14/13
c ---[ 998]---> Adder-cost: 26   maxlim: 5374   bits: 14/13
c ---[ 996]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 995]---> Adder-cost: 39   maxlim: 1278   bits: 12/11
c ---[ 993]---> Adder-cost: 24   maxlim: 3582   bits: 13/12
c ---[ 992]---> Adder-cost: 26   maxlim: 6910   bits: 14/13
c ---[ 991]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[ 990]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[ 989]---> Adder-cost: 24   maxlim: 2942   bits: 13/12
c ---[ 988]---> Adder-cost: 24   maxlim: 3454   bits: 13/12
c ---[ 987]---> Adder-cost: 26   maxlim: 8062   bits: 14/13
c ---[ 986]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 985]---> Adder-cost: 43   maxlim: 2046   bits: 12/11
c ---[ 984]---> Adder-cost: 26   maxlim: 4478   bits: 14/13
c ---[ 981]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 980]---> Adder-cost: 37   maxlim: 766   bits: 11/10
c ---[ 978]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[ 977]---> Adder-cost: 24   maxlim: 3710   bits: 13/12
c ---[ 974]---> Adder-cost: 33   maxlim: 382   bits: 10/9
c ---[ 973]---> Adder-cost: 24   maxlim: 3966   bits: 13/12
c ---[ 972]---> Adder-cost: 37   maxlim: 894   bits: 11/10
c ---[ 971]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 970]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[ 969]---> Adder-cost: 26   maxlim: 7678   bits: 14/13
c ---[ 968]---> Adder-cost: 43   maxlim: 3710   bits: 13/12
c ---[ 967]---> Adder-cost: 26   maxlim: 4606   bits: 14/13
c ---[ 966]---> Adder-cost: 24   maxlim: 2430   bits: 13/12
c ---[ 964]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 963]---> Adder-cost: 26   maxlim: 7038   bits: 14/13
c ---[ 962]---> Adder-cost: 41   maxlim: 1918   bits: 12/11
c ---[ 961]---> Adder-cost: 35   maxlim: 510   bits: 10/9
c ---[ 960]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[ 959]---> Adder-cost: 35   maxlim: 510   bits: 10/9
c ---[ 958]---> Adder-cost: 26   maxlim: 4990   bits: 14/13
c ---[ 956]---> Adder-cost: 41   maxlim: 1534   bits: 12/11
c ---[ 955]---> Adder-cost: 26   maxlim: 4990   bits: 14/13
c ---[ 954]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[ 953]---> Adder-cost: 26   maxlim: 7038   bits: 14/13
c ---[ 952]---> Adder-cost: 45   maxlim: 3966   bits: 13/12
c ---[ 951]---> Adder-cost: 22   maxlim: 1406   bits: 12/11
c ---[ 950]---> Adder-cost: 26   maxlim: 6782   bits: 14/13
c ---[ 949]---> Adder-cost: 26   maxlim: 5246   bits: 14/13
c ---[ 948]---> Adder-cost: 26   maxlim: 6526   bits: 14/13
c ---[ 947]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[ 946]---> Adder-cost: 26   maxlim: 6654   bits: 14/13
c ---[ 945]---> Adder-cost: 26   maxlim: 6014   bits: 14/13
c ---[ 944]---> Adder-cost: 24   maxlim: 3966   bits: 13/12
c ---[ 943]---> Adder-cost: 26   maxlim: 5502   bits: 14/13
c ---[ 942]---> Adder-cost: 26   maxlim: 5246   bits: 14/13
c ---[ 941]---> Adder-cost: 22   maxlim: 1662   bits: 12/11
c ---[ 940]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 939]---> Adder-cost: 26   maxlim: 7678   bits: 14/13
c ---[ 937]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 936]---> Adder-cost: 41   maxlim: 1790   bits: 12/11
c ---[ 935]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[ 934]---> Adder-cost: 26   maxlim: 6398   bits: 14/13
c ---[ 933]---> Adder-cost: 33   maxlim: 382   bits: 10/9
c ---[ 932]---> Adder-cost: 39   maxlim: 1662   bits: 12/11
c ---[ 931]---> Adder-cost: 24   maxlim: 2430   bits: 13/12
c ---[ 930]---> Adder-cost: 26   maxlim: 5886   bits: 14/13
c ---[ 928]---> Adder-cost: 37   maxlim: 894   bits: 11/10
c ---[ 927]---> Adder-cost: 26   maxlim: 6398   bits: 14/13
c ---[ 926]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 925]---> Adder-cost: 26   maxlim: 4222   bits: 14/13
c ---[ 924]---> Adder-cost: 26   maxlim: 7038   bits: 14/13
c ---[ 923]---> Adder-cost: 22   maxlim: 1278   bits: 12/11
c ---[ 922]---> Adder-cost: 41   maxlim: 1918   bits: 12/11
c ---[ 921]---> Adder-cost: 39   maxlim: 1278   bits: 12/11
c ---[ 919]---> Adder-cost: 43   maxlim: 2046   bits: 12/11
c ---[ 918]---> Adder-cost: 41   maxlim: 1534   bits: 12/11
c ---[ 917]---> Adder-cost: 26   maxlim: 4350   bits: 14/13
c ---[ 916]---> Adder-cost: 33   maxlim: 382   bits: 10/9
c ---[ 915]---> Adder-cost: 24   maxlim: 2174   bits: 13/12
c ---[ 914]---> Adder-cost: 26   maxlim: 7294   bits: 14/13
c ---[ 913]---> Adder-cost: 26   maxlim: 7806   bits: 14/13
c ---[ 912]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 911]---> Adder-cost: 26   maxlim: 4862   bits: 14/13
c ---[ 910]---> Adder-cost: 43   maxlim: 2046   bits: 12/11
c ---[ 908]---> Adder-cost: 26   maxlim: 8062   bits: 14/13
c ---[ 907]---> Adder-cost: 26   maxlim: 4350   bits: 14/13
c ---[ 906]---> Adder-cost: 24   maxlim: 3198   bits: 13/12
c ---[ 905]---> Adder-cost: 26   maxlim: 6270   bits: 14/13
c ---[ 903]---> Adder-cost: 26   maxlim: 5630   bits: 14/13
c ---[ 902]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 900]---> Adder-cost: 26   maxlim: 7678   bits: 14/13
c ---[ 899]---> Adder-cost: 35   maxlim: 510   bits: 10/9
c ---[ 898]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[ 897]---> Adder-cost: 41   maxlim: 1534   bits: 12/11
c ---[ 896]---> Adder-cost: 24   maxlim: 2686   bits: 13/12
c ---[ 895]---> Adder-cost: 26   maxlim: 7806   bits: 14/13
c ---[ 893]---> Adder-cost: 37   maxlim: 1150   bits: 12/11
c ---[ 892]---> Adder-cost: 26   maxlim: 6654   bits: 14/13
c ---[ 891]---> Adder-cost: 35   maxlim: 638   bits: 11/10
c ---[ 890]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[ 889]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 888]---> Adder-cost: 26   maxlim: 8062   bits: 14/13
c ---[ 887]---> Adder-cost: 26   maxlim: 6398   bits: 14/13
c ---[ 886]---> Adder-cost: 22   maxlim: 1790   bits: 12/11
c ---[ 885]---> Adder-cost: 26   maxlim: 4478   bits: 14/13
c ---[ 883]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[ 882]---> Adder-cost: 35   maxlim: 638   bits: 11/10
c ---[ 881]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[ 880]---> Adder-cost: 26   maxlim: 7294   bits: 14/13
c ---[ 879]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 878]---> Adder-cost: 24   maxlim: 3454   bits: 13/12
c ---[ 877]---> Adder-cost: 22   maxlim: 1278   bits: 12/11
c ---[ 876]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[ 875]---> Adder-cost: 26   maxlim: 6526   bits: 14/13
c ---[ 874]---> Adder-cost: 26   maxlim: 6782   bits: 14/13
c ---[ 873]---> Adder-cost: 22   maxlim: 1918   bits: 12/11
c ---[ 871]---> Adder-cost: 24   maxlim: 3198   bits: 13/12
c ---[ 870]---> Adder-cost: 26   maxlim: 6910   bits: 14/13
c ---[ 869]---> Adder-cost: 24   maxlim: 3454   bits: 13/12
c ---[ 867]---> Adder-cost: 37   maxlim: 766   bits: 11/10
c ---[ 866]---> Adder-cost: 45   maxlim: 3966   bits: 13/12
c ---[ 865]---> Adder-cost: 26   maxlim: 4606   bits: 14/13
c ---[ 863]---> Adder-cost: 26   maxlim: 4862   bits: 14/13
c ---[ 862]---> Adder-cost: 26   maxlim: 5374   bits: 14/13
c ---[ 861]---> Adder-cost: 39   maxlim: 1406   bits: 12/11
c ---[ 860]---> Adder-cost: 26   maxlim: 6910   bits: 14/13
c ---[ 859]---> Adder-cost: 24   maxlim: 2174   bits: 13/12
c ---[ 858]---> Adder-cost: 26   maxlim: 6654   bits: 14/13
c ---[ 857]---> Adder-cost: 39   maxlim: 1662   bits: 12/11
c ---[ 856]---> Adder-cost: 45   maxlim: 3966   bits: 13/12
c ---[ 855]---> Adder-cost: 24   maxlim: 3710   bits: 13/12
c ---[ 853]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 851]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 850]---> Adder-cost: 24   maxlim: 3454   bits: 13/12
c ---[ 849]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 848]---> Adder-cost: 24   maxlim: 2302   bits: 13/12
c ---[ 847]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 846]---> Adder-cost: 24   maxlim: 3582   bits: 13/12
c ---[ 845]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 844]---> Adder-cost: 24   maxlim: 2686   bits: 13/12
c ---[ 843]---> Adder-cost: 24   maxlim: 3454   bits: 13/12
c ---[ 842]---> Adder-cost: 22   maxlim: 1406   bits: 12/11
c ---[ 841]---> Adder-cost: 22   maxlim: 1790   bits: 12/11
c ---[ 840]---> Adder-cost: 35   maxlim: 510   bits: 10/9
c ---[ 839]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 837]---> Adder-cost: 33   maxlim: 382   bits: 10/9
c ---[ 836]---> Adder-cost: 24   maxlim: 3966   bits: 13/12
c ---[ 835]---> Adder-cost: 26   maxlim: 7294   bits: 14/13
c ---[ 834]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[ 833]---> Adder-cost: 26   maxlim: 6270   bits: 14/13
c ---[ 832]---> Adder-cost: 26   maxlim: 4606   bits: 14/13
c ---[ 831]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[ 829]---> Adder-cost: 26   maxlim: 7550   bits: 14/13
c ---[ 828]---> Adder-cost: 24   maxlim: 2558   bits: 13/12
c ---[ 825]---> Adder-cost: 37   maxlim: 894   bits: 11/10
c ---[ 824]---> Adder-cost: 26   maxlim: 5630   bits: 14/13
c ---[ 823]---> Adder-cost: 43   maxlim: 3710   bits: 13/12
c ---[ 822]---> Adder-cost: 24   maxlim: 3710   bits: 13/12
c ---[ 821]---> Adder-cost: 26   maxlim: 4478   bits: 14/13
c ---[ 820]---> Adder-cost: 26   maxlim: 4350   bits: 14/13
c ---[ 819]---> Adder-cost: 26   maxlim: 4350   bits: 14/13
c ---[ 818]---> Adder-cost: 26   maxlim: 4734   bits: 14/13
c ---[ 817]---> Adder-cost: 26   maxlim: 5886   bits: 14/13
c ---[ 816]---> Adder-cost: 26   maxlim: 7294   bits: 14/13
c ---[ 815]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 814]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[ 812]---> Adder-cost: 26   maxlim: 7934   bits: 14/13
c ---[ 811]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[ 809]---> Adder-cost: 24   maxlim: 3710   bits: 13/12
c ---[ 808]---> Adder-cost: 24   maxlim: 2558   bits: 13/12
c ---[ 807]---> Adder-cost: 26   maxlim: 8062   bits: 14/13
c ---[ 806]---> Adder-cost: 26   maxlim: 4990   bits: 14/13
c ---[ 805]---> Adder-cost: 24   maxlim: 2174   bits: 13/12
c ---[ 804]---> Adder-cost: 24   maxlim: 3582   bits: 13/12
c ---[ 803]---> Adder-cost: 26   maxlim: 5502   bits: 14/13
c ---[ 801]---> Adder-cost: 26   maxlim: 7422   bits: 14/13
c ---[ 800]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[ 799]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[ 798]---> Adder-cost: 39   maxlim: 1278   bits: 12/11
c ---[ 797]---> Adder-cost: 26   maxlim: 7678   bits: 14/13
c ---[ 796]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 795]---> Adder-cost: 26   maxlim: 5246   bits: 14/13
c ---[ 793]---> Adder-cost: 24   maxlim: 2558   bits: 13/12
c ---[ 791]---> Adder-cost: 26   maxlim: 4350   bits: 14/13
c ---[ 790]---> Adder-cost: 24   maxlim: 2942   bits: 13/12
c ---[ 789]---> Adder-cost: 35   maxlim: 638   bits: 11/10
c ---[ 788]---> Adder-cost: 43   maxlim: 3710   bits: 13/12
c ---[ 787]---> Adder-cost: 26   maxlim: 7422   bits: 14/13
c ---[ 786]---> Adder-cost: 26   maxlim: 5886   bits: 14/13
c ---[ 785]---> Adder-cost: 26   maxlim: 6014   bits: 14/13
c ---[ 784]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 782]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[ 781]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 780]---> Adder-cost: 22   maxlim: 1918   bits: 12/11
c ---[ 779]---> Adder-cost: 26   maxlim: 6270   bits: 14/13
c ---[ 778]---> Adder-cost: 26   maxlim: 6398   bits: 14/13
c ---[ 777]---> Adder-cost: 22   maxlim: 1918   bits: 12/11
c ---[ 776]---> Adder-cost: 22   maxlim: 1662   bits: 12/11
c ---[ 774]---> Adder-cost: 26   maxlim: 6782   bits: 14/13
c ---[ 772]---> Adder-cost: 24   maxlim: 2174   bits: 13/12
c ---[ 771]---> Adder-cost: 26   maxlim: 5758   bits: 14/13
c ---[ 770]---> Adder-cost: 26   maxlim: 7294   bits: 14/13
c ---[ 769]---> Adder-cost: 26   maxlim: 4478   bits: 14/13
c ---[ 768]---> Adder-cost: 26   maxlim: 7678   bits: 14/13
c ---[ 767]---> Adder-cost: 37   maxlim: 766   bits: 11/10
c ---[ 766]---> Adder-cost: 26   maxlim: 5630   bits: 14/13
c ---[ 764]---> Adder-cost: 26   maxlim: 5886   bits: 14/13
c ---[ 763]---> Adder-cost: 35   maxlim: 510   bits: 10/9
c ---[ 762]---> Adder-cost: 26   maxlim: 7806   bits: 14/13
c ---[ 761]---> Adder-cost: 26   maxlim: 5246   bits: 14/13
c ---[ 760]---> Adder-cost: 26   maxlim: 4478   bits: 14/13
c ---[ 759]---> Adder-cost: 41   maxlim: 1534   bits: 12/11
c ---[ 758]---> Adder-cost: 39   maxlim: 1278   bits: 12/11
c ---[ 757]---> Adder-cost: 22   maxlim: 1662   bits: 12/11
c ---[ 756]---> Adder-cost: 41   maxlim: 1918   bits: 12/11
c ---[ 754]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[ 753]---> Adder-cost: 26   maxlim: 6014   bits: 14/13
c ---[ 752]---> Adder-cost: 26   maxlim: 7294   bits: 14/13
c ---[ 751]---> Adder-cost: 33   maxlim: 382   bits: 10/9
c ---[ 750]---> Adder-cost: 24   maxlim: 3198   bits: 13/12
c ---[ 749]---> Adder-cost: 26   maxlim: 8062   bits: 14/13
c ---[ 747]---> Adder-cost: 24   maxlim: 3710   bits: 13/12
c ---[ 746]---> Adder-cost: 24   maxlim: 2558   bits: 13/12
c ---[ 745]---> Adder-cost: 24   maxlim: 2686   bits: 13/12
c ---[ 744]---> Adder-cost: 22   maxlim: 1406   bits: 12/11
c ---[ 743]---> Adder-cost: 24   maxlim: 2174   bits: 13/12
c ---[ 742]---> Adder-cost: 26   maxlim: 6782   bits: 14/13
c ---[ 741]---> Adder-cost: 22   maxlim: 1278   bits: 12/11
c ---[ 740]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[ 738]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[ 737]---> Adder-cost: 24   maxlim: 2430   bits: 13/12
c ---[ 736]---> Adder-cost: 24   maxlim: 2174   bits: 13/12
c ---[ 734]---> Adder-cost: 35   maxlim: 638   bits: 11/10
c ---[ 733]---> Adder-cost: 24   maxlim: 2174   bits: 13/12
c ---[ 732]---> Adder-cost: 37   maxlim: 894   bits: 11/10
c ---[ 730]---> Adder-cost: 41   maxlim: 1790   bits: 12/11
c ---[ 729]---> Adder-cost: 35   maxlim: 510   bits: 10/9
c ---[ 728]---> Adder-cost: 24   maxlim: 3582   bits: 13/12
c ---[ 727]---> Adder-cost: 37   maxlim: 1150   bits: 12/11
c ---[ 726]---> Adder-cost: 24   maxlim: 2302   bits: 13/12
c ---[ 725]---> Adder-cost: 35   maxlim: 638   bits: 11/10
c ---[ 723]---> Adder-cost: 26   maxlim: 4734   bits: 14/13
c ---[ 722]---> Adder-cost: 24   maxlim: 3198   bits: 13/12
c ---[ 721]---> Adder-cost: 26   maxlim: 7934   bits: 14/13
c ---[ 720]---> Adder-cost: 26   maxlim: 6654   bits: 14/13
c ---[ 719]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[ 718]---> Adder-cost: 26   maxlim: 5886   bits: 14/13
c ---[ 717]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[ 716]---> Adder-cost: 22   maxlim: 1918   bits: 12/11
c ---[ 713]---> Adder-cost: 24   maxlim: 2430   bits: 13/12
c ---[ 712]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 711]---> Adder-cost: 41   maxlim: 1534   bits: 12/11
c ---[ 710]---> Adder-cost: 41   maxlim: 1790   bits: 12/11
c ---[ 708]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[ 706]---> Adder-cost: 26   maxlim: 6910   bits: 14/13
c ---[ 705]---> Adder-cost: 26   maxlim: 6270   bits: 14/13
c ---[ 704]---> Adder-cost: 35   maxlim: 510   bits: 10/9
c ---[ 703]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 702]---> Adder-cost: 26   maxlim: 6782   bits: 14/13
c ---[ 701]---> Adder-cost: 26   maxlim: 5630   bits: 14/13
c ---[ 700]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 699]---> Adder-cost: 41   maxlim: 1534   bits: 12/11
c ---[ 698]---> Adder-cost: 26   maxlim: 7550   bits: 14/13
c ---[ 695]---> Adder-cost: 22   maxlim: 1790   bits: 12/11
c ---[ 694]---> Adder-cost: 41   maxlim: 1790   bits: 12/11
c ---[ 693]---> Adder-cost: 26   maxlim: 8062   bits: 14/13
c ---[ 692]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 691]---> Adder-cost: 26   maxlim: 6782   bits: 14/13
c ---[ 690]---> Adder-cost: 24   maxlim: 2430   bits: 13/12
c ---[ 688]---> Adder-cost: 41   maxlim: 1918   bits: 12/11
c ---[ 687]---> Adder-cost: 37   maxlim: 894   bits: 11/10
c ---[ 686]---> Adder-cost: 26   maxlim: 7294   bits: 14/13
c ---[ 684]---> Adder-cost: 26   maxlim: 6782   bits: 14/13
c ---[ 683]---> Adder-cost: 22   maxlim: 1662   bits: 12/11
c ---[ 682]---> Adder-cost: 22   maxlim: 1406   bits: 12/11
c ---[ 681]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 680]---> Adder-cost: 26   maxlim: 7806   bits: 14/13
c ---[ 679]---> Adder-cost: 24   maxlim: 3454   bits: 13/12
c ---[ 678]---> Adder-cost: 24   maxlim: 3838   bits: 13/12
c ---[ 677]---> Adder-cost: 24   maxlim: 2558   bits: 13/12
c ---[ 676]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 675]---> Adder-cost: 24   maxlim: 2686   bits: 13/12
c ---[ 673]---> Adder-cost: 22   maxlim: 1662   bits: 12/11
c ---[ 672]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 671]---> Adder-cost: 26   maxlim: 4990   bits: 14/13
c ---[ 670]---> Adder-cost: 26   maxlim: 7934   bits: 14/13
c ---[ 668]---> Adder-cost: 26   maxlim: 5630   bits: 14/13
c ---[ 667]---> Adder-cost: 26   maxlim: 7934   bits: 14/13
c ---[ 666]---> Adder-cost: 37   maxlim: 766   bits: 11/10
c ---[ 665]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[ 664]---> Adder-cost: 24   maxlim: 3582   bits: 13/12
c ---[ 663]---> Adder-cost: 26   maxlim: 5886   bits: 14/13
c ---[ 662]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 661]---> Adder-cost: 24   maxlim: 2814   bits: 13/12
c ---[ 660]---> Adder-cost: 37   maxlim: 766   bits: 11/10
c ---[ 659]---> Adder-cost: 26   maxlim: 6654   bits: 14/13
c ---[ 658]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[ 657]---> Adder-cost: 41   maxlim: 1534   bits: 12/11
c ---[ 656]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 655]---> Adder-cost: 43   maxlim: 2046   bits: 12/11
c ---[ 654]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[ 653]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[ 651]---> Adder-cost: 37   maxlim: 1150   bits: 12/11
c ---[ 649]---> Adder-cost: 24   maxlim: 3198   bits: 13/12
c ---[ 648]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[ 647]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[ 645]---> Adder-cost: 26   maxlim: 6398   bits: 14/13
c ---[ 644]---> Adder-cost: 33   maxlim: 382   bits: 10/9
c ---[ 643]---> Adder-cost: 26   maxlim: 5758   bits: 14/13
c ---[ 642]---> Adder-cost: 26   maxlim: 4862   bits: 14/13
c ---[ 640]---> Adder-cost: 24   maxlim: 3582   bits: 13/12
c ---[ 638]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[ 637]---> Adder-cost: 24   maxlim: 3582   bits: 13/12
c ---[ 636]---> Adder-cost: 26   maxlim: 6910   bits: 14/13
c ---[ 635]---> Adder-cost: 24   maxlim: 2302   bits: 13/12
c ---[ 634]---> Adder-cost: 35   maxlim: 638   bits: 11/10
c ---[ 633]---> Adder-cost: 24   maxlim: 2942   bits: 13/12
c ---[ 632]---> Adder-cost: 26   maxlim: 5630   bits: 14/13
c ---[ 631]---> Adder-cost: 39   maxlim: 1406   bits: 12/11
c ---[ 630]---> Adder-cost: 26   maxlim: 8062   bits: 14/13
c ---[ 628]---> Adder-cost: 24   maxlim: 2686   bits: 13/12
c ---[ 627]---> Adder-cost: 26   maxlim: 5630   bits: 14/13
c ---[ 625]---> Adder-cost: 26   maxlim: 7294   bits: 14/13
c ---[ 624]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 623]---> Adder-cost: 24   maxlim: 3710   bits: 13/12
c ---[ 622]---> Adder-cost: 24   maxlim: 3198   bits: 13/12
c ---[ 621]---> Adder-cost: 35   maxlim: 510   bits: 10/9
c ---[ 620]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[ 619]---> Adder-cost: 26   maxlim: 7422   bits: 14/13
c ---[ 618]---> Adder-cost: 22   maxlim: 1278   bits: 12/11
c ---[ 617]---> Adder-cost: 37   maxlim: 894   bits: 11/10
c ---[ 616]---> Adder-cost: 26   maxlim: 7934   bits: 14/13
c ---[ 615]---> Adder-cost: 26   maxlim: 7934   bits: 14/13
c ---[ 614]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[ 613]---> Adder-cost: 41   maxlim: 1918   bits: 12/11
c ---[ 608]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[ 607]---> Adder-cost: 26   maxlim: 4222   bits: 14/13
c ---[ 606]---> Adder-cost: 39   maxlim: 1022   bits: 11/10
c ---[ 605]---> Adder-cost: 45   maxlim: 3838   bits: 13/12
c ---[ 604]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 603]---> Adder-cost: 45   maxlim: 3966   bits: 13/12
c ---[ 602]---> Adder-cost: 26   maxlim: 6910   bits: 14/13
c ---[ 601]---> Adder-cost: 26   maxlim: 7550   bits: 14/13
c ---[ 600]---> Adder-cost: 35   maxlim: 510   bits: 10/9
c ---[ 598]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 596]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 595]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 594]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 593]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 592]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 591]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 590]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 589]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 588]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 587]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 586]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 584]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 583]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 582]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 581]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 580]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 579]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 578]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 577]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 576]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 575]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 574]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 572]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 571]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 570]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 569]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 568]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 567]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 566]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 565]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 564]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 563]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 562]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 560]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 559]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 558]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 557]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 556]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 555]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 554]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 553]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 552]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 551]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 550]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 548]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 547]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 546]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 545]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 544]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 543]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 542]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 541]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 540]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 539]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 538]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 536]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 535]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 534]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 533]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 532]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 531]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 530]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 529]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 528]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 527]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 526]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 524]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 523]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 522]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 521]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 520]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 519]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 518]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 517]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 516]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 515]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 514]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 512]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 511]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 510]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 509]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 508]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 507]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 506]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 505]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 504]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 503]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 502]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 500]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 499]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 498]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 497]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 496]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 495]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 494]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 493]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 492]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 491]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 490]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 488]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 487]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 486]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 485]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 484]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 483]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 482]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 481]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 480]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 479]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 478]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 476]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 474]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 473]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 472]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 471]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 470]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 469]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 468]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 467]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 466]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 465]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 464]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 462]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 461]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 460]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 459]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 458]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 457]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 456]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 455]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 454]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 453]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 452]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 450]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 449]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 448]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 447]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 446]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 445]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 444]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 443]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 442]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 441]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 440]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 438]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 437]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 436]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 435]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 434]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 433]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 432]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 431]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 430]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 429]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 428]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 426]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 425]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 424]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 423]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 422]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 421]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 420]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 419]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 418]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 417]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 416]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 414]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 413]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 412]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 411]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 410]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 409]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 408]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 407]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 406]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 405]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 404]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 402]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 401]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 400]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 399]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 398]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 397]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 396]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 395]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 394]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 393]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 392]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 390]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 389]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 388]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 387]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 386]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 385]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 384]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 383]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 382]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 381]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 380]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 378]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 377]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 376]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 375]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 374]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 373]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 372]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 371]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 370]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 369]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 368]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 366]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 365]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 364]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 363]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 362]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 361]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 360]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 359]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 358]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 357]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 356]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 354]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 352]---> Adder-cost: 693   maxlim: 102262   bits: 18/17
c ---[ 351]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 350]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 349]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 348]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 347]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 346]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 345]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 344]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 343]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 342]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 340]---> Adder-cost: 572   maxlim: 148723   bits: 18/18
c ---[ 339]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 338]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 337]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 336]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 335]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 334]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 333]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 332]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 331]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 330]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 328]---> Adder-cost: 880   maxlim: 181231   bits: 19/18
c ---[ 327]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 326]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 325]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 324]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 323]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 322]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 321]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 320]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 319]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 318]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 316]---> Adder-cost: 820   maxlim: 146161   bits: 19/18
c ---[ 315]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 314]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 313]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 312]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 311]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 310]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 309]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 308]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 307]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 306]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 304]---> Adder-cost: 838   maxlim: 185456   bits: 19/18
c ---[ 303]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 302]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 301]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 300]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 299]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 298]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 297]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 296]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 295]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 294]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 292]---> Adder-cost: 546   maxlim: 93302   bits: 18/17
c ---[ 291]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 290]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 289]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 288]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 287]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 286]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 285]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 284]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 283]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 282]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 280]---> Adder-cost: 720   maxlim: 163185   bits: 19/18
c ---[ 279]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 278]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 277]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 276]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 275]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 274]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 273]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 272]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 271]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 270]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 268]---> Adder-cost: 768   maxlim: 162802   bits: 19/18
c ---[ 267]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 266]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 265]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 264]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 263]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 262]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 261]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 260]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 259]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 258]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 256]---> Adder-cost: 800   maxlim: 202094   bits: 19/18
c ---[ 255]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 254]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 253]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 252]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 251]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 250]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 249]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 248]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 247]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 246]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 244]---> Adder-cost: 670   maxlim: 163442   bits: 19/18
c ---[ 243]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 242]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 241]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 240]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 239]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 238]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 237]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 236]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 235]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 234]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 232]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 230]---> Adder-cost: 706   maxlim: 157169   bits: 19/18
c ---[ 229]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 228]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 227]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 226]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 225]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 224]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 223]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 222]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 221]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 220]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 218]---> Adder-cost: 762   maxlim: 147056   bits: 19/18
c ---[ 217]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 216]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 215]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 214]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 213]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 212]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 211]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 210]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 209]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 208]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 206]---> Adder-cost: 759   maxlim: 130929   bits: 18/17
c ---[ 205]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 204]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 203]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 202]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 201]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 200]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 199]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 198]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 197]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 196]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 194]---> Adder-cost: 696   maxlim: 101365   bits: 18/17
c ---[ 193]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 192]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 191]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 190]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 189]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 188]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 187]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 186]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 185]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 184]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 182]---> Adder-cost: 614   maxlim: 144627   bits: 19/18
c ---[ 181]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 180]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 179]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 178]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 177]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 176]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 175]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 174]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 173]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 172]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 170]---> Adder-cost: 764   maxlim: 174961   bits: 19/18
c ---[ 169]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 168]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 167]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 166]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 165]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 164]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 163]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 162]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 161]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 160]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 158]---> Adder-cost: 548   maxlim: 159603   bits: 18/18
c ---[ 157]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 156]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 155]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 154]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 153]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 152]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 151]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 150]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 149]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 148]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 146]---> Adder-cost: 824   maxlim: 173423   bits: 19/18
c ---[ 145]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 144]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 143]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 142]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 141]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 140]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 139]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 138]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 137]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 136]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 134]---> Adder-cost: 858   maxlim: 137074   bits: 19/18
c ---[ 132]---> Adder-cost: 786   maxlim: 177902   bits: 19/18
c ---[ 130]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 128]---> Adder-cost: 602   maxlim: 120053   bits: 18/17
c ---[ 126]---> Adder-cost: 646   maxlim: 154865   bits: 18/18
c ---[ 124]---> Adder-cost: 864   maxlim: 214125   bits: 19/18
c ---[ 122]---> Adder-cost: 710   maxlim: 143089   bits: 19/18
c ---[ 120]---> Adder-cost: 614   maxlim: 83701   bits: 18/17
c ---[ 118]---> Adder-cost: 706   maxlim: 144239   bits: 19/18
c ---[ 116]---> Adder-cost: 826   maxlim: 169330   bits: 19/18
c ---[ 114]---> Adder-cost: 604   maxlim: 130932   bits: 18/17
c ---[ 112]---> Adder-cost: 816   maxlim: 175726   bits: 19/18
c ---[ 111]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 109]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 108]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 107]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 106]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 105]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 104]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 103]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 102]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 101]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 100]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[  99]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[  97]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[  96]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[  95]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[  94]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  93]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  92]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  91]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  90]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  89]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[  88]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[  87]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  85]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  84]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  83]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[  82]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[  81]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  80]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[  79]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[  78]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  77]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[  76]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  75]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  73]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[  72]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  71]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  70]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[  69]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  68]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  67]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  66]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  65]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  64]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  63]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[  62]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[  61]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[  60]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  59]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  58]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  57]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  56]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  55]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[  54]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  53]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[  52]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  51]---> Adder-cost: 20   maxlim: 894   bits: 11/10
c ---[  50]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[  49]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  48]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  47]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[  46]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[  45]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  44]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  43]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  42]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  41]---> Adder-cost: 20   maxlim: 894   bits: 11/10
c ---[  40]---> Adder-cost: 20   maxlim: 894   bits: 11/10
c ---[  39]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  38]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[  37]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  36]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[  35]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[  34]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  33]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  32]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  31]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  30]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  29]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  28]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  27]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  26]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  25]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  24]---> Adder-cost: 20   maxlim: 894   bits: 11/10
c ---[  23]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  22]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[  21]---> Adder-cost: 20   maxlim: 894   bits: 11/10
c ---[  20]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  19]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[  18]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 20   maxlim: 638   bits: 11/10
c ---[  16]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  15]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  14]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  13]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  12]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  11]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[  10]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[   9]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[   8]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[   7]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[   6]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[   5]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[   4]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ---[   3]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[   2]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[   1]---> Adder-cost: 18   maxlim: 382   bits: 10/9
c ---[   0]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  245559   916090 |   81853       0        0     nan |  0.000 % |
c |       104 |  245559   916090 |   90038     104      552     5.3 | 20.458 % |
c |       259 |  245559   916090 |   99042     259     1404     5.4 | 20.458 % |
c |       484 |  245559   916090 |  108946     484     2434     5.0 | 20.458 % |
c |       821 |  245521   915962 |  119840     816     3516     4.3 | 20.467 % |
c |      1327 |  245482   915831 |  131825    1317     5302     4.0 | 20.478 % |
c |      2086 |  245442   915701 |  145007    2071     8025     3.9 | 20.489 % |
c |      3225 |  245402   915567 |  159508    3205    12426     3.9 | 20.500 % |
c |      4933 |  245279   915154 |  175459    4900    23856     4.9 | 20.538 % |
c |      7495 |  245138   914691 |  193005    7445    43726     5.9 | 20.584 % |
c |     11339 |  245001   914234 |  212305   11240    99846     8.9 | 20.627 % |
c |     17106 |  244969   914128 |  233536   16989   291929    17.2 | 20.637 % |
c |     25755 |  244909   913918 |  256889   25622   596108    23.3 | 20.655 % |
c |     38729 |  244668   913093 |  282578   38429   991230    25.8 | 20.720 % |
c |     58190 |  244466   912425 |  310836   57837  1740691    30.1 | 20.782 % |
c |     87382 |  244404   912217 |  341920   87012  3595927    41.3 | 20.799 % |
c |    131171 |  244249   911696 |  376112  130726  6067928    46.4 | 20.845 % |
c |    196856 |  244047   911018 |  413723  196342  9948023    50.7 | 20.907 % |
c |    295382 |  243937   910648 |  455095  294833 14788471    50.2 | 20.935 % |
c |    443174 |  243836   910301 |  500605  442573 23213837    52.5 | 20.961 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.95 2/55 1165
Raw data (stat): 1165 (runsolver) R 1164 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546698731 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 6539 0 0 0 980 18 0 0 25 0 1 0 546698731 27889664 6157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6809 6157 603 41 0 6768 0
vsize: 27236
[startup+19.9994 s]
Raw data (loadavg): 0.89 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 6717 0 0 0 1979 19 0 0 25 0 1 0 546698731 28741632 6335 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7017 6335 603 41 0 6976 0
vsize: 28068
[startup+30.0002 s]
Raw data (loadavg): 0.91 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 7553 0 0 0 2976 21 0 0 25 0 1 0 546698731 32157696 7171 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7851 7171 603 41 0 7810 0
vsize: 31404
[startup+40 s]
Raw data (loadavg): 0.92 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 8021 0 0 0 3974 23 0 0 25 0 1 0 546698731 34172928 7639 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8343 7639 603 41 0 8302 0
vsize: 33372
[startup+49.9993 s]
Raw data (loadavg): 0.93 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 8397 0 0 0 4974 24 0 0 25 0 1 0 546698731 35659776 8015 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8706 8015 603 41 0 8665 0
vsize: 34824
[startup+59.9989 s]
Raw data (loadavg): 0.94 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 9045 0 0 0 5973 25 0 0 25 0 1 0 546698731 38232064 8663 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9334 8663 603 41 0 9293 0
vsize: 37336
[startup+69.9987 s]
Raw data (loadavg): 0.95 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 10030 0 0 0 6971 27 0 0 25 0 1 0 546698731 42532864 9648 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10384 9648 603 41 0 10343 0
vsize: 41536
[startup+79.999 s]
Raw data (loadavg): 0.96 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 10826 0 0 0 7968 29 0 0 25 0 1 0 546698731 45776896 10444 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11176 10444 603 41 0 11135 0
vsize: 44704
[startup+89.9986 s]
Raw data (loadavg): 0.96 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 11293 0 0 0 8968 30 0 0 25 0 1 0 546698731 47665152 10911 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11637 10911 603 41 0 11596 0
vsize: 46548
[startup+99.9986 s]
Raw data (loadavg): 0.97 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 11938 0 0 0 9965 33 0 0 25 0 1 0 546698731 50221056 11556 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12261 11556 603 41 0 12220 0
vsize: 49044
[startup+109.999 s]
Raw data (loadavg): 0.97 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 12423 0 0 0 10964 34 0 0 25 0 1 0 546698731 52248576 12041 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12756 12041 603 41 0 12715 0
vsize: 51024
[startup+119.998 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 12932 0 0 0 11962 37 0 0 25 0 1 0 546698731 54415360 12550 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13285 12550 603 41 0 13244 0
vsize: 53140
[startup+129.998 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 13287 0 0 0 12961 38 0 0 25 0 1 0 546698731 55775232 12905 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13617 12905 603 41 0 13576 0
vsize: 54468
[startup+139.998 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 1165
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 13676 0 0 0 13960 39 0 0 25 0 1 0 546698731 57393152 13294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14012 13294 603 41 0 13971 0
vsize: 56048
[startup+149.997 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 1167
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 14158 0 0 0 14958 41 0 0 25 0 1 0 546698731 59424768 13776 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14508 13776 603 41 0 14467 0
vsize: 58032
[startup+159.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 1167
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 14393 0 0 0 15958 41 0 0 25 0 1 0 546698731 60379136 14011 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14741 14011 603 41 0 14700 0
vsize: 58964
[startup+169.997 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 1167
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 14645 0 0 0 16957 42 0 0 25 0 1 0 546698731 61992960 14263 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15135 14263 603 41 0 15094 0
vsize: 60540
[startup+179.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 1167
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 14888 0 0 0 17955 44 0 0 25 0 1 0 546698731 62926848 14506 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15363 14506 603 41 0 15322 0
vsize: 61452
[startup+189.996 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 1167
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 15101 0 0 0 18955 44 0 0 25 0 1 0 546698731 63860736 14719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15591 14719 603 41 0 15550 0
vsize: 62364
[startup+199.995 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 1167
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 15342 0 0 0 19954 45 0 0 25 0 1 0 546698731 64929792 14960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15852 14960 603 41 0 15811 0
vsize: 63408
[startup+209.995 s]
Raw data (loadavg): 1.07 0.99 0.95 2/55 1220
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 15553 0 0 0 20953 46 0 0 25 0 1 0 546698731 65732608 15171 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16048 15171 603 41 0 16007 0
vsize: 64192
[startup+219.995 s]
Raw data (loadavg): 1.06 0.99 0.95 2/55 1220
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 15886 0 0 0 21952 47 0 0 25 0 1 0 546698731 67108864 15504 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16384 15504 603 41 0 16343 0
vsize: 65536
[startup+229.996 s]
Raw data (loadavg): 1.05 0.99 0.95 2/55 1220
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 16136 0 0 0 22952 48 0 0 25 0 1 0 546698731 68063232 15754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16617 15754 603 41 0 16576 0
vsize: 66468
[startup+239.996 s]
Raw data (loadavg): 1.04 0.99 0.95 2/55 1220
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 16422 0 0 0 23951 49 0 0 25 0 1 0 546698731 69287936 16040 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16916 16040 603 41 0 16875 0
vsize: 67664
[startup+249.996 s]
Raw data (loadavg): 1.04 0.99 0.95 2/55 1220
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 16703 0 0 0 24950 50 0 0 25 0 1 0 546698731 70377472 16321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17182 16321 603 41 0 17141 0
vsize: 68728
[startup+259.995 s]
Raw data (loadavg): 1.03 0.99 0.95 2/55 1220
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 16936 0 0 0 25949 51 0 0 25 0 1 0 546698731 71450624 16554 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17444 16554 603 41 0 17403 0
vsize: 69776
[startup+269.995 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 1220
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 17171 0 0 0 26948 52 0 0 25 0 1 0 546698731 72323072 16789 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17657 16789 603 41 0 17616 0
vsize: 70628
[startup+279.995 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 17420 0 0 0 27947 53 0 0 25 0 1 0 546698731 73449472 17038 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17932 17038 603 41 0 17891 0
vsize: 71728
[startup+289.996 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 17605 0 0 0 28946 54 0 0 25 0 1 0 546698731 74227712 17223 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18122 17223 603 41 0 18081 0
vsize: 72488
[startup+299.996 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 17803 0 0 0 29946 55 0 0 25 0 1 0 546698731 75030528 17421 4294967295 134512640 134672761 3221224544 3221223648 134560364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18318 17421 603 41 0 18277 0
vsize: 73272
[startup+309.996 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 18044 0 0 0 30945 56 0 0 25 0 1 0 546698731 76165120 17662 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18595 17662 603 41 0 18554 0
vsize: 74380
[startup+319.997 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 18241 0 0 0 31945 56 0 0 25 0 1 0 546698731 76972032 17859 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18792 17859 603 41 0 18751 0
vsize: 75168
[startup+329.997 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 18481 0 0 0 32944 57 0 0 25 0 1 0 546698731 77971456 18099 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19036 18099 603 41 0 18995 0
vsize: 76144
[startup+339.997 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 18596 0 0 0 33944 58 0 0 25 0 1 0 546698731 78385152 18214 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19137 18214 603 41 0 19096 0
vsize: 76548
[startup+349.997 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 18876 0 0 0 34943 59 0 0 25 0 1 0 546698731 79638528 18494 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19443 18494 603 41 0 19402 0
vsize: 77772
[startup+359.997 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 19127 0 0 0 35942 60 0 0 25 0 1 0 546698731 80744448 18745 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19713 18745 603 41 0 19672 0
vsize: 78852
[startup+369.997 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 19300 0 0 0 36942 60 0 0 25 0 1 0 546698731 81416192 18918 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19877 18918 603 41 0 19836 0
vsize: 79508
[startup+379.998 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 19487 0 0 0 37941 61 0 0 25 0 1 0 546698731 82087936 19105 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20041 19105 603 41 0 20000 0
vsize: 80164
[startup+389.998 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 19696 0 0 0 38941 61 0 0 25 0 1 0 546698731 83046400 19314 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20275 19314 603 41 0 20234 0
vsize: 81100
[startup+399.998 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 19898 0 0 0 39940 62 0 0 25 0 1 0 546698731 83857408 19516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20473 19516 603 41 0 20432 0
vsize: 81892
[startup+409.999 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 20182 0 0 0 40940 62 0 0 25 0 1 0 546698731 84934656 19800 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20736 19800 603 41 0 20695 0
vsize: 82944
[startup+419.998 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 20734 0 0 0 41939 64 0 0 25 0 1 0 546698731 87224320 20352 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21295 20352 603 41 0 21254 0
vsize: 85180
[startup+429.998 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 21467 0 0 0 42937 66 0 0 25 0 1 0 546698731 90083328 21085 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21993 21085 603 41 0 21952 0
vsize: 87972
[startup+439.998 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1222
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 21725 0 0 0 43936 67 0 0 25 0 1 0 546698731 91164672 21343 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22257 21343 603 41 0 22216 0
vsize: 89028
[startup+449.998 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1224
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 21889 0 0 0 44935 68 0 0 25 0 1 0 546698731 91848704 21507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22424 21507 603 41 0 22383 0
vsize: 89696
[startup+459.998 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1224
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 22063 0 0 0 45935 69 0 0 25 0 1 0 546698731 92512256 21681 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22586 21681 603 41 0 22545 0
vsize: 90344
[startup+469.998 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1224
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 22223 0 0 0 46935 69 0 0 25 0 1 0 546698731 93237248 21841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22763 21841 603 41 0 22722 0
vsize: 91052
[startup+479.999 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1224
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 22379 0 0 0 47934 69 0 0 25 0 1 0 546698731 93900800 21997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22925 21997 603 41 0 22884 0
vsize: 91700
[startup+490.001 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1224
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 22523 0 0 0 48934 70 0 0 25 0 1 0 546698731 94453760 22141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23060 22141 603 41 0 23019 0
vsize: 92240
[startup+500.001 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1224
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 22783 0 0 0 49934 71 0 0 25 0 1 0 546698731 95592448 22401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23338 22401 603 41 0 23297 0
vsize: 93352
[startup+510.001 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1224
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 22932 0 0 0 50934 71 0 0 25 0 1 0 546698731 96235520 22550 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23495 22550 603 41 0 23454 0
vsize: 93980
[startup+520.001 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1224
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 23090 0 0 0 51933 71 0 0 25 0 1 0 546698731 97968128 22708 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23918 22708 603 41 0 23877 0
vsize: 95672
[startup+530.002 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 23508 0 0 0 52933 72 0 0 25 0 1 0 546698731 99758080 23126 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24355 23126 603 41 0 24314 0
vsize: 97420
[startup+540.001 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 24074 0 0 0 53932 73 0 0 25 0 1 0 546698731 102105088 23692 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24928 23692 603 41 0 24887 0
vsize: 99712
[startup+550.001 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 24365 0 0 0 54931 74 0 0 25 0 1 0 546698731 103182336 23983 4294967295 134512640 134672761 3221224544 3221223616 134553553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25191 23983 603 41 0 25150 0
vsize: 100764
[startup+560.001 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 24585 0 0 0 55931 75 0 0 25 0 1 0 546698731 104112128 24203 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25418 24203 603 41 0 25377 0
vsize: 101672
[startup+570.001 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 24797 0 0 0 56930 76 0 0 25 0 1 0 546698731 104923136 24415 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25616 24415 603 41 0 25575 0
vsize: 102464
[startup+580.002 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 25085 0 0 0 57929 77 0 0 25 0 1 0 546698731 106135552 24703 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 24703 603 41 0 25871 0
vsize: 103648
[startup+590.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 25404 0 0 0 58928 77 0 0 25 0 1 0 546698731 107372544 25022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26214 25022 603 41 0 26173 0
vsize: 104856
[startup+600.002 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 25684 0 0 0 59927 79 0 0 25 0 1 0 546698731 108593152 25302 4294967295 134512640 134672761 3221224544 3221223760 134558229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26512 25302 603 41 0 26471 0
vsize: 106048
[startup+610.002 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 25904 0 0 0 60927 79 0 0 25 0 1 0 546698731 109445120 25522 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26720 25522 603 41 0 26679 0
vsize: 106880
[startup+620.002 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 26125 0 0 0 61926 80 0 0 25 0 1 0 546698731 110432256 25743 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26961 25743 603 41 0 26920 0
vsize: 107844
[startup+630.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 26263 0 0 0 62926 80 0 0 25 0 1 0 546698731 110960640 25881 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27090 25881 603 41 0 27049 0
vsize: 108360
[startup+640.002 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 26404 0 0 0 63926 81 0 0 25 0 1 0 546698731 111497216 26022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27221 26022 603 41 0 27180 0
vsize: 108884
[startup+650.002 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 26889 0 0 0 64925 82 0 0 25 0 1 0 546698731 113512448 26507 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27713 26507 603 41 0 27672 0
vsize: 110852
[startup+660.002 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 27278 0 0 0 65924 84 0 0 25 0 1 0 546698731 115126272 26896 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28107 26896 603 41 0 28066 0
vsize: 112428
[startup+670.002 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 27610 0 0 0 66923 84 0 0 25 0 1 0 546698731 116469760 27228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28435 27228 603 41 0 28394 0
vsize: 113740
[startup+680.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 27926 0 0 0 67923 85 0 0 25 0 1 0 546698731 117821440 27544 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28765 27544 603 41 0 28724 0
vsize: 115060
[startup+690.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 28354 0 0 0 68921 86 0 0 25 0 1 0 546698731 119463936 27972 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29166 27972 603 41 0 29125 0
vsize: 116664
[startup+700.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 28582 0 0 0 69921 87 0 0 25 0 1 0 546698731 120414208 28200 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29398 28200 603 41 0 29357 0
vsize: 117592
[startup+710.004 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 28696 0 0 0 70921 87 0 0 25 0 1 0 546698731 120942592 28314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29527 28314 603 41 0 29486 0
vsize: 118108
[startup+720.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 28976 0 0 0 71920 88 0 0 25 0 1 0 546698731 122028032 28594 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29792 28594 603 41 0 29751 0
vsize: 119168
[startup+730.004 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 29333 0 0 0 72919 90 0 0 25 0 1 0 546698731 123523072 28951 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30157 28951 603 41 0 30116 0
vsize: 120628
[startup+740.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1226
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 29568 0 0 0 73918 91 0 0 25 0 1 0 546698731 124489728 29186 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30393 29186 603 41 0 30352 0
vsize: 121572
[startup+750.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 29759 0 0 0 74918 91 0 0 25 0 1 0 546698731 125161472 29377 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30557 29377 603 41 0 30516 0
vsize: 122228
[startup+760.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 29928 0 0 0 75918 91 0 0 25 0 1 0 546698731 125919232 29546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30742 29546 603 41 0 30701 0
vsize: 122968
[startup+770.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 30068 0 0 0 76918 92 0 0 25 0 1 0 546698731 126451712 29686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30872 29686 603 41 0 30831 0
vsize: 123488
[startup+780.004 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 30178 0 0 0 77917 92 0 0 25 0 1 0 546698731 126988288 29796 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31003 29796 603 41 0 30962 0
vsize: 124012
[startup+790.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 30329 0 0 0 78917 92 0 0 25 0 1 0 546698731 127545344 29947 4294967295 134512640 134672761 3221224544 3221223648 134560352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31139 29947 603 41 0 31098 0
vsize: 124556
[startup+800.003 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 30460 0 0 0 79917 93 0 0 25 0 1 0 546698731 128077824 30078 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31269 30078 603 41 0 31228 0
vsize: 125076
[startup+810.004 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 30615 0 0 0 80917 93 0 0 25 0 1 0 546698731 128761856 30233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31436 30233 603 41 0 31395 0
vsize: 125744
[startup+820.003 s]
Raw data (loadavg): 1.08 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 30752 0 0 0 81917 94 0 0 25 0 1 0 546698731 129302528 30370 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31568 30370 603 41 0 31527 0
vsize: 126272
[startup+830.004 s]
Raw data (loadavg): 1.07 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 30907 0 0 0 82916 94 0 0 25 0 1 0 546698731 130048000 30525 4294967295 134512640 134672761 3221224544 3221223616 134553553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31750 30525 603 41 0 31709 0
vsize: 127000
[startup+840.004 s]
Raw data (loadavg): 1.06 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 31212 0 0 0 83915 95 0 0 25 0 1 0 546698731 131436544 30830 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32089 30830 603 41 0 32048 0
vsize: 128356
[startup+850.004 s]
Raw data (loadavg): 1.05 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 31521 0 0 0 84915 96 0 0 25 0 1 0 546698731 132698112 31139 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32397 31139 603 41 0 32356 0
vsize: 129588
[startup+860.004 s]
Raw data (loadavg): 1.04 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 31808 0 0 0 85914 97 0 0 25 0 1 0 546698731 133840896 31426 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32676 31426 603 41 0 32635 0
vsize: 130704
[startup+870.004 s]
Raw data (loadavg): 1.03 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 32195 0 0 0 86913 98 0 0 25 0 1 0 546698731 135454720 31813 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33070 31813 603 41 0 33029 0
vsize: 132280
[startup+880.004 s]
Raw data (loadavg): 1.03 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 32807 0 0 0 87910 101 0 0 25 0 1 0 546698731 137887744 32425 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33664 32425 603 41 0 33623 0
vsize: 134656
[startup+890.004 s]
Raw data (loadavg): 1.02 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 33199 0 0 0 88909 103 0 0 25 0 1 0 546698731 139501568 32817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34058 32817 603 41 0 34017 0
vsize: 136232
[startup+900.004 s]
Raw data (loadavg): 1.02 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 33348 0 0 0 89908 104 0 0 25 0 1 0 546698731 140173312 32966 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34222 32966 603 41 0 34181 0
vsize: 136888
[startup+910.004 s]
Raw data (loadavg): 1.02 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 33496 0 0 0 90908 104 0 0 25 0 1 0 546698731 140795904 33114 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34374 33114 603 41 0 34333 0
vsize: 137496
[startup+920.003 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 33667 0 0 0 91908 105 0 0 25 0 1 0 546698731 141463552 33285 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34537 33285 603 41 0 34496 0
vsize: 138148
[startup+930.003 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 33770 0 0 0 92907 105 0 0 25 0 1 0 546698731 141901824 33388 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34644 33388 603 41 0 34603 0
vsize: 138576
[startup+940.003 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 33969 0 0 0 93907 106 0 0 25 0 1 0 546698731 142753792 33587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34852 33587 603 41 0 34811 0
vsize: 139408
[startup+950.003 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 34149 0 0 0 94906 106 0 0 25 0 1 0 546698731 143429632 33767 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35017 33767 603 41 0 34976 0
vsize: 140068
[startup+960.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 34420 0 0 0 95905 108 0 0 25 0 1 0 546698731 144502784 34038 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35279 34038 603 41 0 35238 0
vsize: 141116
[startup+970.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 34728 0 0 0 96905 108 0 0 25 0 1 0 546698731 145715200 34346 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35575 34346 603 41 0 35534 0
vsize: 142300
[startup+980.004 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 35094 0 0 0 97904 109 0 0 25 0 1 0 546698731 147329024 34712 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35969 34712 603 41 0 35928 0
vsize: 143876
[startup+990.003 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 35287 0 0 0 98904 110 0 0 25 0 1 0 546698731 148148224 34905 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36169 34905 603 41 0 36128 0
vsize: 144676
[startup+1000 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 35412 0 0 0 99904 110 0 0 25 0 1 0 546698731 148549632 35030 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36267 35030 603 41 0 36226 0
vsize: 145068
[startup+1010 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 35636 0 0 0 100903 111 0 0 25 0 1 0 546698731 149483520 35254 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36495 35254 603 41 0 36454 0
vsize: 145980
[startup+1020 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 35894 0 0 0 101902 112 0 0 25 0 1 0 546698731 150568960 35512 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36760 35512 603 41 0 36719 0
vsize: 147040
[startup+1030 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 36179 0 0 0 102901 113 0 0 25 0 1 0 546698731 151662592 35797 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37027 35797 603 41 0 36986 0
vsize: 148108
[startup+1040 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1228
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 36479 0 0 0 103900 114 0 0 25 0 1 0 546698731 152907776 36097 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37331 36097 603 41 0 37290 0
vsize: 149324
[startup+1050 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 36788 0 0 0 104900 115 0 0 25 0 1 0 546698731 154271744 36406 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37664 36406 603 41 0 37623 0
vsize: 150656
[startup+1060 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 37029 0 0 0 105899 116 0 0 25 0 1 0 546698731 155279360 36647 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37910 36647 603 41 0 37869 0
vsize: 151640
[startup+1070 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 37242 0 0 0 106898 117 0 0 25 0 1 0 546698731 156119040 36860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38115 36860 603 41 0 38074 0
vsize: 152460
[startup+1080 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 37469 0 0 0 107897 117 0 0 25 0 1 0 546698731 157114368 37087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38358 37087 603 41 0 38317 0
vsize: 153432
[startup+1090 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 37660 0 0 0 108897 118 0 0 25 0 1 0 546698731 158007296 37278 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38576 37278 603 41 0 38535 0
vsize: 154304
[startup+1100 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 37878 0 0 0 109897 118 0 0 25 0 1 0 546698731 158904320 37496 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38795 37496 603 41 0 38754 0
vsize: 155180
[startup+1110 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 38015 0 0 0 110896 119 0 0 25 0 1 0 546698731 159457280 37633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38930 37633 603 41 0 38889 0
vsize: 155720
[startup+1120 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 38168 0 0 0 111896 120 0 0 25 0 1 0 546698731 160129024 37786 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39094 37786 603 41 0 39053 0
vsize: 156376
[startup+1130 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 38315 0 0 0 112895 120 0 0 25 0 1 0 546698731 160665600 37933 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39225 37933 603 41 0 39184 0
vsize: 156900
[startup+1140 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 38477 0 0 0 113895 121 0 0 25 0 1 0 546698731 161353728 38095 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39393 38095 603 41 0 39352 0
vsize: 157572
[startup+1150 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 38682 0 0 0 114895 121 0 0 25 0 1 0 546698731 162287616 38300 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39621 38300 603 41 0 39580 0
vsize: 158484
[startup+1160 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 38876 0 0 0 115894 122 0 0 25 0 1 0 546698731 163016704 38494 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39799 38494 603 41 0 39758 0
vsize: 159196
[startup+1170 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 39044 0 0 0 116893 123 0 0 25 0 1 0 546698731 163819520 38662 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39995 38662 603 41 0 39954 0
vsize: 159980
[startup+1180 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 39211 0 0 0 117893 124 0 0 25 0 1 0 546698731 164491264 38829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40159 38829 603 41 0 40118 0
vsize: 160636
[startup+1190 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 39361 0 0 0 118892 124 0 0 25 0 1 0 546698731 165036032 38979 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40292 38979 603 41 0 40251 0
vsize: 161168
[startup+1200 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 1230
Raw data (stat): 1165 (minisat+) R 1164 20838 20837 0 -1 0 39540 0 0 0 119892 125 0 0 25 0 1 0 546698731 165842944 39158 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40489 39158 603 41 0 40448 0
vsize: 161956
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.96 1/55 1230
Raw data (stat): 1165 (minisat+) Z 1164 20838 20837 0 -1 12 39542 0 0 0 119892 132 0 0 25 0 1 0 546698731 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.25
CPU user time (s): 1198.93
CPU system time (s): 1.3258
CPU usage (%): 100.015
Max. virtual memory (Kb): 161956
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####