PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-aflow30a.opb
MD5SUM	7fcbcb2a8848112bb780308c9eb60989
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4241
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	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	3334110
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.05
Number of variables	7195
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	555
Trace number 21908

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        442364 kB
Buffers:         13500 kB
Cached:         554828 kB
SwapCached:        560 kB
Active:          31256 kB
Inactive:       539136 kB
HighTotal:      131008 kB
HighFree:         7448 kB
LowTotal:       903652 kB
LowFree:        434916 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5172 kB
Slab:            16176 kB
Committed_AS:    63784 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:43:23 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 12412 7 1200.34 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: 32   maxlim: 35838   bits: 17/16
c ---[1019]---> Adder-cost: 49   maxlim: 6142   bits: 14/13
c ---[1018]---> Adder-cost: 28   maxlim: 13310   bits: 15/14
c ---[1017]---> Adder-cost: 30   maxlim: 18430   bits: 16/15
c ---[1016]---> Adder-cost: 32   maxlim: 51198   bits: 17/16
c ---[1015]---> Adder-cost: 30   maxlim: 30718   bits: 16/15
c ---[1014]---> Adder-cost: 59   maxlim: 32766   bits: 16/15
c ---[1013]---> Adder-cost: 55   maxlim: 16382   bits: 15/14
c ---[1012]---> Adder-cost: 55   maxlim: 29694   bits: 16/15
c ---[1011]---> Adder-cost: 28   maxlim: 16382   bits: 15/14
c ---[1010]---> Adder-cost: 57   maxlim: 31742   bits: 16/15
c ---[1009]---> Adder-cost: 32   maxlim: 39934   bits: 17/16
c ---[1008]---> Adder-cost: 51   maxlim: 11262   bits: 15/14
c ---[1007]---> Adder-cost: 28   maxlim: 15358   bits: 15/14
c ---[1006]---> Adder-cost: 55   maxlim: 16382   bits: 15/14
c ---[1005]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[1004]---> Adder-cost: 32   maxlim: 58366   bits: 17/16
c ---[1002]---> Adder-cost: 32   maxlim: 51198   bits: 17/16
c ---[1001]---> Adder-cost: 32   maxlim: 33790   bits: 17/16
c ---[1000]---> Adder-cost: 30   maxlim: 22526   bits: 16/15
c ---[ 999]---> Adder-cost: 32   maxlim: 43006   bits: 17/16
c ---[ 998]---> Adder-cost: 32   maxlim: 43006   bits: 17/16
c ---[ 996]---> Adder-cost: 59   maxlim: 32766   bits: 16/15
c ---[ 995]---> Adder-cost: 51   maxlim: 10238   bits: 15/14
c ---[ 993]---> Adder-cost: 30   maxlim: 28670   bits: 16/15
c ---[ 992]---> Adder-cost: 32   maxlim: 55294   bits: 17/16
c ---[ 991]---> Adder-cost: 30   maxlim: 26622   bits: 16/15
c ---[ 990]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[ 989]---> Adder-cost: 30   maxlim: 23550   bits: 16/15
c ---[ 988]---> Adder-cost: 30   maxlim: 27646   bits: 16/15
c ---[ 987]---> Adder-cost: 32   maxlim: 64510   bits: 17/16
c ---[ 986]---> Adder-cost: 32   maxlim: 49150   bits: 17/16
c ---[ 985]---> Adder-cost: 55   maxlim: 16382   bits: 15/14
c ---[ 984]---> Adder-cost: 32   maxlim: 35838   bits: 17/16
c ---[ 981]---> Adder-cost: 32   maxlim: 40958   bits: 17/16
c ---[ 980]---> Adder-cost: 49   maxlim: 6142   bits: 14/13
c ---[ 978]---> Adder-cost: 32   maxlim: 57342   bits: 17/16
c ---[ 977]---> Adder-cost: 30   maxlim: 29694   bits: 16/15
c ---[ 974]---> Adder-cost: 45   maxlim: 3070   bits: 13/12
c ---[ 973]---> Adder-cost: 30   maxlim: 31742   bits: 16/15
c ---[ 972]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 971]---> Adder-cost: 32   maxlim: 49150   bits: 17/16
c ---[ 970]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 969]---> Adder-cost: 32   maxlim: 61438   bits: 17/16
c ---[ 968]---> Adder-cost: 55   maxlim: 29694   bits: 16/15
c ---[ 967]---> Adder-cost: 32   maxlim: 36862   bits: 17/16
c ---[ 966]---> Adder-cost: 30   maxlim: 19454   bits: 16/15
c ---[ 964]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 963]---> Adder-cost: 32   maxlim: 56318   bits: 17/16
c ---[ 962]---> Adder-cost: 53   maxlim: 15358   bits: 15/14
c ---[ 961]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 960]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[ 959]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 958]---> Adder-cost: 32   maxlim: 39934   bits: 17/16
c ---[ 956]---> Adder-cost: 53   maxlim: 12286   bits: 15/14
c ---[ 955]---> Adder-cost: 32   maxlim: 39934   bits: 17/16
c ---[ 954]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 953]---> Adder-cost: 32   maxlim: 56318   bits: 17/16
c ---[ 952]---> Adder-cost: 57   maxlim: 31742   bits: 16/15
c ---[ 951]---> Adder-cost: 28   maxlim: 11262   bits: 15/14
c ---[ 950]---> Adder-cost: 32   maxlim: 54270   bits: 17/16
c ---[ 949]---> Adder-cost: 32   maxlim: 41982   bits: 17/16
c ---[ 948]---> Adder-cost: 32   maxlim: 52222   bits: 17/16
c ---[ 947]---> Adder-cost: 32   maxlim: 57342   bits: 17/16
c ---[ 946]---> Adder-cost: 32   maxlim: 53246   bits: 17/16
c ---[ 945]---> Adder-cost: 32   maxlim: 48126   bits: 17/16
c ---[ 944]---> Adder-cost: 30   maxlim: 31742   bits: 16/15
c ---[ 943]---> Adder-cost: 32   maxlim: 44030   bits: 17/16
c ---[ 942]---> Adder-cost: 32   maxlim: 41982   bits: 17/16
c ---[ 941]---> Adder-cost: 28   maxlim: 13310   bits: 15/14
c ---[ 940]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 939]---> Adder-cost: 32   maxlim: 61438   bits: 17/16
c ---[ 937]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 936]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 935]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 934]---> Adder-cost: 32   maxlim: 51198   bits: 17/16
c ---[ 933]---> Adder-cost: 45   maxlim: 3070   bits: 13/12
c ---[ 932]---> Adder-cost: 51   maxlim: 13310   bits: 15/14
c ---[ 931]---> Adder-cost: 30   maxlim: 19454   bits: 16/15
c ---[ 930]---> Adder-cost: 32   maxlim: 47102   bits: 17/16
c ---[ 928]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 927]---> Adder-cost: 32   maxlim: 51198   bits: 17/16
c ---[ 926]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 925]---> Adder-cost: 32   maxlim: 33790   bits: 17/16
c ---[ 924]---> Adder-cost: 32   maxlim: 56318   bits: 17/16
c ---[ 923]---> Adder-cost: 28   maxlim: 10238   bits: 15/14
c ---[ 922]---> Adder-cost: 53   maxlim: 15358   bits: 15/14
c ---[ 921]---> Adder-cost: 51   maxlim: 10238   bits: 15/14
c ---[ 919]---> Adder-cost: 55   maxlim: 16382   bits: 15/14
c ---[ 918]---> Adder-cost: 53   maxlim: 12286   bits: 15/14
c ---[ 917]---> Adder-cost: 32   maxlim: 34814   bits: 17/16
c ---[ 916]---> Adder-cost: 45   maxlim: 3070   bits: 13/12
c ---[ 915]---> Adder-cost: 30   maxlim: 17406   bits: 16/15
c ---[ 914]---> Adder-cost: 32   maxlim: 58366   bits: 17/16
c ---[ 913]---> Adder-cost: 32   maxlim: 62462   bits: 17/16
c ---[ 912]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 911]---> Adder-cost: 32   maxlim: 38910   bits: 17/16
c ---[ 910]---> Adder-cost: 55   maxlim: 16382   bits: 15/14
c ---[ 908]---> Adder-cost: 32   maxlim: 64510   bits: 17/16
c ---[ 907]---> Adder-cost: 32   maxlim: 34814   bits: 17/16
c ---[ 906]---> Adder-cost: 30   maxlim: 25598   bits: 16/15
c ---[ 905]---> Adder-cost: 32   maxlim: 50174   bits: 17/16
c ---[ 903]---> Adder-cost: 32   maxlim: 45054   bits: 17/16
c ---[ 902]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 900]---> Adder-cost: 32   maxlim: 61438   bits: 17/16
c ---[ 899]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 898]---> Adder-cost: 30   maxlim: 24574   bits: 16/15
c ---[ 897]---> Adder-cost: 53   maxlim: 12286   bits: 15/14
c ---[ 896]---> Adder-cost: 30   maxlim: 21502   bits: 16/15
c ---[ 895]---> Adder-cost: 32   maxlim: 62462   bits: 17/16
c ---[ 893]---> Adder-cost: 49   maxlim: 9214   bits: 15/14
c ---[ 892]---> Adder-cost: 32   maxlim: 53246   bits: 17/16
c ---[ 891]---> Adder-cost: 47   maxlim: 5118   bits: 14/13
c ---[ 890]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[ 889]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 888]---> Adder-cost: 32   maxlim: 64510   bits: 17/16
c ---[ 887]---> Adder-cost: 32   maxlim: 51198   bits: 17/16
c ---[ 886]---> Adder-cost: 28   maxlim: 14334   bits: 15/14
c ---[ 885]---> Adder-cost: 32   maxlim: 35838   bits: 17/16
c ---[ 883]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 882]---> Adder-cost: 47   maxlim: 5118   bits: 14/13
c ---[ 881]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[ 880]---> Adder-cost: 32   maxlim: 58366   bits: 17/16
c ---[ 879]---> Adder-cost: 32   maxlim: 49150   bits: 17/16
c ---[ 878]---> Adder-cost: 30   maxlim: 27646   bits: 16/15
c ---[ 877]---> Adder-cost: 28   maxlim: 10238   bits: 15/14
c ---[ 876]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 875]---> Adder-cost: 32   maxlim: 52222   bits: 17/16
c ---[ 874]---> Adder-cost: 32   maxlim: 54270   bits: 17/16
c ---[ 873]---> Adder-cost: 28   maxlim: 15358   bits: 15/14
c ---[ 871]---> Adder-cost: 30   maxlim: 25598   bits: 16/15
c ---[ 870]---> Adder-cost: 32   maxlim: 55294   bits: 17/16
c ---[ 869]---> Adder-cost: 30   maxlim: 27646   bits: 16/15
c ---[ 867]---> Adder-cost: 49   maxlim: 6142   bits: 14/13
c ---[ 866]---> Adder-cost: 57   maxlim: 31742   bits: 16/15
c ---[ 865]---> Adder-cost: 32   maxlim: 36862   bits: 17/16
c ---[ 863]---> Adder-cost: 32   maxlim: 38910   bits: 17/16
c ---[ 862]---> Adder-cost: 32   maxlim: 43006   bits: 17/16
c ---[ 861]---> Adder-cost: 51   maxlim: 11262   bits: 15/14
c ---[ 860]---> Adder-cost: 32   maxlim: 55294   bits: 17/16
c ---[ 859]---> Adder-cost: 30   maxlim: 17406   bits: 16/15
c ---[ 858]---> Adder-cost: 32   maxlim: 53246   bits: 17/16
c ---[ 857]---> Adder-cost: 51   maxlim: 13310   bits: 15/14
c ---[ 856]---> Adder-cost: 57   maxlim: 31742   bits: 16/15
c ---[ 855]---> Adder-cost: 30   maxlim: 29694   bits: 16/15
c ---[ 853]---> Adder-cost: 32   maxlim: 40958   bits: 17/16
c ---[ 851]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 850]---> Adder-cost: 30   maxlim: 27646   bits: 16/15
c ---[ 849]---> Adder-cost: 28   maxlim: 16382   bits: 15/14
c ---[ 848]---> Adder-cost: 30   maxlim: 18430   bits: 16/15
c ---[ 847]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 846]---> Adder-cost: 30   maxlim: 28670   bits: 16/15
c ---[ 845]---> Adder-cost: 32   maxlim: 40958   bits: 17/16
c ---[ 844]---> Adder-cost: 30   maxlim: 21502   bits: 16/15
c ---[ 843]---> Adder-cost: 30   maxlim: 27646   bits: 16/15
c ---[ 842]---> Adder-cost: 28   maxlim: 11262   bits: 15/14
c ---[ 841]---> Adder-cost: 28   maxlim: 14334   bits: 15/14
c ---[ 840]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 839]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 837]---> Adder-cost: 45   maxlim: 3070   bits: 13/12
c ---[ 836]---> Adder-cost: 30   maxlim: 31742   bits: 16/15
c ---[ 835]---> Adder-cost: 32   maxlim: 58366   bits: 17/16
c ---[ 834]---> Adder-cost: 32   maxlim: 57342   bits: 17/16
c ---[ 833]---> Adder-cost: 32   maxlim: 50174   bits: 17/16
c ---[ 832]---> Adder-cost: 32   maxlim: 36862   bits: 17/16
c ---[ 831]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[ 829]---> Adder-cost: 32   maxlim: 60414   bits: 17/16
c ---[ 828]---> Adder-cost: 30   maxlim: 20478   bits: 16/15
c ---[ 825]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 824]---> Adder-cost: 32   maxlim: 45054   bits: 17/16
c ---[ 823]---> Adder-cost: 55   maxlim: 29694   bits: 16/15
c ---[ 822]---> Adder-cost: 30   maxlim: 29694   bits: 16/15
c ---[ 821]---> Adder-cost: 32   maxlim: 35838   bits: 17/16
c ---[ 820]---> Adder-cost: 32   maxlim: 34814   bits: 17/16
c ---[ 819]---> Adder-cost: 32   maxlim: 34814   bits: 17/16
c ---[ 818]---> Adder-cost: 32   maxlim: 37886   bits: 17/16
c ---[ 817]---> Adder-cost: 32   maxlim: 47102   bits: 17/16
c ---[ 816]---> Adder-cost: 32   maxlim: 58366   bits: 17/16
c ---[ 815]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 814]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 812]---> Adder-cost: 32   maxlim: 63486   bits: 17/16
c ---[ 811]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 809]---> Adder-cost: 30   maxlim: 29694   bits: 16/15
c ---[ 808]---> Adder-cost: 30   maxlim: 20478   bits: 16/15
c ---[ 807]---> Adder-cost: 32   maxlim: 64510   bits: 17/16
c ---[ 806]---> Adder-cost: 32   maxlim: 39934   bits: 17/16
c ---[ 805]---> Adder-cost: 30   maxlim: 17406   bits: 16/15
c ---[ 804]---> Adder-cost: 30   maxlim: 28670   bits: 16/15
c ---[ 803]---> Adder-cost: 32   maxlim: 44030   bits: 17/16
c ---[ 801]---> Adder-cost: 32   maxlim: 59390   bits: 17/16
c ---[ 800]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[ 799]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 798]---> Adder-cost: 51   maxlim: 10238   bits: 15/14
c ---[ 797]---> Adder-cost: 32   maxlim: 61438   bits: 17/16
c ---[ 796]---> Adder-cost: 28   maxlim: 16382   bits: 15/14
c ---[ 795]---> Adder-cost: 32   maxlim: 41982   bits: 17/16
c ---[ 793]---> Adder-cost: 30   maxlim: 20478   bits: 16/15
c ---[ 791]---> Adder-cost: 32   maxlim: 34814   bits: 17/16
c ---[ 790]---> Adder-cost: 30   maxlim: 23550   bits: 16/15
c ---[ 789]---> Adder-cost: 47   maxlim: 5118   bits: 14/13
c ---[ 788]---> Adder-cost: 55   maxlim: 29694   bits: 16/15
c ---[ 787]---> Adder-cost: 32   maxlim: 59390   bits: 17/16
c ---[ 786]---> Adder-cost: 32   maxlim: 47102   bits: 17/16
c ---[ 785]---> Adder-cost: 32   maxlim: 48126   bits: 17/16
c ---[ 784]---> Adder-cost: 51   maxlim: 8190   bits: 14/13
c ---[ 782]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[ 781]---> Adder-cost: 32   maxlim: 49150   bits: 17/16
c ---[ 780]---> Adder-cost: 28   maxlim: 15358   bits: 15/14
c ---[ 779]---> Adder-cost: 32   maxlim: 50174   bits: 17/16
c ---[ 778]---> Adder-cost: 32   maxlim: 51198   bits: 17/16
c ---[ 777]---> Adder-cost: 28   maxlim: 15358   bits: 15/14
c ---[ 776]---> Adder-cost: 28   maxlim: 13310   bits: 15/14
c ---[ 774]---> Adder-cost: 32   maxlim: 54270   bits: 17/16
c ---[ 772]---> Adder-cost: 30   maxlim: 17406   bits: 16/15
c ---[ 771]---> Adder-cost: 32   maxlim: 46078   bits: 17/16
c ---[ 770]---> Adder-cost: 32   maxlim: 58366   bits: 17/16
c ---[ 769]---> Adder-cost: 32   maxlim: 35838   bits: 17/16
c ---[ 768]---> Adder-cost: 32   maxlim: 61438   bits: 17/16
c ---[ 767]---> Adder-cost: 49   maxlim: 6142   bits: 14/13
c ---[ 766]---> Adder-cost: 32   maxlim: 45054   bits: 17/16
c ---[ 764]---> Adder-cost: 32   maxlim: 47102   bits: 17/16
c ---[ 763]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 762]---> Adder-cost: 32   maxlim: 62462   bits: 17/16
c ---[ 761]---> Adder-cost: 32   maxlim: 41982   bits: 17/16
c ---[ 760]---> Adder-cost: 32   maxlim: 35838   bits: 17/16
c ---[ 759]---> Adder-cost: 53   maxlim: 12286   bits: 15/14
c ---[ 758]---> Adder-cost: 51   maxlim: 10238   bits: 15/14
c ---[ 757]---> Adder-cost: 28   maxlim: 13310   bits: 15/14
c ---[ 756]---> Adder-cost: 53   maxlim: 15358   bits: 15/14
c ---[ 754]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 753]---> Adder-cost: 32   maxlim: 48126   bits: 17/16
c ---[ 752]---> Adder-cost: 32   maxlim: 58366   bits: 17/16
c ---[ 751]---> Adder-cost: 45   maxlim: 3070   bits: 13/12
c ---[ 750]---> Adder-cost: 30   maxlim: 25598   bits: 16/15
c ---[ 749]---> Adder-cost: 32   maxlim: 64510   bits: 17/16
c ---[ 747]---> Adder-cost: 30   maxlim: 29694   bits: 16/15
c ---[ 746]---> Adder-cost: 30   maxlim: 20478   bits: 16/15
c ---[ 745]---> Adder-cost: 30   maxlim: 21502   bits: 16/15
c ---[ 744]---> Adder-cost: 28   maxlim: 11262   bits: 15/14
c ---[ 743]---> Adder-cost: 30   maxlim: 17406   bits: 16/15
c ---[ 742]---> Adder-cost: 32   maxlim: 54270   bits: 17/16
c ---[ 741]---> Adder-cost: 28   maxlim: 10238   bits: 15/14
c ---[ 740]---> Adder-cost: 30   maxlim: 26622   bits: 16/15
c ---[ 738]---> Adder-cost: 30   maxlim: 24574   bits: 16/15
c ---[ 737]---> Adder-cost: 30   maxlim: 19454   bits: 16/15
c ---[ 736]---> Adder-cost: 30   maxlim: 17406   bits: 16/15
c ---[ 734]---> Adder-cost: 47   maxlim: 5118   bits: 14/13
c ---[ 733]---> Adder-cost: 30   maxlim: 17406   bits: 16/15
c ---[ 732]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 730]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 729]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 728]---> Adder-cost: 30   maxlim: 28670   bits: 16/15
c ---[ 727]---> Adder-cost: 49   maxlim: 9214   bits: 15/14
c ---[ 726]---> Adder-cost: 30   maxlim: 18430   bits: 16/15
c ---[ 725]---> Adder-cost: 47   maxlim: 5118   bits: 14/13
c ---[ 723]---> Adder-cost: 32   maxlim: 37886   bits: 17/16
c ---[ 722]---> Adder-cost: 30   maxlim: 25598   bits: 16/15
c ---[ 721]---> Adder-cost: 32   maxlim: 63486   bits: 17/16
c ---[ 720]---> Adder-cost: 32   maxlim: 53246   bits: 17/16
c ---[ 719]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 718]---> Adder-cost: 32   maxlim: 47102   bits: 17/16
c ---[ 717]---> Adder-cost: 30   maxlim: 24574   bits: 16/15
c ---[ 716]---> Adder-cost: 28   maxlim: 15358   bits: 15/14
c ---[ 713]---> Adder-cost: 30   maxlim: 19454   bits: 16/15
c ---[ 712]---> Adder-cost: 51   maxlim: 8190   bits: 14/13
c ---[ 711]---> Adder-cost: 53   maxlim: 12286   bits: 15/14
c ---[ 710]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 708]---> Adder-cost: 32   maxlim: 65534   bits: 17/16
c ---[ 706]---> Adder-cost: 32   maxlim: 55294   bits: 17/16
c ---[ 705]---> Adder-cost: 32   maxlim: 50174   bits: 17/16
c ---[ 704]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 703]---> Adder-cost: 32   maxlim: 49150   bits: 17/16
c ---[ 702]---> Adder-cost: 32   maxlim: 54270   bits: 17/16
c ---[ 701]---> Adder-cost: 32   maxlim: 45054   bits: 17/16
c ---[ 700]---> Adder-cost: 32   maxlim: 40958   bits: 17/16
c ---[ 699]---> Adder-cost: 53   maxlim: 12286   bits: 15/14
c ---[ 698]---> Adder-cost: 32   maxlim: 60414   bits: 17/16
c ---[ 695]---> Adder-cost: 28   maxlim: 14334   bits: 15/14
c ---[ 694]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 693]---> Adder-cost: 32   maxlim: 64510   bits: 17/16
c ---[ 692]---> Adder-cost: 32   maxlim: 49150   bits: 17/16
c ---[ 691]---> Adder-cost: 32   maxlim: 54270   bits: 17/16
c ---[ 690]---> Adder-cost: 30   maxlim: 19454   bits: 16/15
c ---[ 688]---> Adder-cost: 53   maxlim: 15358   bits: 15/14
c ---[ 687]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 686]---> Adder-cost: 32   maxlim: 58366   bits: 17/16
c ---[ 684]---> Adder-cost: 32   maxlim: 54270   bits: 17/16
c ---[ 683]---> Adder-cost: 28   maxlim: 13310   bits: 15/14
c ---[ 682]---> Adder-cost: 28   maxlim: 11262   bits: 15/14
c ---[ 681]---> Adder-cost: 32   maxlim: 49150   bits: 17/16
c ---[ 680]---> Adder-cost: 32   maxlim: 62462   bits: 17/16
c ---[ 679]---> Adder-cost: 30   maxlim: 27646   bits: 16/15
c ---[ 678]---> Adder-cost: 30   maxlim: 30718   bits: 16/15
c ---[ 677]---> Adder-cost: 30   maxlim: 20478   bits: 16/15
c ---[ 676]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 675]---> Adder-cost: 30   maxlim: 21502   bits: 16/15
c ---[ 673]---> Adder-cost: 28   maxlim: 13310   bits: 15/14
c ---[ 672]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 671]---> Adder-cost: 32   maxlim: 39934   bits: 17/16
c ---[ 670]---> Adder-cost: 32   maxlim: 63486   bits: 17/16
c ---[ 668]---> Adder-cost: 32   maxlim: 45054   bits: 17/16
c ---[ 667]---> Adder-cost: 32   maxlim: 63486   bits: 17/16
c ---[ 666]---> Adder-cost: 49   maxlim: 6142   bits: 14/13
c ---[ 665]---> Adder-cost: 30   maxlim: 32766   bits: 16/15
c ---[ 664]---> Adder-cost: 30   maxlim: 28670   bits: 16/15
c ---[ 663]---> Adder-cost: 32   maxlim: 47102   bits: 17/16
c ---[ 662]---> Adder-cost: 59   maxlim: 32766   bits: 16/15
c ---[ 661]---> Adder-cost: 30   maxlim: 22526   bits: 16/15
c ---[ 660]---> Adder-cost: 49   maxlim: 6142   bits: 14/13
c ---[ 659]---> Adder-cost: 32   maxlim: 53246   bits: 17/16
c ---[ 658]---> Adder-cost: 32   maxlim: 57342   bits: 17/16
c ---[ 657]---> Adder-cost: 53   maxlim: 12286   bits: 15/14
c ---[ 656]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 655]---> Adder-cost: 55   maxlim: 16382   bits: 15/14
c ---[ 654]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 653]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 651]---> Adder-cost: 49   maxlim: 9214   bits: 15/14
c ---[ 649]---> Adder-cost: 30   maxlim: 25598   bits: 16/15
c ---[ 648]---> Adder-cost: 30   maxlim: 32766   bits: 16/15
c ---[ 647]---> Adder-cost: 32   maxlim: 57342   bits: 17/16
c ---[ 645]---> Adder-cost: 32   maxlim: 51198   bits: 17/16
c ---[ 644]---> Adder-cost: 45   maxlim: 3070   bits: 13/12
c ---[ 643]---> Adder-cost: 32   maxlim: 46078   bits: 17/16
c ---[ 642]---> Adder-cost: 32   maxlim: 38910   bits: 17/16
c ---[ 640]---> Adder-cost: 30   maxlim: 28670   bits: 16/15
c ---[ 638]---> Adder-cost: 32   maxlim: 57342   bits: 17/16
c ---[ 637]---> Adder-cost: 30   maxlim: 28670   bits: 16/15
c ---[ 636]---> Adder-cost: 32   maxlim: 55294   bits: 17/16
c ---[ 635]---> Adder-cost: 30   maxlim: 18430   bits: 16/15
c ---[ 634]---> Adder-cost: 47   maxlim: 5118   bits: 14/13
c ---[ 633]---> Adder-cost: 30   maxlim: 23550   bits: 16/15
c ---[ 632]---> Adder-cost: 32   maxlim: 45054   bits: 17/16
c ---[ 631]---> Adder-cost: 51   maxlim: 11262   bits: 15/14
c ---[ 630]---> Adder-cost: 32   maxlim: 64510   bits: 17/16
c ---[ 628]---> Adder-cost: 30   maxlim: 21502   bits: 16/15
c ---[ 627]---> Adder-cost: 32   maxlim: 45054   bits: 17/16
c ---[ 625]---> Adder-cost: 32   maxlim: 58366   bits: 17/16
c ---[ 624]---> Adder-cost: 59   maxlim: 32766   bits: 16/15
c ---[ 623]---> Adder-cost: 30   maxlim: 29694   bits: 16/15
c ---[ 622]---> Adder-cost: 30   maxlim: 25598   bits: 16/15
c ---[ 621]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
c ---[ 620]---> Adder-cost: 30   maxlim: 24574   bits: 16/15
c ---[ 619]---> Adder-cost: 32   maxlim: 59390   bits: 17/16
c ---[ 618]---> Adder-cost: 28   maxlim: 10238   bits: 15/14
c ---[ 617]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 616]---> Adder-cost: 32   maxlim: 63486   bits: 17/16
c ---[ 615]---> Adder-cost: 32   maxlim: 63486   bits: 17/16
c ---[ 614]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[ 613]---> Adder-cost: 53   maxlim: 15358   bits: 15/14
c ---[ 608]---> Adder-cost: 30   maxlim: 26622   bits: 16/15
c ---[ 607]---> Adder-cost: 32   maxlim: 33790   bits: 17/16
c ---[ 606]---> Adder-cost: 51   maxlim: 8190   bits: 14/13
c ---[ 605]---> Adder-cost: 57   maxlim: 30718   bits: 16/15
c ---[ 604]---> Adder-cost: 28   maxlim: 16382   bits: 15/14
c ---[ 603]---> Adder-cost: 57   maxlim: 31742   bits: 16/15
c ---[ 602]---> Adder-cost: 32   maxlim: 55294   bits: 17/16
c ---[ 601]---> Adder-cost: 32   maxlim: 60414   bits: 17/16
c ---[ 600]---> Adder-cost: 47   maxlim: 4094   bits: 13/12
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: 131070   bits: 18/17
c ---[ 594]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 593]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 592]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 591]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 590]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 589]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 588]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 587]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 586]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 584]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 583]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 582]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 581]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 580]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 579]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 578]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 577]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 576]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 575]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 574]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 572]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 571]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 570]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 569]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 568]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 567]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 566]---> Adder-cost: 4   maxlim: 65534   bits: 17/16
c ---[ 565]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 564]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 563]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 562]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 560]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 559]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 558]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 557]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 556]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 555]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 554]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 553]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 552]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 551]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 550]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 548]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 547]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 546]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 545]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 544]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 543]---> Adder-cost: 2   maxlim: 131070   bits: 18/17
c ---[ 542]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 541]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 540]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 539]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 538]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 536]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 535]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 534]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 533]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 532]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 531]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 530]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 529]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 528]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 527]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 526]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 524]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 523]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 522]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 521]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 520]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 519]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 518]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 517]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 516]---> Adder-cost: 2   maxlim: 32766   bits: 16/15
c ---[ 515]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 514]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 512]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 511]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 510]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 509]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 508]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 507]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 506]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 505]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 504]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 503]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 502]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 500]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 499]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 498]---> Adder-cost: 2   maxlim: 131070   bits: 18/17
c ---[ 497]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 496]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 495]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 494]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 493]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 492]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 491]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 490]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 488]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 487]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 486]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 485]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 484]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 483]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 482]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 481]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 480]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 479]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 478]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
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: 131070   bits: 18/17
c ---[ 472]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 471]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 470]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 469]---> Adder-cost: 2   maxlim: 32766   bits: 16/15
c ---[ 468]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 467]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 466]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 465]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 464]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 462]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 461]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 460]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 459]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 458]---> Adder-cost: 4   maxlim: 32766   bits: 16/15
c ---[ 457]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 456]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 455]---> Adder-cost: 6   maxlim: 131070   bits: 18/17
c ---[ 454]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 453]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 452]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 450]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 449]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 448]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 447]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 446]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 445]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 444]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 443]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 442]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 441]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 440]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 438]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 437]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 436]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 435]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 434]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 433]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 432]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 431]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 430]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 429]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 428]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 426]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 425]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 424]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 423]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 422]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 421]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 420]---> Adder-cost: 2   maxlim: 131070   bits: 18/17
c ---[ 419]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 418]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 417]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 416]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 414]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 413]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 412]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 411]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 410]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 409]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 408]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 407]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 406]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 405]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 404]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 402]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 401]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 400]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 399]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 398]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 397]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 396]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 395]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 394]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 393]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 392]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 390]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 389]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 388]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 387]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 386]---> Adder-cost: 4   maxlim: 32766   bits: 16/15
c ---[ 385]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 384]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 383]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 382]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 381]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 380]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 378]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 377]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 376]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 375]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 374]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 373]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 372]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 371]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 370]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 369]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 368]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 366]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 365]---> Adder-cost: 2   maxlim: 131070   bits: 18/17
c ---[ 364]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 363]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 362]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 361]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 360]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 359]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 358]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 357]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 356]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 354]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 352]---> Adder-cost: 849   maxlim: 818166   bits: 21/20
c ---[ 351]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 350]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 349]---> Adder-cost: 6   maxlim: 131070   bits: 18/17
c ---[ 348]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 347]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 346]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 345]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 344]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 343]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 342]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 340]---> Adder-cost: 704   maxlim: 1189875   bits: 21/21
c ---[ 339]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 338]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 337]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 336]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 335]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 334]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 333]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 332]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 331]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 330]---> Adder-cost: 2   maxlim: 65534   bits: 17/16
c ---[ 328]---> Adder-cost: 1078   maxlim: 1449967   bits: 22/21
c ---[ 327]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 326]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 325]---> Adder-cost: 4   maxlim: 131070   bits: 18/17
c ---[ 324]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 323]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 322]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 321]---> Adder-cost: 4   maxlim: 131070   bits: 18/17
c ---[ 320]---> Adder-cost: 4   maxlim: 65534   bits: 17/16
c ---[ 319]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 318]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 316]---> Adder-cost: 1006   maxlim: 1169393   bits: 22/21
c ---[ 315]---> Adder-cost: 6   maxlim: 131070   bits: 18/17
c ---[ 314]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 313]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 312]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 311]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 310]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 309]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 308]---> Adder-cost: 6   maxlim: 131070   bits: 18/17
c ---[ 307]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 306]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 304]---> Adder-cost: 1030   maxlim: 1483760   bits: 22/21
c ---[ 303]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 302]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 301]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 300]---> Adder-cost: 2   maxlim: 65534   bits: 17/16
c ---[ 299]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 298]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 297]---> Adder-cost: 2   maxlim: 131070   bits: 18/17
c ---[ 296]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 295]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 294]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 292]---> Adder-cost: 672   maxlim: 746486   bits: 21/20
c ---[ 291]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 290]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 289]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 288]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 287]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 286]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 285]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 284]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 283]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 282]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 280]---> Adder-cost: 882   maxlim: 1305585   bits: 22/21
c ---[ 279]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 278]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 277]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 276]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 275]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 274]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 273]---> Adder-cost: 2   maxlim: 131070   bits: 18/17
c ---[ 272]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 271]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 270]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 268]---> Adder-cost: 942   maxlim: 1302514   bits: 22/21
c ---[ 267]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 266]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 265]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 264]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 263]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 262]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 261]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 260]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 259]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 258]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 256]---> Adder-cost: 980   maxlim: 1616878   bits: 22/21
c ---[ 255]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 254]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 253]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 252]---> Adder-cost: 6   maxlim: 16382   bits: 15/14
c ---[ 251]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 250]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 249]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 248]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 247]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 246]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 244]---> Adder-cost: 820   maxlim: 1307634   bits: 22/21
c ---[ 243]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 242]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 241]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 240]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 239]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 238]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 237]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 236]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 235]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 234]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 232]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 230]---> Adder-cost: 868   maxlim: 1257457   bits: 22/21
c ---[ 229]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 228]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 227]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 226]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 225]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 224]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 223]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 222]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 221]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 220]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 218]---> Adder-cost: 936   maxlim: 1176560   bits: 22/21
c ---[ 217]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 216]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 215]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 214]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 213]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 212]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 211]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 210]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 209]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 208]---> Adder-cost: 4   maxlim: 65534   bits: 17/16
c ---[ 206]---> Adder-cost: 933   maxlim: 1047537   bits: 21/20
c ---[ 205]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 204]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 203]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 202]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 201]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 200]---> Adder-cost: 4   maxlim: 65534   bits: 17/16
c ---[ 199]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 198]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 197]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 196]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 194]---> Adder-cost: 858   maxlim: 810997   bits: 21/20
c ---[ 193]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 192]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 191]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 190]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 189]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 188]---> Adder-cost: 4   maxlim: 32766   bits: 16/15
c ---[ 187]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 186]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 185]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 184]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 182]---> Adder-cost: 752   maxlim: 1157107   bits: 22/21
c ---[ 181]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 180]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 179]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 178]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 177]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 176]---> Adder-cost: 6   maxlim: 131070   bits: 18/17
c ---[ 175]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 174]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 173]---> Adder-cost: 4   maxlim: 131070   bits: 18/17
c ---[ 172]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 170]---> Adder-cost: 938   maxlim: 1399793   bits: 22/21
c ---[ 169]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 168]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 167]---> Adder-cost: 2   maxlim: 32766   bits: 16/15
c ---[ 166]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 165]---> Adder-cost: 2   maxlim: 32766   bits: 16/15
c ---[ 164]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 163]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 162]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 161]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 160]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 158]---> Adder-cost: 674   maxlim: 1276915   bits: 21/21
c ---[ 157]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 156]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 155]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 154]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 153]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 152]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 151]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 150]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 149]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 148]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 146]---> Adder-cost: 1010   maxlim: 1387503   bits: 22/21
c ---[ 145]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 144]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 143]---> Adder-cost: 6   maxlim: 131070   bits: 18/17
c ---[ 142]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 141]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 140]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 139]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 138]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 137]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 136]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 134]---> Adder-cost: 1056   maxlim: 1096690   bits: 22/21
c ---[ 132]---> Adder-cost: 966   maxlim: 1423342   bits: 22/21
c ---[ 130]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 128]---> Adder-cost: 740   maxlim: 960501   bits: 21/20
c ---[ 126]---> Adder-cost: 796   maxlim: 1239025   bits: 21/21
c ---[ 124]---> Adder-cost: 1062   maxlim: 1713133   bits: 22/21
c ---[ 122]---> Adder-cost: 872   maxlim: 1144817   bits: 22/21
c ---[ 120]---> Adder-cost: 758   maxlim: 669685   bits: 21/20
c ---[ 118]---> Adder-cost: 868   maxlim: 1154031   bits: 22/21
c ---[ 116]---> Adder-cost: 1012   maxlim: 1354738   bits: 22/21
c ---[ 114]---> Adder-cost: 742   maxlim: 1047540   bits: 21/20
c ---[ 112]---> Adder-cost: 1002   maxlim: 1405934   bits: 22/21
c ---[ 111]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 109]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 108]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 107]---> Adder-cost: 4   maxlim: 65534   bits: 17/16
c ---[ 106]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 105]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 104]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[ 103]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 102]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 101]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 100]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[  99]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[  97]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[  96]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[  95]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[  94]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[  93]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[  92]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[  91]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[  90]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[  89]---> Adder-cost: 4   maxlim: 65534   bits: 17/16
c ---[  88]---> Adder-cost: 2   maxlim: 131070   bits: 18/17
c ---[  87]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[  85]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  84]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  83]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[  82]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[  81]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  80]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[  79]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[  78]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[  77]---> Adder-cost: 4   maxlim: 131070   bits: 18/17
c ---[  76]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  75]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[  73]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[  72]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  71]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  70]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[  69]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[  68]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[  67]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[  66]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[  65]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[  64]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[  63]---> Adder-cost: 6   maxlim: 131070   bits: 18/17
c ---[  62]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[  61]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[  60]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  59]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  58]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  57]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  56]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[  55]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[  54]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[  53]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[  52]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  51]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[  50]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[  49]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  48]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  47]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[  46]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[  45]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  44]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  42]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  41]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[  40]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[  39]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  38]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[  37]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  36]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[  35]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[  34]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  33]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[  32]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  31]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[  30]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  29]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  28]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[  27]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  26]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  25]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  24]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[  23]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  22]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[  21]---> Adder-cost: 26   maxlim: 7166   bits: 14/13
c ---[  20]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  19]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[  18]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[  17]---> Adder-cost: 26   maxlim: 5118   bits: 14/13
c ---[  16]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  15]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  13]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  12]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  11]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[  10]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[   9]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[   8]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[   7]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[   6]---> Adder-cost: 26   maxlim: 8190   bits: 14/13
c ---[   5]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[   4]---> Adder-cost: 26   maxlim: 6142   bits: 14/13
c ---[   3]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[   2]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[   1]---> Adder-cost: 24   maxlim: 3070   bits: 13/12
c ---[   0]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  303093  1153507 |  101031       0        0     nan |  0.000 % |
c |       101 |  303093  1153507 |  111134     101      682     6.8 | 20.900 % |
c |       259 |  303093  1153507 |  122247     259     1741     6.7 | 20.900 % |
c |       486 |  303093  1153507 |  134472     486     3294     6.8 | 20.900 % |
c |       823 |  303085  1153477 |  147919     822     4780     5.8 | 20.901 % |
c |      1329 |  303037  1153311 |  162711    1324     6509     4.9 | 20.914 % |
c |      2088 |  302981  1153131 |  178982    2077     9055     4.4 | 20.929 % |
c |      3227 |  302941  1152997 |  196880    3211    13492     4.2 | 20.936 % |
c |      4935 |  302799  1152531 |  216568    4903    20878     4.3 | 20.970 % |
c |      7497 |  302677  1152121 |  238225    7449    35618     4.8 | 20.998 % |
c |     11341 |  302591  1151845 |  262048   11282    92465     8.2 | 21.021 % |
c |     17107 |  302499  1151537 |  288253   17033   192208    11.3 | 21.047 % |
c |     25757 |  302449  1151365 |  317078   25674   412646    16.1 | 21.059 % |
c |     38731 |  302433  1151313 |  348786   38646   845177    21.9 | 21.063 % |
c |     58192 |  302282  1150810 |  383665   58085  1559896    26.9 | 21.106 % |
c |     87384 |  302071  1150105 |  422031   87244  2631073    30.2 | 21.163 % |
c |    131174 |  301726  1148948 |  464234  130948  3888085    29.7 | 21.250 % |
c |    196858 |  301617  1148581 |  510658  196585  6808037    34.6 | 21.277 % |
c |    295384 |  301448  1147992 |  561724  294918 13208817    44.8 | 21.309 % |
c |    443175 |  301217  1147213 |  617896  442536 20273809    45.8 | 21.364 % |
#### 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.81 0.95 0.95 2/55 13362
Raw data (stat): 13362 (runsolver) R 13361 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549725961 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.84 0.95 0.95 2/55 13362
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 7897 0 0 0 978 20 0 0 25 0 1 0 549725961 35954688 7527 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8778 7527 603 41 0 8737 0
vsize: 35112
[startup+20.0016 s]
Raw data (loadavg): 0.86 0.95 0.95 2/55 13362
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 8084 0 0 0 1977 21 0 0 25 0 1 0 549725961 36765696 7714 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8976 7714 603 41 0 8935 0
vsize: 35904
[startup+30.003 s]
Raw data (loadavg): 0.88 0.95 0.95 2/55 13362
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 8363 0 0 0 2977 22 0 0 25 0 1 0 549725961 37871616 7993 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9246 7993 603 41 0 9205 0
vsize: 36984
[startup+40.0038 s]
Raw data (loadavg): 0.90 0.96 0.95 2/55 13362
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 9023 0 0 0 3974 25 0 0 25 0 1 0 549725961 40681472 8653 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9932 8653 603 41 0 9891 0
vsize: 39728
[startup+50.0042 s]
Raw data (loadavg): 0.92 0.96 0.95 2/55 13362
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 9523 0 0 0 4972 26 0 0 25 0 1 0 549725961 42708992 9153 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10427 9153 603 41 0 10386 0
vsize: 41708
[startup+60.0045 s]
Raw data (loadavg): 0.93 0.96 0.95 2/55 13362
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 9996 0 0 0 5971 28 0 0 25 0 1 0 549725961 44625920 9626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10895 9626 603 41 0 10854 0
vsize: 43580
[startup+70.0053 s]
Raw data (loadavg): 0.94 0.96 0.95 2/55 13362
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 10383 0 0 0 6969 30 0 0 25 0 1 0 549725961 46104576 10013 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11256 10013 603 41 0 11215 0
vsize: 45024
[startup+80.0067 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 13362
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 10736 0 0 0 7968 32 0 0 25 0 1 0 549725961 47841280 10366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11680 10366 603 41 0 11639 0
vsize: 46720
[startup+90.0069 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 11105 0 0 0 8966 33 0 0 25 0 1 0 549725961 49336320 10735 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12045 10735 603 41 0 12004 0
vsize: 48180
[startup+100.007 s]
Raw data (loadavg): 0.96 0.96 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 11354 0 0 0 9964 35 0 0 25 0 1 0 549725961 50454528 10984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12318 10984 603 41 0 12277 0
vsize: 49272
[startup+110.007 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 11628 0 0 0 10963 37 0 0 25 0 1 0 549725961 51544064 11258 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12584 11258 603 41 0 12543 0
vsize: 50336
[startup+120.008 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 11879 0 0 0 11962 37 0 0 25 0 1 0 549725961 52486144 11509 4294967295 134512640 134672761 3221224544 3221223632 1075346529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12814 11509 603 41 0 12773 0
vsize: 51256
[startup+130.009 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 12154 0 0 0 12961 39 0 0 25 0 1 0 549725961 53719040 11784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13115 11784 603 41 0 13074 0
vsize: 52460
[startup+140.009 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 12372 0 0 0 13960 40 0 0 25 0 1 0 549725961 54554624 12002 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13319 12002 603 41 0 13278 0
vsize: 53276
[startup+150.01 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 12610 0 0 0 14959 42 0 0 25 0 1 0 549725961 55504896 12240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13551 12240 603 41 0 13510 0
vsize: 54204
[startup+160.011 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 12746 0 0 0 15958 42 0 0 25 0 1 0 549725961 56082432 12376 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13692 12376 603 41 0 13651 0
vsize: 54768
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 12931 0 0 0 16957 43 0 0 25 0 1 0 549725961 56918016 12561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12561 603 41 0 13855 0
vsize: 55584
[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 13414 0 0 0 17956 45 0 0 25 0 1 0 549725961 58793984 13044 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14354 13044 603 41 0 14313 0
vsize: 57416
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 13771 0 0 0 18954 47 0 0 25 0 1 0 549725961 60813312 13401 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14847 13401 603 41 0 14806 0
vsize: 59388
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 14693 0 0 0 19952 49 0 0 25 0 1 0 549725961 64458752 14323 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15737 14323 603 41 0 15696 0
vsize: 62948
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 15493 0 0 0 20950 51 0 0 25 0 1 0 549725961 67698688 15123 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16528 15123 603 41 0 16487 0
vsize: 66112
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 16068 0 0 0 21947 54 0 0 25 0 1 0 549725961 69984256 15698 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17086 15698 603 41 0 17045 0
vsize: 68344
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 16542 0 0 0 22946 55 0 0 25 0 1 0 549725961 71897088 16172 4294967295 134512640 134672761 3221224544 3221223696 134565212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17553 16172 603 41 0 17512 0
vsize: 70212
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 17027 0 0 0 23945 57 0 0 25 0 1 0 549725961 73924608 16657 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18048 16657 603 41 0 18007 0
vsize: 72192
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 17564 0 0 0 24942 59 0 0 25 0 1 0 549725961 76128256 17194 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18586 17194 603 41 0 18545 0
vsize: 74344
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 17959 0 0 0 25941 60 0 0 25 0 1 0 549725961 77733888 17589 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18978 17589 603 41 0 18937 0
vsize: 75912
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 18372 0 0 0 26940 62 0 0 25 0 1 0 549725961 79478784 18002 4294967295 134512640 134672761 3221224544 3221223648 134554877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19404 18002 603 41 0 19363 0
vsize: 77616
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 18854 0 0 0 27938 64 0 0 25 0 1 0 549725961 81391616 18484 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19871 18484 603 41 0 19830 0
vsize: 79484
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 19263 0 0 0 28936 66 0 0 25 0 1 0 549725961 83021824 18893 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20269 18893 603 41 0 20228 0
vsize: 81076
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 19765 0 0 0 29935 67 0 0 25 0 1 0 549725961 85049344 19395 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20764 19395 603 41 0 20723 0
vsize: 83056
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 20252 0 0 0 30933 69 0 0 25 0 1 0 549725961 87056384 19882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21254 19882 603 41 0 21213 0
vsize: 85016
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 20710 0 0 0 31931 71 0 0 25 0 1 0 549725961 88948736 20340 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21716 20340 603 41 0 21675 0
vsize: 86864
[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 21179 0 0 0 32930 72 0 0 25 0 1 0 549725961 90828800 20809 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22175 20809 603 41 0 22134 0
vsize: 88700
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 21649 0 0 0 33930 73 0 0 25 0 1 0 549725961 92729344 21279 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22639 21279 603 41 0 22598 0
vsize: 90556
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 22115 0 0 0 34928 74 0 0 25 0 1 0 549725961 94670848 21745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23113 21745 603 41 0 23072 0
vsize: 92452
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 22495 0 0 0 35928 75 0 0 25 0 1 0 549725961 96317440 22125 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23515 22125 603 41 0 23474 0
vsize: 94060
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 22862 0 0 0 36927 77 0 0 25 0 1 0 549725961 98873344 22492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24139 22492 603 41 0 24098 0
vsize: 96556
[startup+380.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13364
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 23238 0 0 0 37926 78 0 0 25 0 1 0 549725961 100356096 22868 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24501 22868 603 41 0 24460 0
vsize: 98004
[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 23524 0 0 0 38925 79 0 0 25 0 1 0 549725961 101597184 23154 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24804 23154 603 41 0 24763 0
vsize: 99216
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 23789 0 0 0 39924 80 0 0 25 0 1 0 549725961 102674432 23419 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25067 23419 603 41 0 25026 0
vsize: 100268
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 24131 0 0 0 40923 81 0 0 25 0 1 0 549725961 103997440 23761 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25390 23761 603 41 0 25349 0
vsize: 101560
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 24378 0 0 0 41921 83 0 0 25 0 1 0 549725961 104947712 24008 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25622 24008 603 41 0 25581 0
vsize: 102488
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 24603 0 0 0 42921 84 0 0 25 0 1 0 549725961 105906176 24233 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25856 24233 603 41 0 25815 0
vsize: 103424
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 24865 0 0 0 43920 84 0 0 25 0 1 0 549725961 106979328 24495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26118 24495 603 41 0 26077 0
vsize: 104472
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 25148 0 0 0 44920 85 0 0 25 0 1 0 549725961 108220416 24778 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26421 24778 603 41 0 26380 0
vsize: 105684
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 25421 0 0 0 45918 86 0 0 25 0 1 0 549725961 109355008 25051 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26698 25051 603 41 0 26657 0
vsize: 106792
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 25832 0 0 0 46917 88 0 0 25 0 1 0 549725961 111022080 25462 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27105 25462 603 41 0 27064 0
vsize: 108420
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 26117 0 0 0 47916 89 0 0 25 0 1 0 549725961 112230400 25747 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27400 25747 603 41 0 27359 0
vsize: 109600
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 26485 0 0 0 48915 89 0 0 25 0 1 0 549725961 113754112 26115 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27772 26115 603 41 0 27731 0
vsize: 111088
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 26710 0 0 0 49915 90 0 0 25 0 1 0 549725961 114847744 26340 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28039 26340 603 41 0 27998 0
vsize: 112156
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 26954 0 0 0 50915 90 0 0 25 0 1 0 549725961 115843072 26584 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28282 26584 603 41 0 28241 0
vsize: 113128
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 27146 0 0 0 51914 91 0 0 25 0 1 0 549725961 116518912 26776 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28447 26776 603 41 0 28406 0
vsize: 113788
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 27402 0 0 0 52914 92 0 0 25 0 1 0 549725961 117624832 27032 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28717 27032 603 41 0 28676 0
vsize: 114868
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 27667 0 0 0 53914 92 0 0 25 0 1 0 549725961 118702080 27297 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28980 27297 603 41 0 28939 0
vsize: 115920
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 27902 0 0 0 54913 93 0 0 25 0 1 0 549725961 119775232 27532 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29242 27532 603 41 0 29201 0
vsize: 116968
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 28154 0 0 0 55913 93 0 0 25 0 1 0 549725961 120795136 27784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29491 27784 603 41 0 29450 0
vsize: 117964
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 28436 0 0 0 56912 94 0 0 25 0 1 0 549725961 121872384 28066 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29754 28066 603 41 0 29713 0
vsize: 119016
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 28689 0 0 0 57912 95 0 0 25 0 1 0 549725961 122994688 28319 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30028 28319 603 41 0 29987 0
vsize: 120112
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 29004 0 0 0 58912 95 0 0 25 0 1 0 549725961 124211200 28634 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30325 28634 603 41 0 30284 0
vsize: 121300
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 29206 0 0 0 59911 96 0 0 25 0 1 0 549725961 125022208 28836 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30523 28836 603 41 0 30482 0
vsize: 122092
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 29447 0 0 0 60910 96 0 0 25 0 1 0 549725961 126021632 29077 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30767 29077 603 41 0 30726 0
vsize: 123068
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 29694 0 0 0 61910 97 0 0 25 0 1 0 549725961 127107072 29324 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31032 29324 603 41 0 30991 0
vsize: 124128
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 29969 0 0 0 62909 99 0 0 25 0 1 0 549725961 128212992 29599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31302 29599 603 41 0 31261 0
vsize: 125208
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 30221 0 0 0 63908 99 0 0 25 0 1 0 549725961 129286144 29851 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31564 29851 603 41 0 31523 0
vsize: 126256
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 30467 0 0 0 64908 100 0 0 25 0 1 0 549725961 130228224 30097 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31794 30097 603 41 0 31753 0
vsize: 127176
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 30819 0 0 0 65907 101 0 0 25 0 1 0 549725961 131706880 30449 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32155 30449 603 41 0 32114 0
vsize: 128620
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 31010 0 0 0 66907 101 0 0 25 0 1 0 549725961 132390912 30640 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32322 30640 603 41 0 32281 0
vsize: 129288
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13366
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 31198 0 0 0 67906 102 0 0 25 0 1 0 549725961 133189632 30828 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32517 30829 603 41 0 32476 0
vsize: 130068
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 31402 0 0 0 68906 102 0 0 25 0 1 0 549725961 134004736 31032 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32716 31032 603 41 0 32675 0
vsize: 130864
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 31607 0 0 0 69906 103 0 0 25 0 1 0 549725961 134807552 31237 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32912 31237 603 41 0 32871 0
vsize: 131648
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 31872 0 0 0 70905 103 0 0 25 0 1 0 549725961 135905280 31502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33180 31502 603 41 0 33139 0
vsize: 132720
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.95 3/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 32105 0 0 0 71905 104 0 0 25 0 1 0 549725961 136876032 31735 4294967295 134512640 134672761 3221224544 3221223648 134555078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33417 31735 603 41 0 33376 0
vsize: 133668
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 32265 0 0 0 72905 104 0 0 25 0 1 0 549725961 137601024 31895 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33594 31895 603 41 0 33553 0
vsize: 134376
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 32425 0 0 0 73905 105 0 0 25 0 1 0 549725961 138293248 32055 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33763 32055 603 41 0 33722 0
vsize: 135052
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 32657 0 0 0 74904 105 0 0 25 0 1 0 549725961 139272192 32287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34002 32287 603 41 0 33961 0
vsize: 136008
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 32830 0 0 0 75904 105 0 0 25 0 1 0 549725961 140083200 32460 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34200 32460 603 41 0 34159 0
vsize: 136800
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 33036 0 0 0 76904 106 0 0 25 0 1 0 549725961 140881920 32666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34395 32666 603 41 0 34354 0
vsize: 137580
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 33181 0 0 0 77904 106 0 0 25 0 1 0 549725961 141443072 32811 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34532 32811 603 41 0 34491 0
vsize: 138128
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 33275 0 0 0 78904 107 0 0 25 0 1 0 549725961 141860864 32905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34634 32905 603 41 0 34593 0
vsize: 138536
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 33480 0 0 0 79903 107 0 0 25 0 1 0 549725961 142712832 33110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34842 33110 603 41 0 34801 0
vsize: 139368
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 33692 0 0 0 80903 108 0 0 25 0 1 0 549725961 143679488 33322 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35078 33322 603 41 0 35037 0
vsize: 140312
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 33854 0 0 0 81903 108 0 0 25 0 1 0 549725961 144338944 33484 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35239 33484 603 41 0 35198 0
vsize: 140956
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 34052 0 0 0 82903 108 0 0 25 0 1 0 549725961 145203200 33682 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35450 33682 603 41 0 35409 0
vsize: 141800
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 34260 0 0 0 83902 109 0 0 25 0 1 0 549725961 146026496 33890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35651 33890 603 41 0 35610 0
vsize: 142604
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 34471 0 0 0 84901 110 0 0 25 0 1 0 549725961 146948096 34101 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35876 34101 603 41 0 35835 0
vsize: 143504
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 34671 0 0 0 85900 111 0 0 25 0 1 0 549725961 147755008 34301 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36073 34301 603 41 0 36032 0
vsize: 144292
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 35082 0 0 0 86899 112 0 0 25 0 1 0 549725961 149385216 34712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36471 34712 603 41 0 36430 0
vsize: 145884
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 35249 0 0 0 87899 112 0 0 25 0 1 0 549725961 150147072 34879 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36657 34879 603 41 0 36616 0
vsize: 146628
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 35420 0 0 0 88899 112 0 0 25 0 1 0 549725961 150847488 35050 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36828 35050 603 41 0 36787 0
vsize: 147312
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 35606 0 0 0 89899 113 0 0 25 0 1 0 549725961 151523328 35236 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36993 35236 603 41 0 36952 0
vsize: 147972
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 35775 0 0 0 90899 113 0 0 25 0 1 0 549725961 152338432 35405 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37192 35405 603 41 0 37151 0
vsize: 148768
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 36029 0 0 0 91898 114 0 0 25 0 1 0 549725961 153350144 35659 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37439 35659 603 41 0 37398 0
vsize: 149756
[startup+930.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 36191 0 0 0 92898 115 0 0 25 0 1 0 549725961 154062848 35821 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37613 35821 603 41 0 37572 0
vsize: 150452
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 36380 0 0 0 93898 115 0 0 25 0 1 0 549725961 154796032 36010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37792 36010 603 41 0 37751 0
vsize: 151168
[startup+950.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 36616 0 0 0 94896 116 0 0 25 0 1 0 549725961 155734016 36246 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38021 36246 603 41 0 37980 0
vsize: 152084
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 36691 0 0 0 95896 117 0 0 25 0 1 0 549725961 156004352 36321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38087 36321 603 41 0 38046 0
vsize: 152348
[startup+970.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 36839 0 0 0 96896 117 0 0 25 0 1 0 549725961 156737536 36469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38266 36469 603 41 0 38225 0
vsize: 153064
[startup+980.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13368
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 36968 0 0 0 97896 118 0 0 25 0 1 0 549725961 157143040 36598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38365 36598 603 41 0 38324 0
vsize: 153460
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 37138 0 0 0 98895 118 0 0 25 0 1 0 549725961 157958144 36768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38564 36768 603 41 0 38523 0
vsize: 154256
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 37295 0 0 0 99895 119 0 0 25 0 1 0 549725961 158507008 36925 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38698 36925 603 41 0 38657 0
vsize: 154792
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 37441 0 0 0 100895 119 0 0 25 0 1 0 549725961 159186944 37071 4294967295 134512640 134672761 3221224544 3221223728 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38864 37071 603 41 0 38823 0
vsize: 155456
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 37640 0 0 0 101894 120 0 0 25 0 1 0 549725961 159887360 37270 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39035 37270 603 41 0 38994 0
vsize: 156140
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 37777 0 0 0 102894 120 0 0 25 0 1 0 549725961 160555008 37407 4294967295 134512640 134672761 3221224544 3221223728 134558918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39198 37407 603 41 0 39157 0
vsize: 156792
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 37989 0 0 0 103894 121 0 0 25 0 1 0 549725961 161366016 37619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39396 37619 603 41 0 39355 0
vsize: 157584
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 38148 0 0 0 104894 121 0 0 25 0 1 0 549725961 162033664 37778 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39559 37778 603 41 0 39518 0
vsize: 158236
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 38347 0 0 0 105897 122 0 0 25 0 1 0 549725961 162836480 37977 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39755 37977 603 41 0 39714 0
vsize: 159020
[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 38602 0 0 0 106900 123 0 0 25 0 1 0 549725961 164028416 38232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40046 38232 603 41 0 40005 0
vsize: 160184
[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 38742 0 0 0 107900 123 0 0 25 0 1 0 549725961 164601856 38372 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40186 38372 603 41 0 40145 0
vsize: 160744
[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 38901 0 0 0 108900 123 0 0 25 0 1 0 549725961 165163008 38531 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40323 38531 603 41 0 40282 0
vsize: 161292
[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 39051 0 0 0 109900 124 0 0 25 0 1 0 549725961 165859328 38681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40493 38681 603 41 0 40452 0
vsize: 161972
[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 39213 0 0 0 110900 124 0 0 25 0 1 0 549725961 166580224 38843 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40669 38843 603 41 0 40628 0
vsize: 162676
[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 39405 0 0 0 111899 125 0 0 25 0 1 0 549725961 167403520 39035 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40870 39035 603 41 0 40829 0
vsize: 163480
[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 39555 0 0 0 112899 125 0 0 25 0 1 0 549725961 170078208 39185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41523 39185 603 41 0 41482 0
vsize: 166092
[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 40171 0 0 0 113898 126 0 0 25 0 1 0 549725961 172654592 39801 4294967295 134512640 134672761 3221224544 3221223776 134541834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42152 39801 603 41 0 42111 0
vsize: 168608
[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 40718 0 0 0 114897 128 0 0 25 0 1 0 549725961 174813184 40348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42679 40348 603 41 0 42638 0
vsize: 170716
[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 41379 0 0 0 115895 130 0 0 25 0 1 0 549725961 177508352 41009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43337 41009 603 41 0 43296 0
vsize: 173348
[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 41976 0 0 0 116894 131 0 0 25 0 1 0 549725961 179924992 41606 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43927 41606 603 41 0 43886 0
vsize: 175708
[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 42485 0 0 0 117892 133 0 0 25 0 1 0 549725961 181985280 42115 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44430 42115 603 41 0 44389 0
vsize: 177720
[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 42952 0 0 0 118891 134 0 0 25 0 1 0 549725961 183894016 42582 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44896 42582 603 41 0 44855 0
vsize: 179584
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 13370
Raw data (stat): 13362 (minisat+) R 13361 22929 22928 0 -1 0 43372 0 0 0 119890 136 0 0 25 0 1 0 549725961 185647104 43002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45324 43002 603 41 0 45283 0
vsize: 181296
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.97 0.95 1/55 13370
Raw data (stat): 13362 (minisat+) Z 13361 22929 22928 0 -1 12 43374 0 0 0 119890 143 0 0 25 0 1 0 549725961 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.2
CPU time (s): 1200.34
CPU user time (s): 1198.9
CPU system time (s): 1.43978
CPU usage (%): 100.012
Max. virtual memory (Kb): 181296
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####