PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-fit1d.opb
MD5SUM	6bb160e5eb0ef9c02ca7232f62836f2b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	8436
Biggest coefficient in the objective function	368640
Number of bits for the biggest coefficient in the objective function	19
Sum of the numbers in the objective function	57614442
Number of bits of the sum of numbers in the objective function	26
Biggest number in a constraint	483840
Number of bits of the biggest number in a constraint	19
Biggest sum of numbers in a constraint	72412534
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1195.48
Number of variables	8436
Total number of constraints	1050
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1050
Minimum length of a constraint	8
Maximum length of a constraint	8436
Trace number 19951

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        577800 kB
Buffers:         22584 kB
Cached:         412176 kB
SwapCached:        304 kB
Active:         116924 kB
Inactive:       320364 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        577548 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6448 kB
Slab:            13996 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 20:15:44 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 15779 7 1200.33 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1051 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): (none)
c ---[1050]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1049]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1048]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1047]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1046]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1045]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1044]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1043]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1042]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1041]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1040]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1039]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1038]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1037]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1036]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1035]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1034]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1033]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1032]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1031]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1030]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1029]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1028]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1027]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1026]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1025]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1024]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1023]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1022]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1021]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1020]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1019]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1018]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1017]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1016]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1015]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1014]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1013]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1012]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1011]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1010]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1009]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1008]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1007]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1006]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1005]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1004]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1003]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1002]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1001]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[1000]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 999]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 998]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 997]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 996]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 995]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 994]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 993]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 992]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 991]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 990]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 989]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 988]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 987]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 986]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 985]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 984]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 983]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 982]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 981]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 980]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 979]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 978]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 977]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 976]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 975]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 974]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 973]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 972]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 971]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 970]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 969]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 968]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 967]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 966]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 965]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 964]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 963]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 962]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 961]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 960]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 959]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 958]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 957]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 956]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 955]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 954]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 953]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 952]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 951]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 950]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 949]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 948]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 947]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 946]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 945]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 944]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 943]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 942]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 941]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 940]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 939]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 938]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 937]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 936]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 935]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 934]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 933]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 932]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 931]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 930]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 929]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 928]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 927]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 926]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 925]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 924]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 923]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 922]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 921]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 920]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 919]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 918]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 917]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 916]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 915]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 914]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 913]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 912]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 911]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 910]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 909]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 908]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 907]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 906]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 905]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 904]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 903]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 902]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 901]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 900]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 899]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 898]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 897]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 896]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 895]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 894]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 893]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 892]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 891]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 890]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 889]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 888]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 887]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 886]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 885]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 884]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 883]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 882]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 881]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 880]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 879]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 878]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 877]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 876]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 875]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 874]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 873]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 872]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 871]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 870]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 869]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 868]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 867]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 866]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 865]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 864]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 863]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 862]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 861]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 860]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 859]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 858]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 857]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 856]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 855]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 854]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 853]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 852]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 851]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 850]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 849]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 848]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 847]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 846]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 845]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 844]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 843]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 842]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 841]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 840]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 839]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 838]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 837]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 836]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 835]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 834]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 833]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 832]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 831]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 830]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 829]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 828]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 827]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 826]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 825]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 824]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 823]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 822]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 821]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 820]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 819]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 818]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 817]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 816]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 815]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 814]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 813]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 812]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 811]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 810]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 809]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 808]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 807]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 806]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 805]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 804]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 803]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 802]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 801]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 800]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 799]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 798]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 797]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 796]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 795]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 794]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 793]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 792]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 791]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 790]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 789]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 788]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 787]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 786]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 785]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 784]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 783]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 782]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 781]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 780]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 779]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 778]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 777]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 776]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 775]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 774]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 773]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 772]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 771]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 770]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 769]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 768]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 767]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 766]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 765]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 764]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 763]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 762]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 761]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 760]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 759]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 758]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 757]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 756]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 755]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 754]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 753]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 752]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 751]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 750]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 749]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 748]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 747]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 746]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 745]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 744]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 743]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 742]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 741]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 740]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 739]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 738]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 737]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 736]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 735]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 734]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 733]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 732]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 731]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 730]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 729]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 728]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 727]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 726]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 725]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 724]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 723]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 722]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 721]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 720]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 719]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 718]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 717]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 716]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 715]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 714]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 713]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 712]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 711]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 710]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 709]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 708]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 707]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 706]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 705]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 704]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 703]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 702]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 701]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 700]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 699]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 698]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 697]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 696]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 695]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 694]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 693]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 692]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 691]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 690]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 689]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 688]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 687]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 686]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 685]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 684]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 683]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 682]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 681]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 680]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 679]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 678]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 677]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 676]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 675]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 674]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 673]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 672]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 671]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 670]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 669]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 668]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 667]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 666]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 665]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 664]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 663]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 662]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 661]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 660]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 659]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 658]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 657]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 656]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 655]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 654]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 653]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 652]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 651]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 650]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 649]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 648]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 647]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 646]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 645]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 644]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 643]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 642]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 641]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 640]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 639]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 638]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 637]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 636]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 635]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 634]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 633]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 632]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 631]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 630]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 629]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 628]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 627]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 626]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 625]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 624]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 623]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 622]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 621]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 620]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 619]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 618]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 617]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 616]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 615]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 614]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 613]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 612]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 611]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 610]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 609]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 608]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 607]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 606]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 605]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 604]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 603]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 602]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 601]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 600]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 599]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 598]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 597]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 596]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 595]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 594]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 593]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 592]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 591]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 590]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 589]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 588]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 587]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 586]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 585]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 584]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 583]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 582]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 581]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 580]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 579]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 578]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 577]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 576]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 575]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 574]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 573]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 572]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 571]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 570]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 569]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 568]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 567]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 566]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 565]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 564]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 563]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 562]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 561]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 560]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 559]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 558]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 557]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 556]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 555]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 554]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 553]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 552]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 551]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 550]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 549]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 548]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 547]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 546]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 545]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 544]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 543]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 542]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 541]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 540]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 539]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 538]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 537]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 536]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 535]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 534]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 533]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 532]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 531]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 530]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 529]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 528]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 527]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 526]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 525]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 524]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 523]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 522]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 521]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 520]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 519]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 518]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 517]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 516]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 515]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 514]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 513]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 512]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 511]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 510]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 509]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 508]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 507]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 506]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 505]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 504]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 503]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 502]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 501]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 500]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 499]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 498]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 497]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 496]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 495]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 494]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 493]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 492]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 491]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 490]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 489]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 488]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 487]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 486]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 485]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 484]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 483]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 482]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 481]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 480]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 479]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 478]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 477]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 476]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 475]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 474]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 473]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 472]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 471]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 470]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 469]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 468]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 467]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 466]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 465]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 464]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 463]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 462]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 461]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 460]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 459]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 458]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 457]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 456]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 455]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 454]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 453]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 452]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 451]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 450]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 449]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 448]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 447]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 446]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 445]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 444]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 443]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 442]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 441]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 440]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 439]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 438]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 437]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 436]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 435]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 434]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 433]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 432]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 431]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 430]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 429]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 428]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 427]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 426]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 425]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 424]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 423]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 422]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 421]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 420]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 419]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 418]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 417]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 416]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 415]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 414]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 413]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 412]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 411]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 410]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 409]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 408]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 407]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 406]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 405]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 404]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 403]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 402]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 401]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 400]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 399]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 398]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 397]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 396]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 395]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 394]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 393]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 392]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 391]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 390]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 389]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 388]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 387]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 386]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 385]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 384]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 383]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 382]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 381]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 380]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 379]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 378]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 377]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 376]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 375]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 374]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 373]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 372]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 371]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 370]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 369]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 368]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 367]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 366]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 365]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 364]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 363]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 362]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 361]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 360]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 359]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 358]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 357]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 356]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 355]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 354]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 353]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 352]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 351]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 350]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 349]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 348]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 347]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 346]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 345]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 344]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 343]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 342]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 341]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 340]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 339]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 338]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 337]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 336]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 335]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 334]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 333]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 332]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 331]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 330]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 329]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 328]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 327]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 326]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 325]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 324]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 323]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 322]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 321]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 320]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 319]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 318]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 317]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 316]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 315]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 314]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 313]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 312]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 311]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 310]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 309]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 308]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 307]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 306]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 305]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 304]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 303]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 302]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 301]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 300]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 299]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 298]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 297]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 296]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 295]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 294]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 293]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 292]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 291]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 290]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 289]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 288]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 287]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 286]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 285]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 284]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 283]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 282]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 281]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 280]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 279]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 278]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 277]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 276]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 275]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 274]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 273]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 272]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 271]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 270]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 269]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 268]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 267]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 266]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 265]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 264]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 263]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 262]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 261]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 260]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 259]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 258]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 257]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 256]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 255]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 254]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 253]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 252]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 251]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 250]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 249]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 248]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 247]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 246]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 245]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 244]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 243]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 242]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 241]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 240]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 239]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 238]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 237]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 236]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 235]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 234]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 233]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 232]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 231]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 230]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 229]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 228]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 227]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 226]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 225]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 224]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 223]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 222]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 221]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 220]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 219]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 218]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 217]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 216]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 215]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 214]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 213]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 212]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 211]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 210]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 209]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 208]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 207]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 206]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 205]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 204]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 203]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 202]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 201]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 200]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 199]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 198]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 197]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 196]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 195]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 194]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 193]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 192]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 191]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 190]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 189]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 188]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 187]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 186]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 185]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 184]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 183]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 182]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 181]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 180]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 179]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 178]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 177]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 176]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 175]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 174]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 173]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 172]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 171]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 170]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 169]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 168]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 167]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 166]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 165]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 164]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 163]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 162]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 161]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 160]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 159]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 158]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 157]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 156]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 155]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 154]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 153]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 152]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 151]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 150]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 149]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 148]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 147]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 146]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 145]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 144]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 143]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 142]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 141]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 140]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 139]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 138]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 137]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 136]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 135]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 134]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 133]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 132]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 131]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 130]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 129]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 128]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 127]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 126]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 125]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 124]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 123]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 122]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 121]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 120]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 119]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 118]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 117]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 116]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 115]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 114]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 113]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 112]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 111]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 110]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 109]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 108]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 107]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 106]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 105]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 104]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 103]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 102]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 101]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[ 100]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  99]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  98]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  97]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  96]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  95]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  94]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  93]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  92]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  91]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  90]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  89]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  88]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  87]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  86]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  85]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  84]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  83]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  82]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  81]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  80]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  79]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  78]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  77]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  76]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  75]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  74]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  73]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  72]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  71]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  70]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  69]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  68]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  67]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  66]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  65]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  64]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  63]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  62]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  61]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  60]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  59]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  58]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  57]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  56]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  55]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  54]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  53]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  52]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  51]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  50]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  49]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  48]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  47]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  46]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  45]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  44]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  43]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  42]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  41]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  40]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  39]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  38]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  37]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  36]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  35]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  34]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  33]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  32]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  31]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  30]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  29]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  28]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  27]---> Adder-cost: 27   maxlim: 126   bits: 8/7
c ---[  23]---> Adder-cost: 16837   maxlim: 101745   bits: 18/17
c ---[  22]---> Adder-cost: 35787   maxlim: 6633569   bits: 24/23
c ---[  21]---> Adder-cost: 18126   maxlim: 4660379   bits: 24/23
c ---[  20]---> Adder-cost: 13526   maxlim: 7782034   bits: 24/23
c ---[  19]---> Adder-cost: 46920   maxlim: 49412548   bits: 27/26
c ---[  18]---> Adder-cost: 7270   maxlim: 202757   bits: 18/18
c ---[  17]---> Adder-cost: 28854   maxlim: 3340290   bits: 23/22
c ---[  16]---> Adder-cost: 44525   maxlim: 3367019   bits: 23/22
c ---[  15]---> Adder-cost: 37629   maxlim: 7305239   bits: 24/23
c ---[  14]---> Adder-cost: 14038   maxlim: 171104   bits: 19/18
c ---[  13]---> Adder-cost: 18310   maxlim: 585650   bits: 20/20
c ---[  12]---> Adder-cost: 51276   maxlim: 48594727   bits: 27/26
c ---[  11]---> Adder-cost: 2096   maxlim: 88902   bits: 17/17
c ---[  10]---> Adder-cost: 8416   maxlim: 4571464   bits: 23/23
c ---[   9]---> Adder-cost: 28701   maxlim: 3985139   bits: 23/22
c ---[   8]---> Adder-cost: 4168   maxlim: 64077   bits: 17/16
c ---[   7]---> Adder-cost: 4299   maxlim: 30599   bits: 16/15
c ---[   6]---> Adder-cost: 4676   maxlim: 35189   bits: 17/16
c ---[   5]---> Adder-cost: 8358   maxlim: 67319   bits: 18/17
c ---[   4]---> Adder-cost: 4270   maxlim: 73024   bits: 17/17
c ---[   3]---> Adder-cost: 3309   maxlim: 24989   bits: 16/15
c ---[   2]---> Adder-cost: 2149   maxlim: 15809   bits: 15/14
c ---[   1]---> Adder-cost: 5642   maxlim: 93949   bits: 18/17
c ---[   0]---> Adder-cost: 3842   maxlim: 34424   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 3002136 10736217 | 1000712       0        0     nan |  0.000 % |
c |       100 | 3002136 10736217 | 1100783     100      317     3.2 |  1.670 % |
c |       250 | 3002136 10736217 | 1210861     250      804     3.2 |  1.670 % |
c |       475 | 3002136 10736217 | 1331947     475     1638     3.4 |  1.670 % |
c |       812 | 3002136 10736217 | 1465142     812     2873     3.5 |  1.670 % |
c |      1318 | 3002136 10736217 | 1611656    1318     4537     3.4 |  1.670 % |
c |      2077 | 3002136 10736217 | 1772822    2077     7388     3.6 |  1.670 % |
c |      3216 | 3002136 10736217 | 1950104    3216    17894     5.6 |  1.670 % |
c |      4924 | 3002136 10736217 | 2145115    4924    25066     5.1 |  1.670 % |
c |      7486 | 3002136 10736217 | 2359626    7486    34560     4.6 |  1.670 % |
c |     11330 | 3002136 10736217 | 2595589   11330   152997    13.5 |  1.670 % |
c |     17096 | 3002136 10736217 | 2855148   17096   174704    10.2 |  1.670 % |
c |     25745 | 3002136 10736217 | 3140662   25745   343429    13.3 |  1.670 % |
c |     38719 | 3002129 10736194 | 3454729   38718   409148    10.6 |  1.671 % |
c |     58181 | 3002117 10736160 | 3800202   58178   561438     9.7 |  1.671 % |
c |     87373 | 3002117 10736160 | 4180222   87370   850307     9.7 |  1.671 % |
c |    131163 | 3002117 10736160 | 4598244  131160  2559697    19.5 |  1.671 % |
c |    196847 | 3002117 10736160 | 5058069  196844  4273945    21.7 |  1.671 % |
#### 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.73 0.78 0.83 2/54 16446
Raw data (stat): 16446 (runsolver) R 16445 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489548553 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.77 0.78 0.83 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 40442 0 0 0 904 94 0 0 25 0 1 0 489548553 180285440 38300 4294967295 134512640 134672761 3221224544 3221216656 134553512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44015 38300 603 41 0 43974 0
vsize: 176060
[startup+20.0002 s]
Raw data (loadavg): 0.80 0.79 0.83 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 50648 0 0 0 1881 117 0 0 25 0 1 0 489548553 213274624 48506 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52069 48506 603 41 0 52028 0
vsize: 208276
[startup+30.0008 s]
Raw data (loadavg): 0.83 0.80 0.83 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 51208 0 0 0 2879 119 0 0 25 0 1 0 489548553 215568384 49066 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52629 49066 603 41 0 52588 0
vsize: 210516
[startup+39.9997 s]
Raw data (loadavg): 0.86 0.80 0.83 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 51614 0 0 0 3877 120 0 0 25 0 1 0 489548553 217214976 49472 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53031 49472 603 41 0 52990 0
vsize: 212124
[startup+50.0009 s]
Raw data (loadavg): 0.88 0.81 0.83 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 51890 0 0 0 4877 121 0 0 25 0 1 0 489548553 218357760 49748 4294967295 134512640 134672761 3221224544 3221223744 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53310 49748 603 41 0 53269 0
vsize: 213240
[startup+60.0013 s]
Raw data (loadavg): 0.90 0.81 0.83 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 52292 0 0 0 5875 122 0 0 25 0 1 0 489548553 219979776 50150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53706 50150 603 41 0 53665 0
vsize: 214824
[startup+70.0016 s]
Raw data (loadavg): 0.91 0.82 0.83 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 52513 0 0 0 6875 123 0 0 25 0 1 0 489548553 220925952 50371 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53937 50371 603 41 0 53896 0
vsize: 215748
[startup+80.0026 s]
Raw data (loadavg): 0.93 0.83 0.83 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 52671 0 0 0 7874 124 0 0 25 0 1 0 489548553 221466624 50529 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54069 50529 603 41 0 54028 0
vsize: 216276
[startup+90.0022 s]
Raw data (loadavg): 0.94 0.83 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 52818 0 0 0 8874 124 0 0 25 0 1 0 489548553 222142464 50676 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54234 50676 603 41 0 54193 0
vsize: 216936
[startup+100.003 s]
Raw data (loadavg): 0.95 0.84 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 52952 0 0 0 9874 125 0 0 25 0 1 0 489548553 222683136 50810 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54366 50810 603 41 0 54325 0
vsize: 217464
[startup+110.002 s]
Raw data (loadavg): 0.95 0.84 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53082 0 0 0 10873 125 0 0 25 0 1 0 489548553 223223808 50940 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54498 50940 603 41 0 54457 0
vsize: 217992
[startup+120.003 s]
Raw data (loadavg): 0.96 0.85 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53196 0 0 0 11873 125 0 0 25 0 1 0 489548553 223756288 51054 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54628 51054 603 41 0 54587 0
vsize: 218512
[startup+130.002 s]
Raw data (loadavg): 0.97 0.85 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53297 0 0 0 12873 126 0 0 25 0 1 0 489548553 224161792 51155 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54727 51155 603 41 0 54686 0
vsize: 218908
[startup+140.002 s]
Raw data (loadavg): 0.97 0.85 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53395 0 0 0 13873 126 0 0 25 0 1 0 489548553 224567296 51253 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54826 51253 603 41 0 54785 0
vsize: 219304
[startup+150.003 s]
Raw data (loadavg): 0.98 0.86 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53483 0 0 0 14873 126 0 0 25 0 1 0 489548553 224837632 51341 4294967295 134512640 134672761 3221224544 3221223552 1075350469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54892 51341 603 41 0 54851 0
vsize: 219568
[startup+160.002 s]
Raw data (loadavg): 0.98 0.86 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53555 0 0 0 15873 126 0 0 25 0 1 0 489548553 225243136 51413 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54991 51413 603 41 0 54950 0
vsize: 219964
[startup+170.003 s]
Raw data (loadavg): 0.98 0.87 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53633 0 0 0 16873 127 0 0 25 0 1 0 489548553 225509376 51491 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55056 51491 603 41 0 55015 0
vsize: 220224
[startup+180.003 s]
Raw data (loadavg): 0.98 0.87 0.84 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53700 0 0 0 17873 127 0 0 25 0 1 0 489548553 225779712 51558 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55122 51558 603 41 0 55081 0
vsize: 220488
[startup+190.002 s]
Raw data (loadavg): 0.99 0.87 0.85 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53773 0 0 0 18873 127 0 0 25 0 1 0 489548553 226050048 51631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55188 51631 603 41 0 55147 0
vsize: 220752
[startup+200.002 s]
Raw data (loadavg): 0.99 0.88 0.85 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53847 0 0 0 19873 127 0 0 25 0 1 0 489548553 226320384 51705 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55254 51705 603 41 0 55213 0
vsize: 221016
[startup+210.008 s]
Raw data (loadavg): 0.99 0.88 0.85 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53897 0 0 0 20873 128 0 0 25 0 1 0 489548553 226455552 51755 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55287 51755 603 41 0 55246 0
vsize: 221148
[startup+220.014 s]
Raw data (loadavg): 0.99 0.89 0.85 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53948 0 0 0 21874 128 0 0 25 0 1 0 489548553 226725888 51806 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55353 51806 603 41 0 55312 0
vsize: 221412
[startup+230.014 s]
Raw data (loadavg): 0.99 0.89 0.85 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 53999 0 0 0 22874 128 0 0 25 0 1 0 489548553 226861056 51857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55386 51857 603 41 0 55345 0
vsize: 221544
[startup+240.014 s]
Raw data (loadavg): 0.99 0.89 0.85 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54046 0 0 0 23873 128 0 0 25 0 1 0 489548553 227131392 51904 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55452 51904 603 41 0 55411 0
vsize: 221808
[startup+250.014 s]
Raw data (loadavg): 0.99 0.89 0.85 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54097 0 0 0 24873 129 0 0 25 0 1 0 489548553 227266560 51955 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55485 51955 603 41 0 55444 0
vsize: 221940
[startup+260.014 s]
Raw data (loadavg): 0.99 0.90 0.85 2/54 16446
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54179 0 0 0 25873 129 0 0 25 0 1 0 489548553 227672064 52037 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55584 52037 603 41 0 55543 0
vsize: 222336
[startup+270.018 s]
Raw data (loadavg): 1.07 0.92 0.86 2/54 16499
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54254 0 0 0 26873 130 0 0 25 0 1 0 489548553 227942400 52112 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55650 52112 603 41 0 55609 0
vsize: 222600
[startup+280.018 s]
Raw data (loadavg): 1.06 0.92 0.86 2/54 16499
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54304 0 0 0 27873 130 0 0 25 0 1 0 489548553 228077568 52162 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55683 52162 603 41 0 55642 0
vsize: 222732
[startup+290.017 s]
Raw data (loadavg): 1.05 0.92 0.86 2/54 16499
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54347 0 0 0 28873 130 0 0 25 0 1 0 489548553 228347904 52205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55749 52205 603 41 0 55708 0
vsize: 222996
[startup+300.021 s]
Raw data (loadavg): 1.04 0.92 0.86 2/54 16499
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54393 0 0 0 29872 130 0 0 25 0 1 0 489548553 228483072 52251 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55782 52251 603 41 0 55741 0
vsize: 223128
[startup+310.021 s]
Raw data (loadavg): 1.04 0.92 0.86 2/54 16499
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54434 0 0 0 30871 131 0 0 25 0 1 0 489548553 228618240 52292 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55815 52292 603 41 0 55774 0
vsize: 223260
[startup+320.022 s]
Raw data (loadavg): 1.03 0.93 0.86 2/54 16499
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54479 0 0 0 31871 131 0 0 25 0 1 0 489548553 228753408 52337 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55848 52337 603 41 0 55807 0
vsize: 223392
[startup+330.022 s]
Raw data (loadavg): 1.03 0.93 0.86 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54632 0 0 0 32870 132 0 0 25 0 1 0 489548553 229425152 52490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56012 52490 603 41 0 55971 0
vsize: 224048
[startup+340.022 s]
Raw data (loadavg): 1.02 0.93 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54667 0 0 0 33870 133 0 0 25 0 1 0 489548553 229822464 52525 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56109 52525 603 41 0 56068 0
vsize: 224436
[startup+350.023 s]
Raw data (loadavg): 1.02 0.93 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54712 0 0 0 34869 133 0 0 25 0 1 0 489548553 229957632 52570 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56142 52570 603 41 0 56101 0
vsize: 224568
[startup+360.023 s]
Raw data (loadavg): 1.01 0.93 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54756 0 0 0 35869 134 0 0 25 0 1 0 489548553 230092800 52614 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56175 52614 603 41 0 56134 0
vsize: 224700
[startup+370.024 s]
Raw data (loadavg): 1.01 0.94 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54820 0 0 0 36869 134 0 0 25 0 1 0 489548553 230367232 52678 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56242 52678 603 41 0 56201 0
vsize: 224968
[startup+380.024 s]
Raw data (loadavg): 1.01 0.94 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54860 0 0 0 37869 134 0 0 25 0 1 0 489548553 230502400 52718 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56275 52718 603 41 0 56234 0
vsize: 225100
[startup+390.023 s]
Raw data (loadavg): 1.01 0.94 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54893 0 0 0 38870 134 0 0 25 0 1 0 489548553 230637568 52751 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56308 52751 603 41 0 56267 0
vsize: 225232
[startup+400.024 s]
Raw data (loadavg): 1.01 0.94 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54934 0 0 0 39870 134 0 0 25 0 1 0 489548553 230772736 52792 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56341 52792 603 41 0 56300 0
vsize: 225364
[startup+410.024 s]
Raw data (loadavg): 1.00 0.94 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 54993 0 0 0 40870 134 0 0 25 0 1 0 489548553 231043072 52851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56407 52851 603 41 0 56366 0
vsize: 225628
[startup+420.024 s]
Raw data (loadavg): 1.00 0.94 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55022 0 0 0 41870 134 0 0 25 0 1 0 489548553 231178240 52880 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56440 52880 603 41 0 56399 0
vsize: 225760
[startup+430.025 s]
Raw data (loadavg): 1.00 0.94 0.87 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55050 0 0 0 42870 134 0 0 25 0 1 0 489548553 231313408 52908 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56473 52908 603 41 0 56432 0
vsize: 225892
[startup+440.024 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55099 0 0 0 43870 134 0 0 25 0 1 0 489548553 231448576 52957 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56506 52957 603 41 0 56465 0
vsize: 226024
[startup+450.025 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55125 0 0 0 44870 134 0 0 25 0 1 0 489548553 231583744 52983 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56539 52983 603 41 0 56498 0
vsize: 226156
[startup+460.025 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55149 0 0 0 45870 134 0 0 25 0 1 0 489548553 231583744 53007 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56539 53007 603 41 0 56498 0
vsize: 226156
[startup+470.026 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55171 0 0 0 46870 135 0 0 25 0 1 0 489548553 231718912 53029 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56572 53029 603 41 0 56531 0
vsize: 226288
[startup+480.026 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55194 0 0 0 47870 135 0 0 25 0 1 0 489548553 231854080 53052 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56605 53052 603 41 0 56564 0
vsize: 226420
[startup+490.026 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55212 0 0 0 48870 135 0 0 25 0 1 0 489548553 231854080 53070 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56605 53070 603 41 0 56564 0
vsize: 226420
[startup+500.026 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55234 0 0 0 49871 135 0 0 25 0 1 0 489548553 231989248 53092 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56638 53092 603 41 0 56597 0
vsize: 226552
[startup+510.026 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55256 0 0 0 50871 135 0 0 25 0 1 0 489548553 232124416 53114 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56671 53114 603 41 0 56630 0
vsize: 226684
[startup+520.026 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55277 0 0 0 51871 135 0 0 25 0 1 0 489548553 232124416 53135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56671 53135 603 41 0 56630 0
vsize: 226684
[startup+530.026 s]
Raw data (loadavg): 1.00 0.95 0.88 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55301 0 0 0 52871 135 0 0 25 0 1 0 489548553 232259584 53159 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56704 53159 603 41 0 56663 0
vsize: 226816
[startup+540.027 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55332 0 0 0 53871 135 0 0 25 0 1 0 489548553 232259584 53190 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56704 53190 603 41 0 56663 0
vsize: 226816
[startup+550.028 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55350 0 0 0 54871 136 0 0 25 0 1 0 489548553 232394752 53208 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56737 53208 603 41 0 56696 0
vsize: 226948
[startup+560.028 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55458 0 0 0 55870 136 0 0 25 0 1 0 489548553 232800256 53316 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56836 53316 603 41 0 56795 0
vsize: 227344
[startup+570.029 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55618 0 0 0 56869 137 0 0 25 0 1 0 489548553 233472000 53476 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57000 53476 603 41 0 56959 0
vsize: 228000
[startup+580.029 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55639 0 0 0 57870 137 0 0 25 0 1 0 489548553 233607168 53497 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57033 53497 603 41 0 56992 0
vsize: 228132
[startup+590.029 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55657 0 0 0 58870 137 0 0 25 0 1 0 489548553 233607168 53515 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57033 53515 603 41 0 56992 0
vsize: 228132
[startup+600.029 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55686 0 0 0 59870 137 0 0 25 0 1 0 489548553 233742336 53544 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57066 53544 603 41 0 57025 0
vsize: 228264
[startup+610.03 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55713 0 0 0 60870 137 0 0 25 0 1 0 489548553 233742336 53571 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57066 53571 603 41 0 57025 0
vsize: 228264
[startup+620.031 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55731 0 0 0 61870 137 0 0 25 0 1 0 489548553 233877504 53589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57099 53589 603 41 0 57058 0
vsize: 228396
[startup+630.03 s]
Raw data (loadavg): 1.00 0.96 0.89 2/54 16501
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55753 0 0 0 62871 137 0 0 25 0 1 0 489548553 234012672 53611 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57132 53611 603 41 0 57091 0
vsize: 228528
[startup+640.031 s]
Raw data (loadavg): 1.00 0.97 0.89 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55773 0 0 0 63871 137 0 0 25 0 1 0 489548553 234012672 53631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57132 53631 603 41 0 57091 0
vsize: 228528
[startup+650.032 s]
Raw data (loadavg): 1.00 0.97 0.90 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55791 0 0 0 64871 138 0 0 25 0 1 0 489548553 234147840 53649 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57165 53649 603 41 0 57124 0
vsize: 228660
[startup+660.032 s]
Raw data (loadavg): 1.00 0.97 0.90 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55811 0 0 0 65871 138 0 0 25 0 1 0 489548553 234147840 53669 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57165 53669 603 41 0 57124 0
vsize: 228660
[startup+670.033 s]
Raw data (loadavg): 1.00 0.97 0.90 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55838 0 0 0 66871 138 0 0 25 0 1 0 489548553 234283008 53696 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57198 53696 603 41 0 57157 0
vsize: 228792
[startup+680.034 s]
Raw data (loadavg): 1.00 0.97 0.90 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 55860 0 0 0 67871 138 0 0 25 0 1 0 489548553 234418176 53718 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57231 53718 603 41 0 57190 0
vsize: 228924
[startup+690.033 s]
Raw data (loadavg): 1.00 0.97 0.90 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 56511 0 0 0 68869 140 0 0 25 0 1 0 489548553 236982272 54369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57857 54369 603 41 0 57816 0
vsize: 231428
[startup+700.034 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 57248 0 0 0 69867 142 0 0 25 0 1 0 489548553 239947776 55106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58581 55106 603 41 0 58540 0
vsize: 234324
[startup+710.035 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 57629 0 0 0 70865 144 0 0 25 0 1 0 489548553 242110464 55487 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59109 55487 603 41 0 59068 0
vsize: 236436
[startup+720.035 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 57650 0 0 0 71866 144 0 0 25 0 1 0 489548553 242245632 55508 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59142 55508 603 41 0 59101 0
vsize: 236568
[startup+730.036 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 57674 0 0 0 72866 144 0 0 25 0 1 0 489548553 242245632 55532 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59142 55532 603 41 0 59101 0
vsize: 236568
[startup+740.035 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 57703 0 0 0 73866 144 0 0 25 0 1 0 489548553 242380800 55561 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59175 55561 603 41 0 59134 0
vsize: 236700
[startup+750.036 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 57719 0 0 0 74866 144 0 0 25 0 1 0 489548553 242515968 55577 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59208 55577 603 41 0 59167 0
vsize: 236832
[startup+760.036 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 57738 0 0 0 75866 144 0 0 25 0 1 0 489548553 242515968 55596 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59208 55596 603 41 0 59167 0
vsize: 236832
[startup+770.037 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 57764 0 0 0 76867 144 0 0 25 0 1 0 489548553 242651136 55622 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59241 55622 603 41 0 59200 0
vsize: 236964
[startup+780.037 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58154 0 0 0 77866 145 0 0 25 0 1 0 489548553 244150272 56012 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59607 56012 603 41 0 59566 0
vsize: 238428
[startup+790.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58198 0 0 0 78866 145 0 0 25 0 1 0 489548553 244416512 56056 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59672 56058 603 41 0 59631 0
vsize: 238688
[startup+800.037 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58228 0 0 0 79866 145 0 0 25 0 1 0 489548553 244416512 56086 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59672 56086 603 41 0 59631 0
vsize: 238688
[startup+810.038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58251 0 0 0 80866 145 0 0 25 0 1 0 489548553 244551680 56109 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59705 56109 603 41 0 59664 0
vsize: 238820
[startup+820.038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58269 0 0 0 81866 145 0 0 25 0 1 0 489548553 244686848 56127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59738 56127 603 41 0 59697 0
vsize: 238952
[startup+830.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58284 0 0 0 82866 146 0 0 25 0 1 0 489548553 244686848 56142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59738 56142 603 41 0 59697 0
vsize: 238952
[startup+840.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58303 0 0 0 83866 146 0 0 25 0 1 0 489548553 244686848 56161 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59738 56161 603 41 0 59697 0
vsize: 238952
[startup+850.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58336 0 0 0 84866 146 0 0 25 0 1 0 489548553 244822016 56194 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59771 56194 603 41 0 59730 0
vsize: 239084
[startup+860.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58531 0 0 0 85866 147 0 0 25 0 1 0 489548553 245628928 56389 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59968 56389 603 41 0 59927 0
vsize: 239872
[startup+870.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58548 0 0 0 86866 147 0 0 25 0 1 0 489548553 245628928 56406 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59968 56406 603 41 0 59927 0
vsize: 239872
[startup+880.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 58830 0 0 0 87865 148 0 0 25 0 1 0 489548553 246845440 56688 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60265 56688 603 41 0 60224 0
vsize: 241060
[startup+890.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59075 0 0 0 88864 149 0 0 25 0 1 0 489548553 247791616 56933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60496 56933 603 41 0 60455 0
vsize: 241984
[startup+900.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59112 0 0 0 89864 149 0 0 25 0 1 0 489548553 247926784 56970 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60529 56970 603 41 0 60488 0
vsize: 242116
[startup+910.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59131 0 0 0 90865 149 0 0 25 0 1 0 489548553 248066048 56989 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60563 56989 603 41 0 60522 0
vsize: 242252
[startup+920.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59152 0 0 0 91865 149 0 0 25 0 1 0 489548553 248201216 57010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60596 57010 603 41 0 60555 0
vsize: 242384
[startup+930.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59164 0 0 0 92865 149 0 0 25 0 1 0 489548553 248201216 57022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60596 57022 603 41 0 60555 0
vsize: 242384
[startup+940.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59178 0 0 0 93866 149 0 0 25 0 1 0 489548553 248201216 57036 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60596 57036 603 41 0 60555 0
vsize: 242384
[startup+950.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59193 0 0 0 94866 149 0 0 25 0 1 0 489548553 248336384 57051 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60629 57051 603 41 0 60588 0
vsize: 242516
[startup+960.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59210 0 0 0 95866 149 0 0 25 0 1 0 489548553 248336384 57068 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60629 57068 603 41 0 60588 0
vsize: 242516
[startup+970.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59379 0 0 0 96865 150 0 0 25 0 1 0 489548553 249008128 57237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60793 57237 603 41 0 60752 0
vsize: 243172
[startup+980.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59712 0 0 0 97865 151 0 0 25 0 1 0 489548553 250363904 57570 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61124 57570 603 41 0 61083 0
vsize: 244496
[startup+990.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59851 0 0 0 98865 151 0 0 25 0 1 0 489548553 250904576 57709 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61256 57709 603 41 0 61215 0
vsize: 245024
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59928 0 0 0 99865 151 0 0 25 0 1 0 489548553 251310080 57786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61355 57786 603 41 0 61314 0
vsize: 245420
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 59973 0 0 0 100865 151 0 0 25 0 1 0 489548553 251445248 57831 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61388 57831 603 41 0 61347 0
vsize: 245552
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60006 0 0 0 101865 151 0 0 25 0 1 0 489548553 251580416 57864 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61421 57864 603 41 0 61380 0
vsize: 245684
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60022 0 0 0 102865 152 0 0 25 0 1 0 489548553 251711488 57880 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61453 57880 603 41 0 61412 0
vsize: 245812
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60058 0 0 0 103865 152 0 0 25 0 1 0 489548553 251846656 57916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61486 57916 603 41 0 61445 0
vsize: 245944
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60070 0 0 0 104865 152 0 0 25 0 1 0 489548553 251846656 57928 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61486 57928 603 41 0 61445 0
vsize: 245944
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60092 0 0 0 105865 152 0 0 25 0 1 0 489548553 251981824 57950 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61519 57950 603 41 0 61478 0
vsize: 246076
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60104 0 0 0 106866 152 0 0 25 0 1 0 489548553 251981824 57962 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61519 57962 603 41 0 61478 0
vsize: 246076
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60118 0 0 0 107866 152 0 0 25 0 1 0 489548553 251981824 57976 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61519 57976 603 41 0 61478 0
vsize: 246076
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60132 0 0 0 108866 152 0 0 25 0 1 0 489548553 252116992 57990 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61552 57990 603 41 0 61511 0
vsize: 246208
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60216 0 0 0 109865 153 0 0 25 0 1 0 489548553 252383232 58074 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61617 58074 603 41 0 61576 0
vsize: 246468
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60233 0 0 0 110865 153 0 0 25 0 1 0 489548553 252518400 58091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61650 58091 603 41 0 61609 0
vsize: 246600
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60248 0 0 0 111865 153 0 0 25 0 1 0 489548553 252518400 58106 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61650 58106 603 41 0 61609 0
vsize: 246600
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60265 0 0 0 112865 153 0 0 25 0 1 0 489548553 252653568 58123 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61683 58123 603 41 0 61642 0
vsize: 246732
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60288 0 0 0 113866 153 0 0 25 0 1 0 489548553 252653568 58146 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61683 58146 603 41 0 61642 0
vsize: 246732
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60302 0 0 0 114866 153 0 0 25 0 1 0 489548553 252788736 58160 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61716 58160 603 41 0 61675 0
vsize: 246864
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60311 0 0 0 115866 153 0 0 25 0 1 0 489548553 252788736 58169 4294967295 134512640 134672761 3221224544 3221223712 134561415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61716 58169 603 41 0 61675 0
vsize: 246864
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60324 0 0 0 116866 154 0 0 25 0 1 0 489548553 252788736 58182 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61716 58182 603 41 0 61675 0
vsize: 246864
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60335 0 0 0 117866 154 0 0 25 0 1 0 489548553 252788736 58193 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61716 58193 603 41 0 61675 0
vsize: 246864
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60364 0 0 0 118866 154 0 0 25 0 1 0 489548553 252923904 58222 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61749 58222 603 41 0 61708 0
vsize: 246996
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16446 (minisat+) R 16445 22932 22931 0 -1 0 60378 0 0 0 119867 154 0 0 25 0 1 0 489548553 252923904 58236 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61749 58236 603 41 0 61708 0
vsize: 246996
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 16503
Raw data (stat): 16446 (minisat+) Z 16445 22932 22931 0 -1 12 60380 0 0 0 119867 165 0 0 25 0 1 0 489548553 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.18
CPU time (s): 1200.33
CPU user time (s): 1198.68
CPU system time (s): 1.65575
CPU usage (%): 100.013
Max. virtual memory (Kb): 246996
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####