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/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-bg512142.opb
MD5SUM	0f3e1a19529370afcd1348994ae2c757
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	6480
Biggest coefficient in the objective function	5242880000
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	755791986840
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	5242880000
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	755791986840
Number of bits of the biggest sum of numbers	40
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1246.02
Number of variables	11280
Total number of constraints	1307
Number of constraints which are clauses	11
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1296
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 14490

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        716812 kB
Buffers:         13224 kB
Cached:         270672 kB
SwapCached:        412 kB
Active:          57832 kB
Inactive:       228376 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        716560 kB
SwapTotal:     2097892 kB
SwapFree:      2096924 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5672 kB
Slab:            26000 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 00:23:43 (client local time) WITH STATUS 0 IN 1200.37 SECONDS
stats: 19939 7 1200.37 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1171 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1224]---> Adder-cost: 155   maxlim: 393213   bits: 20/19
c ---[1223]---> Adder-cost: 98   maxlim: 65534   bits: 17/16
c ---[1222]---> Adder-cost: 157   maxlim: 786429   bits: 21/20
c ---[1221]---> Adder-cost: 154   maxlim: 524285   bits: 20/19
c ---[1220]---> Adder-cost: 112   maxlim: 1572861   bits: 22/21
c ---[1219]---> Adder-cost: 162   maxlim: 1310716   bits: 22/21
c ---[1218]---> Adder-cost: 111   maxlim: 1048573   bits: 21/20
c ---[1211]---> Adder-cost: 158   maxlim: 524285   bits: 20/19
c ---[1210]---> Adder-cost: 136   maxlim: 262141   bits: 19/18
c ---[1209]---> Adder-cost: 96   maxlim: 32766   bits: 16/15
c ---[1208]---> Adder-cost: 116   maxlim: 524286   bits: 20/19
c ---[1207]---> Adder-cost: 152   maxlim: 524285   bits: 20/19
c ---[1206]---> Adder-cost: 65   maxlim: 1048574   bits: 21/20
c ---[1205]---> Adder-cost: 106   maxlim: 786429   bits: 21/20
c ---[1200]---> Adder-cost: 151   maxlim: 524285   bits: 20/19
c ---[1199]---> Adder-cost: 140   maxlim: 131070   bits: 18/17
c ---[1198]---> Adder-cost: 157   maxlim: 262142   bits: 19/18
c ---[1197]---> Adder-cost: 166   maxlim: 131070   bits: 18/17
c ---[1188]---> Adder-cost: 167   maxlim: 786429   bits: 21/20
c ---[1182]---> Adder-cost: 135   maxlim: 65534   bits: 17/16
c ---[1181]---> Adder-cost: 131   maxlim: 65534   bits: 17/16
c ---[1180]---> Adder-cost: 162   maxlim: 1310716   bits: 22/21
c ---[1178]---> Adder-cost: 138   maxlim: 262141   bits: 19/18
c ---[1177]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1176]---> Adder-cost: 112   maxlim: 786429   bits: 21/20
c ---[1175]---> Adder-cost: 152   maxlim: 131070   bits: 18/17
c ---[1173]---> Adder-cost: 176   maxlim: 1048573   bits: 21/20
c ---[1172]---> Adder-cost: 117   maxlim: 1048573   bits: 21/20
c ---[1171]---> Adder-cost: 157   maxlim: 327677   bits: 20/19
c ---[1168]---> Adder-cost: 150   maxlim: 524285   bits: 20/19
c ---[1167]---> Adder-cost: 112   maxlim: 524286   bits: 20/19
c ---[1166]---> Adder-cost: 73   maxlim: 131070   bits: 18/17
c ---[1165]---> Adder-cost: 158   maxlim: 524285   bits: 20/19
c ---[1164]---> Adder-cost: 79   maxlim: 131070   bits: 18/17
c ---[1163]---> Adder-cost: 110   maxlim: 131070   bits: 18/17
c ---[1159]---> Adder-cost: 69   maxlim: 262142   bits: 19/18
c ---[1153]---> Adder-cost: 173   maxlim: 786429   bits: 21/20
c ---[1152]---> Adder-cost: 165   maxlim: 393213   bits: 20/19
c ---[1147]---> Adder-cost: 139   maxlim: 196605   bits: 19/18
c ---[1146]---> Adder-cost: 161   maxlim: 393213   bits: 20/19
c ---[1145]---> Adder-cost: 96   maxlim: 131070   bits: 18/17
c ---[1143]---> Adder-cost: 160   maxlim: 262141   bits: 19/18
c ---[1142]---> Adder-cost: 110   maxlim: 262142   bits: 19/18
c ---[1140]---> Adder-cost: 62   maxlim: 131070   bits: 18/17
c ---[1139]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1136]---> Adder-cost: 78   maxlim: 65534   bits: 17/16
c ---[1135]---> Adder-cost: 112   maxlim: 786429   bits: 21/20
c ---[1134]---> Adder-cost: 104   maxlim: 131070   bits: 18/17
c ---[1131]---> Adder-cost: 111   maxlim: 524287   bits: 20/19
c ---[1129]---> Adder-cost: 108   maxlim: 262143   bits: 19/18
c ---[1127]---> Adder-cost: 114   maxlim: 524287   bits: 20/19
c ---[1125]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[1123]---> Adder-cost: 117   maxlim: 1048575   bits: 21/20
c ---[1121]---> Adder-cost: 117   maxlim: 1048575   bits: 21/20
c ---[1119]---> Adder-cost: 149   maxlim: 1048574   bits: 21/20
c ---[1117]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1115]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1113]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1111]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1109]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1107]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1105]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1103]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1101]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1099]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1097]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1095]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1093]---> Adder-cost: 146   maxlim: 1179646   bits: 22/21
c ---[1091]---> Adder-cost: 146   maxlim: 1179646   bits: 22/21
c ---[1089]---> Adder-cost: 146   maxlim: 1179646   bits: 22/21
c ---[1087]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[1085]---> Adder-cost: 142   maxlim: 1114110   bits: 22/21
c ---[1083]---> Adder-cost: 142   maxlim: 1114110   bits: 22/21
c ---[1081]---> Adder-cost: 138   maxlim: 1114110   bits: 22/21
c ---[1079]---> Adder-cost: 138   maxlim: 1081342   bits: 22/21
c ---[1077]---> Adder-cost: 134   maxlim: 1064958   bits: 22/21
c ---[1075]---> Adder-cost: 126   maxlim: 1056766   bits: 22/21
c ---[1073]---> Adder-cost: 143   maxlim: 524286   bits: 20/19
c ---[1071]---> Adder-cost: 149   maxlim: 786430   bits: 21/20
c ---[1069]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1067]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1065]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1063]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1061]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1059]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1057]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1055]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1053]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1051]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1049]---> Adder-cost: 146   maxlim: 1179646   bits: 22/21
c ---[1047]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[1045]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[1043]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[1041]---> Adder-cost: 142   maxlim: 1114110   bits: 22/21
c ---[1039]---> Adder-cost: 138   maxlim: 1114110   bits: 22/21
c ---[1037]---> Adder-cost: 138   maxlim: 1114110   bits: 22/21
c ---[1035]---> Adder-cost: 138   maxlim: 1081342   bits: 22/21
c ---[1033]---> Adder-cost: 134   maxlim: 1081342   bits: 22/21
c ---[1031]---> Adder-cost: 134   maxlim: 1064958   bits: 22/21
c ---[1029]---> Adder-cost: 126   maxlim: 1056766   bits: 22/21
c ---[1027]---> Adder-cost: 151   maxlim: 1048574   bits: 21/20
c ---[1025]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[1023]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[1021]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[1019]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[1017]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[1015]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1013]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1011]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1009]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1007]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1005]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1003]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1001]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[ 999]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[ 997]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[ 995]---> Adder-cost: 146   maxlim: 1179646   bits: 22/21
c ---[ 993]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[ 991]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[ 989]---> Adder-cost: 142   maxlim: 1114110   bits: 22/21
c ---[ 987]---> Adder-cost: 138   maxlim: 1114110   bits: 22/21
c ---[ 985]---> Adder-cost: 134   maxlim: 1081342   bits: 22/21
c ---[ 983]---> Adder-cost: 130   maxlim: 1064958   bits: 22/21
c ---[ 981]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[ 979]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[ 977]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[ 975]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[ 973]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[ 971]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[ 969]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[ 967]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[ 965]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[ 963]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[ 961]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[ 959]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[ 957]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[ 955]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[ 953]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[ 951]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[ 949]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[ 947]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[ 945]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[ 943]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[ 941]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[ 939]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[ 937]---> Adder-cost: 106   maxlim: 1056766   bits: 22/21
c ---[ 935]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 933]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 931]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 929]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[ 927]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[ 925]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[ 923]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[ 921]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[ 919]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[ 917]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[ 915]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[ 913]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[ 911]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[ 909]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[ 907]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[ 905]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[ 903]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[ 901]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[ 899]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[ 897]---> Adder-cost: 142   maxlim: 1114110   bits: 22/21
c ---[ 895]---> Adder-cost: 138   maxlim: 1114110   bits: 22/21
c ---[ 893]---> Adder-cost: 134   maxlim: 1081342   bits: 22/21
c ---[ 891]---> Adder-cost: 130   maxlim: 1064958   bits: 22/21
c ---[ 889]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 887]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 885]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 883]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 881]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 879]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 877]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 875]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[ 873]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[ 871]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[ 869]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[ 867]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[ 865]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[ 863]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[ 861]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[ 859]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[ 857]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[ 855]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[ 853]---> Adder-cost: 146   maxlim: 1179646   bits: 22/21
c ---[ 851]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[ 849]---> Adder-cost: 142   maxlim: 1114110   bits: 22/21
c ---[ 847]---> Adder-cost: 138   maxlim: 1114110   bits: 22/21
c ---[ 845]---> Adder-cost: 134   maxlim: 1081342   bits: 22/21
c ---[ 843]---> Adder-cost: 36   maxlim: 257919   bits: 19/18
c ---[ 841]---> Adder-cost: 34   maxlim: 129535   bits: 18/17
c ---[ 839]---> Adder-cost: 36   maxlim: 258687   bits: 19/18
c ---[ 837]---> Adder-cost: 38   maxlim: 517503   bits: 20/19
c ---[ 835]---> Adder-cost: 72   maxlim: 520062   bits: 20/19
c ---[ 833]---> Adder-cost: 76   maxlim: 782078   bits: 21/20
c ---[ 831]---> Adder-cost: 80   maxlim: 1305598   bits: 22/21
c ---[ 829]---> Adder-cost: 80   maxlim: 1304574   bits: 22/21
c ---[ 827]---> Adder-cost: 80   maxlim: 1304190   bits: 22/21
c ---[ 825]---> Adder-cost: 80   maxlim: 1301502   bits: 22/21
c ---[ 823]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 821]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 819]---> Adder-cost: 80   maxlim: 1293694   bits: 22/21
c ---[ 817]---> Adder-cost: 80   maxlim: 1298686   bits: 22/21
c ---[ 815]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 813]---> Adder-cost: 80   maxlim: 1164414   bits: 22/21
c ---[ 811]---> Adder-cost: 80   maxlim: 1167742   bits: 22/21
c ---[ 809]---> Adder-cost: 80   maxlim: 1167486   bits: 22/21
c ---[ 807]---> Adder-cost: 80   maxlim: 1170430   bits: 22/21
c ---[ 805]---> Adder-cost: 80   maxlim: 1166206   bits: 22/21
c ---[ 803]---> Adder-cost: 80   maxlim: 1103230   bits: 22/21
c ---[ 801]---> Adder-cost: 80   maxlim: 1103358   bits: 22/21
c ---[ 799]---> Adder-cost: 80   maxlim: 1101182   bits: 22/21
c ---[ 797]---> Adder-cost: 80   maxlim: 1073406   bits: 22/21
c ---[ 795]---> Adder-cost: 80   maxlim: 1074430   bits: 22/21
c ---[ 793]---> Adder-cost: 80   maxlim: 1058430   bits: 22/21
c ---[ 791]---> Adder-cost: 80   maxlim: 1049214   bits: 22/21
c ---[ 789]---> Adder-cost: 68   maxlim: 260350   bits: 19/18
c ---[ 787]---> Adder-cost: 72   maxlim: 391166   bits: 20/19
c ---[ 785]---> Adder-cost: 76   maxlim: 652030   bits: 21/20
c ---[ 783]---> Adder-cost: 80   maxlim: 1176702   bits: 22/21
c ---[ 781]---> Adder-cost: 80   maxlim: 1176446   bits: 22/21
c ---[ 779]---> Adder-cost: 80   maxlim: 1175550   bits: 22/21
c ---[ 777]---> Adder-cost: 80   maxlim: 1174782   bits: 22/21
c ---[ 775]---> Adder-cost: 80   maxlim: 1174526   bits: 22/21
c ---[ 773]---> Adder-cost: 80   maxlim: 1110782   bits: 22/21
c ---[ 771]---> Adder-cost: 80   maxlim: 1108606   bits: 22/21
c ---[ 769]---> Adder-cost: 80   maxlim: 1107838   bits: 22/21
c ---[ 767]---> Adder-cost: 80   maxlim: 1106558   bits: 22/21
c ---[ 765]---> Adder-cost: 80   maxlim: 1109374   bits: 22/21
c ---[ 763]---> Adder-cost: 80   maxlim: 1108478   bits: 22/21
c ---[ 761]---> Adder-cost: 80   maxlim: 1076606   bits: 22/21
c ---[ 759]---> Adder-cost: 80   maxlim: 1075070   bits: 22/21
c ---[ 757]---> Adder-cost: 80   maxlim: 1077886   bits: 22/21
c ---[ 755]---> Adder-cost: 80   maxlim: 1062398   bits: 22/21
c ---[ 753]---> Adder-cost: 80   maxlim: 1061886   bits: 22/21
c ---[ 751]---> Adder-cost: 80   maxlim: 1062142   bits: 22/21
c ---[ 749]---> Adder-cost: 80   maxlim: 1054206   bits: 22/21
c ---[ 747]---> Adder-cost: 80   maxlim: 1054462   bits: 22/21
c ---[ 745]---> Adder-cost: 80   maxlim: 1048702   bits: 22/21
c ---[ 743]---> Adder-cost: 72   maxlim: 521342   bits: 20/19
c ---[ 741]---> Adder-cost: 76   maxlim: 783870   bits: 21/20
c ---[ 739]---> Adder-cost: 80   maxlim: 1305854   bits: 22/21
c ---[ 737]---> Adder-cost: 80   maxlim: 1304702   bits: 22/21
c ---[ 735]---> Adder-cost: 80   maxlim: 1306366   bits: 22/21
c ---[ 733]---> Adder-cost: 80   maxlim: 1303934   bits: 22/21
c ---[ 731]---> Adder-cost: 80   maxlim: 1172222   bits: 22/21
c ---[ 729]---> Adder-cost: 80   maxlim: 1170814   bits: 22/21
c ---[ 727]---> Adder-cost: 80   maxlim: 1170302   bits: 22/21
c ---[ 725]---> Adder-cost: 80   maxlim: 1170174   bits: 22/21
c ---[ 723]---> Adder-cost: 80   maxlim: 1169406   bits: 22/21
c ---[ 721]---> Adder-cost: 80   maxlim: 1168638   bits: 22/21
c ---[ 719]---> Adder-cost: 80   maxlim: 1168126   bits: 22/21
c ---[ 717]---> Adder-cost: 80   maxlim: 1106430   bits: 22/21
c ---[ 715]---> Adder-cost: 80   maxlim: 1106046   bits: 22/21
c ---[ 713]---> Adder-cost: 80   maxlim: 1106558   bits: 22/21
c ---[ 711]---> Adder-cost: 80   maxlim: 1107582   bits: 22/21
c ---[ 709]---> Adder-cost: 80   maxlim: 1075966   bits: 22/21
c ---[ 707]---> Adder-cost: 80   maxlim: 1074302   bits: 22/21
c ---[ 705]---> Adder-cost: 80   maxlim: 1075838   bits: 22/21
c ---[ 703]---> Adder-cost: 80   maxlim: 1059326   bits: 22/21
c ---[ 701]---> Adder-cost: 80   maxlim: 1060478   bits: 22/21
c ---[ 699]---> Adder-cost: 80   maxlim: 1048702   bits: 22/21
c ---[ 697]---> Adder-cost: 76   maxlim: 1043070   bits: 21/20
c ---[ 695]---> Adder-cost: 80   maxlim: 1563262   bits: 22/21
c ---[ 693]---> Adder-cost: 80   maxlim: 1567614   bits: 22/21
c ---[ 691]---> Adder-cost: 80   maxlim: 1565566   bits: 22/21
c ---[ 689]---> Adder-cost: 80   maxlim: 1566334   bits: 22/21
c ---[ 687]---> Adder-cost: 80   maxlim: 1559678   bits: 22/21
c ---[ 685]---> Adder-cost: 80   maxlim: 1289598   bits: 22/21
c ---[ 683]---> Adder-cost: 80   maxlim: 1288958   bits: 22/21
c ---[ 681]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[ 679]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 677]---> Adder-cost: 80   maxlim: 1288958   bits: 22/21
c ---[ 675]---> Adder-cost: 80   maxlim: 1291518   bits: 22/21
c ---[ 673]---> Adder-cost: 80   maxlim: 1288574   bits: 22/21
c ---[ 671]---> Adder-cost: 80   maxlim: 1164414   bits: 22/21
c ---[ 669]---> Adder-cost: 80   maxlim: 1164798   bits: 22/21
c ---[ 667]---> Adder-cost: 80   maxlim: 1158910   bits: 22/21
c ---[ 665]---> Adder-cost: 80   maxlim: 1165438   bits: 22/21
c ---[ 663]---> Adder-cost: 80   maxlim: 1105534   bits: 22/21
c ---[ 661]---> Adder-cost: 80   maxlim: 1102206   bits: 22/21
c ---[ 659]---> Adder-cost: 80   maxlim: 1104766   bits: 22/21
c ---[ 657]---> Adder-cost: 80   maxlim: 1071358   bits: 22/21
c ---[ 655]---> Adder-cost: 80   maxlim: 1057278   bits: 22/21
c ---[ 653]---> Adder-cost: 80   maxlim: 1049342   bits: 22/21
c ---[ 652]---> Adder-cost: 38   maxlim: 233598   bits: 19/18
c ---[ 651]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 650]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 649]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 648]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 647]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 646]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 645]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 644]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 643]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 642]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 641]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 640]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 639]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 638]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 637]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 636]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 635]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 634]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 633]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 632]---> Adder-cost: 37   maxlim: 102526   bits: 18/17
c ---[ 631]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 630]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 629]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 628]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 627]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 626]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 625]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 624]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 623]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 622]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 621]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 620]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 619]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 618]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 617]---> Adder-cost: 52   maxlim: 32766   bits: 16/15
c ---[ 616]---> Adder-cost: 38   maxlim: 216446   bits: 19/18
c ---[ 615]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 614]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 613]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 612]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 611]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 610]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 609]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 608]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 607]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 606]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 605]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 604]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 603]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 602]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 601]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 600]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 599]---> Adder-cost: 39   maxlim: 478590   bits: 20/19
c ---[ 598]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 597]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 596]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 595]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 594]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 593]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 592]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 591]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 590]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 589]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 588]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 587]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 586]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 585]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 584]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 583]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 582]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 581]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 580]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 579]---> Adder-cost: 39   maxlim: 435326   bits: 20/19
c ---[ 578]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 577]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 576]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 575]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 574]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 573]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 572]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 571]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 570]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 569]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 568]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 567]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 566]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 565]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 564]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 563]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 562]---> Adder-cost: 38   maxlim: 233598   bits: 19/18
c ---[ 561]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 560]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 559]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 558]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 557]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 556]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 555]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 554]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 553]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 552]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 551]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 550]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 549]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 548]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 547]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 546]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 545]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 544]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 543]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 542]---> Adder-cost: 52   maxlim: 32766   bits: 16/15
c ---[ 541]---> Adder-cost: 39   maxlim: 477310   bits: 20/19
c ---[ 540]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 539]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 538]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 537]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 536]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 535]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 534]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 533]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 532]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 531]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 530]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[ 529]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 528]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 527]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 526]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 525]---> Adder-cost: 61   maxlim: 262142   bits: 19/18
c ---[ 524]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 523]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 522]---> Adder-cost: 58   maxlim: 131070   bits: 18/17
c ---[ 521]---> Adder-cost: 55   maxlim: 65534   bits: 17/16
c ---[ 520]---> Adder-cost: 39   maxlim: 434686   bits: 20/19
c ---[ 519]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 518]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 517]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 516]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 515]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 514]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 513]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 512]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 511]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 510]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 509]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 508]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 507]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 506]---> Adder-cost: 54   maxlim: 131070   bits: 18/17
c ---[ 505]---> Adder-cost: 54   maxlim: 131070   bits: 18/17
c ---[ 504]---> Adder-cost: 54   maxlim: 131070   bits: 18/17
c ---[ 503]---> Adder-cost: 40   maxlim: 958974   bits: 21/20
c ---[ 502]---> Adder-cost: 29   maxlim: 1048574   bits: 21/20
c ---[ 501]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 500]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 499]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 498]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 497]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 496]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 495]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 494]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 493]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 492]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 491]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 490]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 489]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 488]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 487]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 486]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 485]---> Adder-cost: 54   maxlim: 131070   bits: 18/17
c ---[ 484]---> Adder-cost: 54   maxlim: 131070   bits: 18/17
c ---[ 483]---> Adder-cost: 40   maxlim: 958974   bits: 21/20
c ---[ 482]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 481]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 480]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 479]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 478]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 477]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 476]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 475]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[ 474]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 473]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 472]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 471]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 470]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 469]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[ 468]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 467]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 466]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 465]---> Adder-cost: 57   maxlim: 262142   bits: 19/18
c ---[ 464]---> Adder-cost: 25   maxlim: 131070   bits: 18/17
c ---[ 463]---> Adder-cost: 49   maxlim: 33022   bits: 17/16
c ---[ 462]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 461]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 460]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 459]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 458]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 457]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 456]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 455]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 454]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 453]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 452]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 451]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 450]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 449]---> Adder-cost: 10   maxlim: 131070   bits: 18/17
c ---[ 448]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 447]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 446]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 445]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 444]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 443]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 442]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 441]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 440]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 439]---> Adder-cost: 32   maxlim: 39422   bits: 17/16
c ---[ 438]---> Adder-cost: 8   maxlim: 131070   bits: 18/17
c ---[ 437]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 436]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 435]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 434]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 433]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 432]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[ 431]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 430]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 429]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 428]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 427]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 426]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 425]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 424]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 423]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 422]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 421]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 420]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 419]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 418]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 417]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 416]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 415]---> Adder-cost: 34   maxlim: 101502   bits: 18/17
c ---[ 414]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 413]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 412]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 411]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 410]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 409]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 408]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 407]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 406]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 405]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 404]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 403]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 402]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 401]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 400]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 399]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 398]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 397]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 396]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 395]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 394]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 393]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 392]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 391]---> Adder-cost: 36   maxlim: 217726   bits: 19/18
c ---[ 390]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 389]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 388]---> Adder-cost: 16   maxlim: 524286   bits: 20/19
c ---[ 387]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 386]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 385]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 384]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 383]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 382]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 381]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 380]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 379]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 378]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 377]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 376]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 375]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 374]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 373]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 372]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 371]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 370]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 369]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 368]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 367]---> Adder-cost: 36   maxlim: 203518   bits: 19/18
c ---[ 366]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 365]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 364]---> Adder-cost: 20   maxlim: 524286   bits: 20/19
c ---[ 363]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 362]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 361]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 360]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 359]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 358]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 357]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 356]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 355]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 354]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 353]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 352]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 351]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 350]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 349]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 348]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 347]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 346]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 345]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 344]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 342]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 341]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 340]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 339]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 338]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 337]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 336]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 335]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 334]---> Adder-cost: 12   maxlim: 262142   bits: 19/18
c ---[ 333]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 332]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 331]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 330]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 329]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 328]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 327]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 326]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 325]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 324]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 323]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 322]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 321]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 320]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 318]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 317]---> Adder-cost: 16   maxlim: 524286   bits: 20/19
c ---[ 316]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 315]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 314]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 313]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 312]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 311]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 310]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 309]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 308]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 307]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 306]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 305]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 304]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 303]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 302]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 301]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 300]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 299]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 298]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 297]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[ 296]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 295]---> Adder-cost: 36   maxlim: 203518   bits: 19/18
c ---[ 294]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 293]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 292]---> Adder-cost: 20   maxlim: 524286   bits: 20/19
c ---[ 291]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 290]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 289]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 288]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 287]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 286]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 285]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 284]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 283]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 282]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 281]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 280]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 279]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 278]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 277]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 276]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 275]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 274]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 273]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 272]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 271]---> Adder-cost: 38   maxlim: 475518   bits: 20/19
c ---[ 270]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 269]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 268]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 267]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 266]---> Adder-cost: 16   maxlim: 524286   bits: 20/19
c ---[ 265]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 264]---> Adder-cost: 20   maxlim: 524286   bits: 20/19
c ---[ 263]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 262]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 261]---> Adder-cost: 20   maxlim: 524286   bits: 20/19
c ---[ 260]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 259]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 258]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 257]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 256]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 255]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 254]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 253]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 252]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 251]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 250]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 249]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 248]---> Adder-cost: 8   maxlim: 16382   bits: 15/14
c ---[ 247]---> Adder-cost: 38   maxlim: 329086   bits: 20/19
c ---[ 246]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 245]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 244]---> Adder-cost: 22   maxlim: 1048574   bits: 21/20
c ---[ 243]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 242]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 241]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 240]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 239]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 238]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 237]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 236]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 235]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 234]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 233]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 232]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 231]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 230]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 229]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 228]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 227]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 226]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 225]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 224]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 223]---> Adder-cost: 112   maxlim: 629372   bits: 21/20
c ---[ 222]---> Adder-cost: 134   maxlim: 629372   bits: 21/20
c ---[ 221]---> Adder-cost: 134   maxlim: 629372   bits: 21/20
c ---[ 220]---> Adder-cost: 134   maxlim: 629372   bits: 21/20
c ---[ 219]---> Adder-cost: 134   maxlim: 629372   bits: 21/20
c ---[ 218]---> Adder-cost: 134   maxlim: 629372   bits: 21/20
c ---[ 217]---> Adder-cost: 134   maxlim: 629372   bits: 21/20
c ---[ 216]---> Adder-cost: 134   maxlim: 629372   bits: 21/20
c ---[ 215]---> Adder-cost: 134   maxlim: 629372   bits: 21/20
c ---[ 214]---> Adder-cost: 132   maxlim: 563836   bits: 21/20
c ---[ 213]---> Adder-cost: 132   maxlim: 563836   bits: 21/20
c ---[ 212]---> Adder-cost: 132   maxlim: 563836   bits: 21/20
c ---[ 211]---> Adder-cost: 151   maxlim: 432764   bits: 20/19
c ---[ 210]---> Adder-cost: 149   maxlim: 301692   bits: 20/19
c ---[ 209]---> Adder-cost: 147   maxlim: 301692   bits: 20/19
c ---[ 208]---> Adder-cost: 147   maxlim: 268924   bits: 20/19
c ---[ 207]---> Adder-cost: 147   maxlim: 268924   bits: 20/19
c ---[ 206]---> Adder-cost: 157   maxlim: 137852   bits: 19/18
c ---[ 200]---> Adder-cost: 118   maxlim: 1267580   bits: 22/21
c ---[ 199]---> Adder-cost: 154   maxlim: 1267580   bits: 22/21
c ---[ 198]---> Adder-cost: 154   maxlim: 1267580   bits: 22/21
c ---[ 197]---> Adder-cost: 154   maxlim: 1267580   bits: 22/21
c ---[ 196]---> Adder-cost: 116   maxlim: 1267580   bits: 22/21
c ---[ 195]---> Adder-cost: 154   maxlim: 1267580   bits: 22/21
c ---[ 194]---> Adder-cost: 154   maxlim: 1267580   bits: 22/21
c ---[ 193]---> Adder-cost: 146   maxlim: 874364   bits: 21/20
c ---[ 192]---> Adder-cost: 146   maxlim: 874364   bits: 21/20
c ---[ 191]---> Adder-cost: 108   maxlim: 874364   bits: 21/20
c ---[ 190]---> Adder-cost: 108   maxlim: 874364   bits: 21/20
c ---[ 189]---> Adder-cost: 146   maxlim: 874364   bits: 21/20
c ---[ 188]---> Adder-cost: 146   maxlim: 612220   bits: 21/20
c ---[ 187]---> Adder-cost: 146   maxlim: 612220   bits: 21/20
c ---[ 186]---> Adder-cost: 161   maxlim: 415612   bits: 20/19
c ---[ 185]---> Adder-cost: 161   maxlim: 415612   bits: 20/19
c ---[ 184]---> Adder-cost: 161   maxlim: 415612   bits: 20/19
c ---[ 183]---> Adder-cost: 159   maxlim: 284540   bits: 20/19
c ---[ 182]---> Adder-cost: 186   maxlim: 186236   bits: 19/18
c ---[ 181]---> Adder-cost: 186   maxlim: 186236   bits: 19/18
c ---[ 177]---> Adder-cost: 154   maxlim: 3058683   bits: 22/22
c ---[ 176]---> Adder-cost: 156   maxlim: 3058683   bits: 23/22
c ---[ 175]---> Adder-cost: 194   maxlim: 3058683   bits: 23/22
c ---[ 174]---> Adder-cost: 194   maxlim: 3058683   bits: 23/22
c ---[ 173]---> Adder-cost: 188   maxlim: 2534395   bits: 22/22
c ---[ 172]---> Adder-cost: 188   maxlim: 2534395   bits: 22/22
c ---[ 171]---> Adder-cost: 188   maxlim: 2534395   bits: 22/22
c ---[ 170]---> Adder-cost: 186   maxlim: 2010107   bits: 22/21
c ---[ 169]---> Adder-cost: 186   maxlim: 2010107   bits: 22/21
c ---[ 168]---> Adder-cost: 184   maxlim: 1485819   bits: 22/21
c ---[ 167]---> Adder-cost: 146   maxlim: 1485819   bits: 22/21
c ---[ 166]---> Adder-cost: 146   maxlim: 1485819   bits: 22/21
c ---[ 165]---> Adder-cost: 146   maxlim: 1485819   bits: 22/21
c ---[ 164]---> Adder-cost: 144   maxlim: 1223675   bits: 22/21
c ---[ 163]---> Adder-cost: 179   maxlim: 961531   bits: 21/20
c ---[ 162]---> Adder-cost: 174   maxlim: 699387   bits: 21/20
c ---[ 161]---> Adder-cost: 174   maxlim: 699387   bits: 21/20
c ---[ 160]---> Adder-cost: 174   maxlim: 699387   bits: 21/20
c ---[ 159]---> Adder-cost: 185   maxlim: 437243   bits: 20/19
c ---[ 158]---> Adder-cost: 183   maxlim: 306171   bits: 20/19
c ---[ 157]---> Adder-cost: 211   maxlim: 240635   bits: 19/18
c ---[ 154]---> Adder-cost: 14   maxlim: 9471   bits: 15/14
c ---[ 153]---> Adder-cost: 10   maxlim: 6911   bits: 14/13
c ---[ 152]---> Adder-cost: 10   maxlim: 5375   bits: 14/13
c ---[ 151]---> Adder-cost: 8   maxlim: 5631   bits: 14/13
c ---[ 150]---> Adder-cost: 24   maxlim: 19327   bits: 16/15
c ---[ 149]---> Adder-cost: 12   maxlim: 9983   bits: 15/14
c ---[ 148]---> Adder-cost: 83   maxlim: 26751   bits: 16/15
c ---[ 147]---> Adder-cost: 78   maxlim: 20223   bits: 16/15
c ---[ 146]---> Adder-cost: 80   maxlim: 18047   bits: 16/15
c ---[ 145]---> Adder-cost: 95   maxlim: 45823   bits: 17/16
c ---[ 144]---> Adder-cost: 82   maxlim: 32895   bits: 17/16
c ---[ 143]---> Adder-cost: 131   maxlim: 29951   bits: 16/15
c ---[ 142]---> Adder-cost: 106   maxlim: 27647   bits: 16/15
c ---[ 141]---> Adder-cost: 120   maxlim: 29311   bits: 16/15
c ---[ 140]---> Adder-cost: 180   maxlim: 47359   bits: 17/16
c ---[ 139]---> Adder-cost: 175   maxlim: 45183   bits: 17/16
c ---[ 138]---> Adder-cost: 187   maxlim: 86143   bits: 18/17
c ---[ 137]---> Adder-cost: 195   maxlim: 71935   bits: 18/17
c ---[ 136]---> Adder-cost: 189   maxlim: 77823   bits: 18/17
c ---[ 135]---> Adder-cost: 12   maxlim: 4223   bits: 14/13
c ---[ 134]---> Adder-cost: 14   maxlim: 12159   bits: 15/14
c ---[ 133]---> Adder-cost: 8   maxlim: 9215   bits: 15/14
c ---[ 132]---> Adder-cost: 14   maxlim: 13439   bits: 15/14
c ---[ 131]---> Adder-cost: 14   maxlim: 10879   bits: 15/14
c ---[ 130]---> Adder-cost: 10   maxlim: 10751   bits: 15/14
c ---[ 129]---> Adder-cost: 14   maxlim: 12927   bits: 15/14
c ---[ 128]---> Adder-cost: 19   maxlim: 12287   bits: 15/14
c ---[ 127]---> Adder-cost: 25   maxlim: 15231   bits: 15/14
c ---[ 126]---> Adder-cost: 12   maxlim: 6527   bits: 14/13
c ---[ 125]---> Adder-cost: 12   maxlim: 7039   bits: 14/13
c ---[ 124]---> Adder-cost: 12   maxlim: 5503   bits: 14/13
c ---[ 123]---> Adder-cost: 14   maxlim: 15231   bits: 15/14
c ---[ 122]---> Adder-cost: 10   maxlim: 14847   bits: 15/14
c ---[ 121]---> Adder-cost: 14   maxlim: 20735   bits: 16/15
c ---[ 120]---> Adder-cost: 14   maxlim: 14207   bits: 15/14
c ---[ 119]---> Adder-cost: 16   maxlim: 21247   bits: 16/15
c ---[ 118]---> Adder-cost: 57   maxlim: 20863   bits: 16/15
c ---[ 117]---> Adder-cost: 87   maxlim: 31743   bits: 16/15
c ---[ 116]---> Adder-cost: 90   maxlim: 33663   bits: 17/16
c ---[ 115]---> Adder-cost: 36   maxlim: 13311   bits: 15/14
c ---[ 114]---> Adder-cost: 24   maxlim: 10751   bits: 15/14
c ---[ 113]---> Adder-cost: 77   maxlim: 26111   bits: 16/15
c ---[ 112]---> Adder-cost: 68   maxlim: 9983   bits: 15/14
c ---[ 111]---> Adder-cost: 74   maxlim: 20735   bits: 16/15
c ---[ 110]---> Adder-cost: 91   maxlim: 33663   bits: 17/16
c ---[ 109]---> Adder-cost: 84   maxlim: 26751   bits: 16/15
c ---[ 108]---> Adder-cost: 182   maxlim: 57855   bits: 17/16
c ---[ 107]---> Adder-cost: 182   maxlim: 60287   bits: 17/16
c ---[ 106]---> Adder-cost: 188   maxlim: 57855   bits: 17/16
c ---[ 105]---> Adder-cost: 184   maxlim: 45567   bits: 17/16
c ---[ 104]---> Adder-cost: 195   maxlim: 72831   bits: 18/17
c ---[ 103]---> Adder-cost: 188   maxlim: 52607   bits: 17/16
c ---[ 102]---> Adder-cost: 186   maxlim: 50943   bits: 17/16
c ---[ 101]---> Adder-cost: 11   maxlim: 3839   bits: 13/12
c ---[ 100]---> Adder-cost: 17   maxlim: 5375   bits: 14/13
c ---[  99]---> Adder-cost: 12   maxlim: 4735   bits: 14/13
c ---[  98]---> Adder-cost: 12   maxlim: 6271   bits: 14/13
c ---[  97]---> Adder-cost: 10   maxlim: 3455   bits: 13/12
c ---[  96]---> Adder-cost: 6   maxlim: 2559   bits: 13/12
c ---[  95]---> Adder-cost: 13   maxlim: 7423   bits: 14/13
c ---[  94]---> Adder-cost: 12   maxlim: 7551   bits: 14/13
c ---[  93]---> Adder-cost: 27   maxlim: 15103   bits: 15/14
c ---[  92]---> Adder-cost: 30   maxlim: 13951   bits: 15/14
c ---[  91]---> Adder-cost: 74   maxlim: 19711   bits: 16/15
c ---[  90]---> Adder-cost: 34   maxlim: 14335   bits: 15/14
c ---[  89]---> Adder-cost: 81   maxlim: 17535   bits: 16/15
c ---[  88]---> Adder-cost: 132   maxlim: 48383   bits: 17/16
c ---[  87]---> Adder-cost: 88   maxlim: 31743   bits: 16/15
c ---[  86]---> Adder-cost: 83   maxlim: 34047   bits: 17/16
c ---[  85]---> Adder-cost: 39   maxlim: 13311   bits: 15/14
c ---[  84]---> Adder-cost: 186   maxlim: 38399   bits: 17/16
c ---[  83]---> Adder-cost: 59   maxlim: 24319   bits: 16/15
c ---[  82]---> Adder-cost: 184   maxlim: 52223   bits: 17/16
c ---[  81]---> Adder-cost: 6   maxlim: 1791   bits: 12/11
c ---[  80]---> Adder-cost: 23   maxlim: 9471   bits: 15/14
c ---[  79]---> Adder-cost: 12   maxlim: 5503   bits: 14/13
c ---[  78]---> Adder-cost: 107   maxlim: 76159   bits: 18/17
c ---[  77]---> Adder-cost: 85   maxlim: 58623   bits: 17/16
c ---[  76]---> Adder-cost: 52   maxlim: 34431   bits: 17/16
c ---[  75]---> Adder-cost: 118   maxlim: 76415   bits: 18/17
c ---[  74]---> Adder-cost: 154   maxlim: 71167   bits: 18/17
c ---[  73]---> Adder-cost: 25   maxlim: 14335   bits: 15/14
c ---[  72]---> Adder-cost: 186   maxlim: 63999   bits: 17/16
c ---[  71]---> Adder-cost: 192   maxlim: 48255   bits: 17/16
c ---[  70]---> Adder-cost: 16   maxlim: 8575   bits: 15/14
c ---[  69]---> Adder-cost: 28   maxlim: 15615   bits: 15/14
c ---[  68]---> Adder-cost: 31   maxlim: 19327   bits: 16/15
c ---[  67]---> Adder-cost: 25   maxlim: 11135   bits: 15/14
c ---[  66]---> Adder-cost: 61   maxlim: 30719   bits: 16/15
c ---[  65]---> Adder-cost: 10   maxlim: 7935   bits: 14/13
c ---[  64]---> Adder-cost: 43   maxlim: 40063   bits: 17/16
c ---[  63]---> Adder-cost: 12   maxlim: 5503   bits: 14/13
c ---[  62]---> Adder-cost: 91   maxlim: 30719   bits: 16/15
c ---[  61]---> Adder-cost: 60   maxlim: 20863   bits: 16/15
c ---[  60]---> Adder-cost: 19   maxlim: 5887   bits: 14/13
c ---[  59]---> Adder-cost: 35   maxlim: 12415   bits: 15/14
c ---[  58]---> Adder-cost: 48   maxlim: 39423   bits: 17/16
c ---[  57]---> Adder-cost: 57   maxlim: 21759   bits: 16/15
c ---[  56]---> Adder-cost: 19   maxlim: 14847   bits: 15/14
c ---[  55]---> Adder-cost: 8   maxlim: 2815   bits: 13/12
c ---[  54]---> Adder-cost: 6   maxlim: 2559   bits: 13/12
c ---[  53]---> Adder-cost: 29   maxlim: 19071   bits: 16/15
c ---[  52]---> Adder-cost: 77   maxlim: 26623   bits: 16/15
c ---[  51]---> Adder-cost: 30   maxlim: 13951   bits: 15/14
c ---[  50]---> Adder-cost: 102   maxlim: 74111   bits: 18/17
c ---[  49]---> Adder-cost: 14   maxlim: 10367   bits: 15/14
c ---[  48]---> Adder-cost: 6   maxlim: 2559   bits: 13/12
c ---[  47]---> Adder-cost: 23   maxlim: 22527   bits: 16/15
c ---[  46]---> Adder-cost: 113   maxlim: 77439   bits: 18/17
c ---[  45]---> Adder-cost: 29   maxlim: 21887   bits: 16/15
c ---[  44]---> Adder-cost: 26   maxlim: 20863   bits: 16/15
c ---[  43]---> Adder-cost: 21   maxlim: 14847   bits: 15/14
c ---[  42]---> Adder-cost: 46   maxlim: 25087   bits: 16/15
c ---[  41]---> Adder-cost: 23   maxlim: 18559   bits: 16/15
c ---[  40]---> Adder-cost: 25   maxlim: 10879   bits: 15/14
c ---[  39]---> Adder-cost: 14   maxlim: 11903   bits: 15/14
c ---[  38]---> Adder-cost: 66   maxlim: 13823   bits: 15/14
c ---[  37]---> Adder-cost: 15   maxlim: 11263   bits: 15/14
c ---[  36]---> Adder-cost: 21   maxlim: 24959   bits: 16/15
c ---[  35]---> Adder-cost: 49   maxlim: 36735   bits: 17/16
c ---[  34]---> Adder-cost: 12   maxlim: 11519   bits: 15/14
c ---[  33]---> Adder-cost: 116   maxlim: 76159   bits: 18/17
c ---[  32]---> Adder-cost: 107   maxlim: 79871   bits: 18/17
c ---[  31]---> Adder-cost: 18   maxlim: 9727   bits: 15/14
c ---[  30]---> Adder-cost: 27   maxlim: 26495   bits: 16/15
c ---[  29]---> Adder-cost: 24   maxlim: 13567   bits: 15/14
c ---[  28]---> Adder-cost: 78   maxlim: 76159   bits: 18/17
c ---[  27]---> Adder-cost: 42   maxlim: 15103   bits: 15/14
c ---[  26]---> Adder-cost: 29   maxlim: 20607   bits: 16/15
c ---[  25]---> Adder-cost: 48   maxlim: 27775   bits: 16/15
c ---[  24]---> Adder-cost: 37   maxlim: 22655   bits: 16/15
c ---[  23]---> Adder-cost: 25   maxlim: 15615   bits: 15/14
c ---[  22]---> Adder-cost: 21   maxlim: 12543   bits: 15/14
c ---[  21]---> Adder-cost: 70   maxlim: 12159   bits: 15/14
c ---[  20]---> Adder-cost: 31   maxlim: 25983   bits: 16/15
c ---[  19]---> Adder-cost: 12   maxlim: 4735   bits: 14/13
c ---[  18]---> Adder-cost: 60   maxlim: 4607   bits: 14/13
c ---[  17]---> Adder-cost: 76   maxlim: 22911   bits: 16/15
c ---[  16]---> Adder-cost: 78   maxlim: 33791   bits: 17/16
c ---[  15]---> Adder-cost: 35   maxlim: 17791   bits: 16/15
c ---[  14]---> Adder-cost: 50   maxlim: 22911   bits: 16/15
c ---[  13]---> Adder-cost: 33   maxlim: 41855   bits: 17/16
c ---[  12]---> Adder-cost: 44   maxlim: 20223   bits: 16/15
c ---[  11]---> Adder-cost: 28   maxlim: 9854   bits: 15/14
c ---[  10]---> Adder-cost: 32   maxlim: 57086   bits: 17/16
c ---[   9]---> Adder-cost: 142   maxlim: 121468   bits: 18/17
c ---[   8]---> Adder-cost: 142   maxlim: 121468   bits: 18/17
c ---[   7]---> Adder-cost: 134   maxlim: 55932   bits: 17/16
c ---[   6]---> Adder-cost: 129   maxlim: 47740   bits: 17/16
c ---[   5]---> Adder-cost: 121   maxlim: 14972   bits: 15/14
c ---[   4]---> Adder-cost: 152   maxlim: 120700   bits: 18/17
c ---[   3]---> Adder-cost: 143   maxlim: 71548   bits: 18/17
c ---[   2]---> Adder-cost: 136   maxlim: 22396   bits: 16/15
c ---[   1]---> Adder-cost: 172   maxlim: 109563   bits: 18/17
c ---[   0]---> Adder-cost: 162   maxlim: 44027   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  416095  1528316 |  138698       0        0     nan |  0.000 % |
c |       100 |  416095  1528316 |  152567     100      417     4.2 | 22.184 % |
c |       250 |  416095  1528316 |  167824     250     1199     4.8 | 22.184 % |
c |       475 |  416095  1528316 |  184607     475     2113     4.4 | 22.184 % |
c |       813 |  416054  1528183 |  203067     804     4068     5.1 | 22.191 % |
c |      1319 |  416020  1528075 |  223374    1302     6479     5.0 | 22.196 % |
c |      2078 |  415817  1527420 |  245711    2003     9843     4.9 | 22.228 % |
c |      3217 |  415664  1526925 |  270283    3105    17407     5.6 | 22.252 % |
c |      4926 |  415455  1526246 |  297311    4750    26012     5.5 | 22.284 % |
c |      7488 |  415155  1525270 |  327042    7226    42445     5.9 | 22.330 % |
c |     11332 |  414667  1523682 |  359746   10950    64587     5.9 | 22.406 % |
c |     17098 |  414175  1522093 |  395721   16580    99862     6.0 | 22.482 % |
c |     25748 |  413349  1519405 |  435293   25006   166227     6.6 | 22.610 % |
c |     38722 |  412990  1518236 |  478823   37890   450625    11.9 | 22.664 % |
c |     58183 |  411456  1513244 |  526705   56934   626177    11.0 | 22.903 % |
c |     87375 |  410187  1509091 |  579375   85745   957727    11.2 | 23.094 % |
c |    131165 |  409474  1506766 |  637313  129370  1547547    12.0 | 23.202 % |
c |    196849 |  409224  1505956 |  701044  194999  2898196    14.9 | 23.241 % |
c |    295375 |  409148  1505710 |  771149  293499  5016081    17.1 | 23.253 % |
c |    443164 |  408867  1504795 |  848264  441222  9185584    20.8 | 23.295 % |
#### 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.86 0.97 0.94 2/54 18969
Raw data (stat): 18969 (runsolver) R 18968 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540608959 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0047 s]
Raw data (loadavg): 0.88 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 11522 0 0 0 968 31 0 0 25 0 1 0 540608959 49876992 10796 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12177 10796 603 41 0 12136 0
vsize: 48708
[startup+20.0083 s]
Raw data (loadavg): 0.90 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 11666 0 0 0 1967 31 0 0 25 0 1 0 540608959 50552832 10940 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12342 10940 603 41 0 12301 0
vsize: 49368
[startup+30.009 s]
Raw data (loadavg): 0.91 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 11757 0 0 0 2967 32 0 0 25 0 1 0 540608959 50855936 11031 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12416 11031 603 41 0 12375 0
vsize: 49664
[startup+40.0088 s]
Raw data (loadavg): 0.93 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 11879 0 0 0 3966 32 0 0 25 0 1 0 540608959 51396608 11153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12548 11153 603 41 0 12507 0
vsize: 50192
[startup+50.0096 s]
Raw data (loadavg): 0.94 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 11963 0 0 0 4966 32 0 0 25 0 1 0 540608959 51761152 11237 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12637 11237 603 41 0 12596 0
vsize: 50548
[startup+60.0094 s]
Raw data (loadavg): 0.95 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12025 0 0 0 5966 33 0 0 25 0 1 0 540608959 52031488 11299 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12703 11299 603 41 0 12662 0
vsize: 50812
[startup+70.0095 s]
Raw data (loadavg): 0.95 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12128 0 0 0 6966 33 0 0 25 0 1 0 540608959 52436992 11402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12802 11402 603 41 0 12761 0
vsize: 51208
[startup+80.01 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12438 0 0 0 7965 34 0 0 25 0 1 0 540608959 53772288 11712 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13128 11712 603 41 0 13087 0
vsize: 52512
[startup+90.0097 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12589 0 0 0 8964 35 0 0 25 0 1 0 540608959 54312960 11863 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13260 11863 603 41 0 13219 0
vsize: 53040
[startup+100.01 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12695 0 0 0 9964 35 0 0 25 0 1 0 540608959 54718464 11969 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13359 11969 603 41 0 13318 0
vsize: 53436
[startup+110.009 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12794 0 0 0 10964 35 0 0 25 0 1 0 540608959 55123968 12068 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13458 12068 603 41 0 13417 0
vsize: 53832
[startup+120.009 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12833 0 0 0 11964 35 0 0 25 0 1 0 540608959 55259136 12107 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13491 12107 603 41 0 13450 0
vsize: 53964
[startup+130.009 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 18969
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12881 0 0 0 12964 36 0 0 25 0 1 0 540608959 55525376 12155 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13556 12155 603 41 0 13515 0
vsize: 54224
[startup+140.009 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12914 0 0 0 13964 36 0 0 25 0 1 0 540608959 55660544 12188 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13589 12188 603 41 0 13548 0
vsize: 54356
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 12962 0 0 0 14964 36 0 0 25 0 1 0 540608959 55795712 12236 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13622 12236 603 41 0 13581 0
vsize: 54488
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13010 0 0 0 15964 36 0 0 25 0 1 0 540608959 55930880 12284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13655 12284 603 41 0 13614 0
vsize: 54620
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13067 0 0 0 16963 37 0 0 25 0 1 0 540608959 56201216 12341 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13721 12341 603 41 0 13680 0
vsize: 54884
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13111 0 0 0 17963 37 0 0 25 0 1 0 540608959 56598528 12385 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13818 12385 603 41 0 13777 0
vsize: 55272
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13184 0 0 0 18963 37 0 0 25 0 1 0 540608959 56868864 12458 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13884 12458 603 41 0 13843 0
vsize: 55536
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13344 0 0 0 19963 38 0 0 25 0 1 0 540608959 57536512 12618 4294967295 134512640 134672761 3221224544 3221223668 134566054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14047 12618 603 41 0 14006 0
vsize: 56188
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13416 0 0 0 20963 38 0 0 25 0 1 0 540608959 57802752 12690 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14112 12690 603 41 0 14071 0
vsize: 56448
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13502 0 0 0 21963 38 0 0 25 0 1 0 540608959 58208256 12776 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14211 12776 603 41 0 14170 0
vsize: 56844
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13635 0 0 0 22962 39 0 0 25 0 1 0 540608959 58613760 12909 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14310 12909 603 41 0 14269 0
vsize: 57240
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13725 0 0 0 23962 39 0 0 25 0 1 0 540608959 59015168 12999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14408 12999 603 41 0 14367 0
vsize: 57632
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13807 0 0 0 24962 39 0 0 25 0 1 0 540608959 59285504 13081 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14474 13081 603 41 0 14433 0
vsize: 57896
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13867 0 0 0 25962 40 0 0 25 0 1 0 540608959 59555840 13141 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14540 13141 603 41 0 14499 0
vsize: 58160
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 13919 0 0 0 26962 40 0 0 25 0 1 0 540608959 59826176 13193 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14606 13193 603 41 0 14565 0
vsize: 58424
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 14012 0 0 0 27962 40 0 0 25 0 1 0 540608959 60092416 13286 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14671 13286 603 41 0 14630 0
vsize: 58684
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 14062 0 0 0 28962 41 0 0 25 0 1 0 540608959 60362752 13336 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14737 13336 603 41 0 14696 0
vsize: 58948
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 14299 0 0 0 29961 41 0 0 25 0 1 0 540608959 61304832 13573 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14967 13573 603 41 0 14926 0
vsize: 59868
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 14624 0 0 0 30960 42 0 0 25 0 1 0 540608959 62648320 13898 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15295 13898 603 41 0 15254 0
vsize: 61180
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 14736 0 0 0 31960 43 0 0 25 0 1 0 540608959 63578112 14010 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15522 14010 603 41 0 15481 0
vsize: 62088
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 14811 0 0 0 32960 43 0 0 25 0 1 0 540608959 63848448 14085 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15588 14085 603 41 0 15547 0
vsize: 62352
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 15067 0 0 0 33959 44 0 0 25 0 1 0 540608959 64790528 14341 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15818 14341 603 41 0 15777 0
vsize: 63272
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 15499 0 0 0 34959 45 0 0 25 0 1 0 540608959 66609152 14773 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16262 14773 603 41 0 16221 0
vsize: 65048
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 15581 0 0 0 35959 45 0 0 25 0 1 0 540608959 67014656 14855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16361 14855 603 41 0 16320 0
vsize: 65444
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 15744 0 0 0 36958 46 0 0 25 0 1 0 540608959 67555328 15018 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16493 15018 603 41 0 16452 0
vsize: 65972
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 15881 0 0 0 37958 47 0 0 25 0 1 0 540608959 68087808 15155 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16623 15155 603 41 0 16582 0
vsize: 66492
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 15954 0 0 0 38958 47 0 0 25 0 1 0 540608959 68489216 15228 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16721 15228 603 41 0 16680 0
vsize: 66884
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 16423 0 0 0 39957 48 0 0 25 0 1 0 540608959 70373376 15697 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17181 15697 603 41 0 17140 0
vsize: 68724
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 16726 0 0 0 40956 49 0 0 25 0 1 0 540608959 71589888 16000 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17478 16000 603 41 0 17437 0
vsize: 69912
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 16816 0 0 0 41955 49 0 0 25 0 1 0 540608959 71856128 16090 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17543 16090 603 41 0 17502 0
vsize: 70172
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 17369 0 0 0 42953 51 0 0 25 0 1 0 540608959 74145792 16643 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18102 16643 603 41 0 18061 0
vsize: 72408
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 17761 0 0 0 43952 52 0 0 25 0 1 0 540608959 75657216 17035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18471 17035 603 41 0 18430 0
vsize: 73884
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 18202 0 0 0 44951 53 0 0 25 0 1 0 540608959 77570048 17476 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18938 17476 603 41 0 18897 0
vsize: 75752
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 18489 0 0 0 45951 54 0 0 25 0 1 0 540608959 78655488 17763 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19203 17763 603 41 0 19162 0
vsize: 76812
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 18833 0 0 0 46951 55 0 0 25 0 1 0 540608959 80134144 18107 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19564 18107 603 41 0 19523 0
vsize: 78256
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 19171 0 0 0 47950 55 0 0 25 0 1 0 540608959 82534400 18445 4294967295 134512640 134672761 3221224544 3221223744 134557930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20150 18445 603 41 0 20109 0
vsize: 80600
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 19454 0 0 0 48950 56 0 0 25 0 1 0 540608959 83656704 18728 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20424 18728 603 41 0 20383 0
vsize: 81696
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 19650 0 0 0 49949 57 0 0 25 0 1 0 540608959 84520960 18924 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20635 18924 603 41 0 20594 0
vsize: 82540
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 19903 0 0 0 50948 58 0 0 25 0 1 0 540608959 85479424 19177 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20869 19177 603 41 0 20828 0
vsize: 83476
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 19991 0 0 0 51948 58 0 0 25 0 1 0 540608959 85880832 19265 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20967 19265 603 41 0 20926 0
vsize: 83868
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 20201 0 0 0 52948 58 0 0 25 0 1 0 540608959 86724608 19475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21173 19475 603 41 0 21132 0
vsize: 84692
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 20370 0 0 0 53947 59 0 0 25 0 1 0 540608959 87396352 19644 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21337 19644 603 41 0 21296 0
vsize: 85348
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 20466 0 0 0 54948 60 0 0 25 0 1 0 540608959 87805952 19740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21437 19740 603 41 0 21396 0
vsize: 85748
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 20565 0 0 0 55947 60 0 0 25 0 1 0 540608959 88207360 19839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21535 19839 603 41 0 21494 0
vsize: 86140
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 20691 0 0 0 56947 60 0 0 25 0 1 0 540608959 88743936 19965 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21666 19965 603 41 0 21625 0
vsize: 86664
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 20833 0 0 0 57947 61 0 0 25 0 1 0 540608959 89284608 20107 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21798 20107 603 41 0 21757 0
vsize: 87192
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 20987 0 0 0 58947 61 0 0 25 0 1 0 540608959 89858048 20261 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21938 20261 603 41 0 21897 0
vsize: 87752
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 21462 0 0 0 59946 63 0 0 25 0 1 0 540608959 91742208 20736 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22398 20736 603 41 0 22357 0
vsize: 89592
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 21747 0 0 0 60945 63 0 0 25 0 1 0 540608959 92954624 21021 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22694 21021 603 41 0 22653 0
vsize: 90776
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 22066 0 0 0 61944 64 0 0 25 0 1 0 540608959 94179328 21340 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22993 21340 603 41 0 22952 0
vsize: 91972
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 22147 0 0 0 62944 65 0 0 25 0 1 0 540608959 94584832 21421 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23092 21421 603 41 0 23051 0
vsize: 92368
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 22386 0 0 0 63943 65 0 0 25 0 1 0 540608959 95522816 21660 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23321 21660 603 41 0 23280 0
vsize: 93284
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 22801 0 0 0 64943 67 0 0 25 0 1 0 540608959 97136640 22075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23715 22075 603 41 0 23674 0
vsize: 94860
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 23183 0 0 0 65942 68 0 0 25 0 1 0 540608959 98746368 22457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24108 22457 603 41 0 24067 0
vsize: 96432
[startup+670.133 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 23328 0 0 0 66952 68 0 0 25 0 1 0 540608959 99287040 22602 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24240 22602 603 41 0 24199 0
vsize: 96960
[startup+680.133 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 23422 0 0 0 67952 68 0 0 25 0 1 0 540608959 99692544 22696 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 22696 603 41 0 24298 0
vsize: 97356
[startup+690.141 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 23493 0 0 0 68953 68 0 0 25 0 1 0 540608959 99966976 22767 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24406 22767 603 41 0 24365 0
vsize: 97624
[startup+700.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 23576 0 0 0 69954 69 0 0 25 0 1 0 540608959 100372480 22850 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24505 22850 603 41 0 24464 0
vsize: 98020
[startup+710.149 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 23922 0 0 0 70953 69 0 0 25 0 1 0 540608959 101724160 23196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24835 23196 603 41 0 24794 0
vsize: 99340
[startup+720.156 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 24262 0 0 0 71953 70 0 0 25 0 1 0 540608959 103075840 23536 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25165 23536 603 41 0 25124 0
vsize: 100660
[startup+730.165 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 24553 0 0 0 72953 72 0 0 25 0 1 0 540608959 104312832 23827 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25467 23827 603 41 0 25426 0
vsize: 101868
[startup+740.165 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 24894 0 0 0 73952 72 0 0 25 0 1 0 540608959 105672704 24168 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25799 24168 603 41 0 25758 0
vsize: 103196
[startup+750.165 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 25184 0 0 0 74951 74 0 0 25 0 1 0 540608959 106893312 24458 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26097 24458 603 41 0 26056 0
vsize: 104388
[startup+760.164 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 25400 0 0 0 75951 74 0 0 25 0 1 0 540608959 107696128 24674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26293 24674 603 41 0 26252 0
vsize: 105172
[startup+770.168 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 25606 0 0 0 76949 75 0 0 25 0 1 0 540608959 108580864 24880 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26509 24880 603 41 0 26468 0
vsize: 106036
[startup+780.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 25688 0 0 0 77948 75 0 0 25 0 1 0 540608959 108871680 24962 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26580 24962 603 41 0 26539 0
vsize: 106320
[startup+790.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 25789 0 0 0 78947 76 0 0 25 0 1 0 540608959 109305856 25063 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26686 25063 603 41 0 26645 0
vsize: 106744
[startup+800.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 25875 0 0 0 79947 76 0 0 25 0 1 0 540608959 109600768 25149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26758 25149 603 41 0 26717 0
vsize: 107032
[startup+810.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 25986 0 0 0 80947 77 0 0 25 0 1 0 540608959 110161920 25260 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26895 25260 603 41 0 26854 0
vsize: 107580
[startup+820.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 26086 0 0 0 81947 77 0 0 25 0 1 0 540608959 110571520 25360 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26995 25360 603 41 0 26954 0
vsize: 107980
[startup+830.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 26187 0 0 0 82947 77 0 0 25 0 1 0 540608959 110985216 25461 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27096 25461 603 41 0 27055 0
vsize: 108384
[startup+840.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 26526 0 0 0 83946 78 0 0 25 0 1 0 540608959 112336896 25800 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27426 25800 603 41 0 27385 0
vsize: 109704
[startup+850.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 26590 0 0 0 84946 78 0 0 25 0 1 0 540608959 112607232 25864 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27492 25864 603 41 0 27451 0
vsize: 109968
[startup+860.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 26659 0 0 0 85946 78 0 0 25 0 1 0 540608959 112873472 25933 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27557 25933 603 41 0 27516 0
vsize: 110228
[startup+870.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 26759 0 0 0 86946 79 0 0 25 0 1 0 540608959 113274880 26033 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27655 26033 603 41 0 27614 0
vsize: 110620
[startup+880.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 26812 0 0 0 87946 79 0 0 25 0 1 0 540608959 113545216 26086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27721 26086 603 41 0 27680 0
vsize: 110884
[startup+890.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 26897 0 0 0 88946 79 0 0 25 0 1 0 540608959 113848320 26171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27795 26171 603 41 0 27754 0
vsize: 111180
[startup+900.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 26946 0 0 0 89946 79 0 0 25 0 1 0 540608959 114118656 26220 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27861 26220 603 41 0 27820 0
vsize: 111444
[startup+910.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 27037 0 0 0 90945 80 0 0 25 0 1 0 540608959 114397184 26311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27929 26311 603 41 0 27888 0
vsize: 111716
[startup+920.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 27129 0 0 0 91945 80 0 0 25 0 1 0 540608959 114802688 26403 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28028 26403 603 41 0 27987 0
vsize: 112112
[startup+930.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 27232 0 0 0 92946 80 0 0 25 0 1 0 540608959 115208192 26506 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28127 26506 603 41 0 28086 0
vsize: 112508
[startup+940.169 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 27480 0 0 0 93945 81 0 0 25 0 1 0 540608959 116146176 26754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28356 26754 603 41 0 28315 0
vsize: 113424
[startup+950.171 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 27647 0 0 0 94944 82 0 0 25 0 1 0 540608959 116834304 26921 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28524 26921 603 41 0 28483 0
vsize: 114096
[startup+960.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 27802 0 0 0 95945 82 0 0 25 0 1 0 540608959 117510144 27076 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28689 27076 603 41 0 28648 0
vsize: 114756
[startup+970.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 27942 0 0 0 96944 82 0 0 25 0 1 0 540608959 118071296 27216 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28826 27216 603 41 0 28785 0
vsize: 115304
[startup+980.171 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 28106 0 0 0 97944 83 0 0 25 0 1 0 540608959 118792192 27380 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29002 27380 603 41 0 28961 0
vsize: 116008
[startup+990.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 28278 0 0 0 98944 83 0 0 25 0 1 0 540608959 121614336 27552 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29691 27552 603 41 0 29650 0
vsize: 118764
[startup+1000.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 28419 0 0 0 99943 84 0 0 25 0 1 0 540608959 122212352 27693 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29837 27693 603 41 0 29796 0
vsize: 119348
[startup+1010.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 28549 0 0 0 100943 84 0 0 25 0 1 0 540608959 122769408 27823 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29973 27823 603 41 0 29932 0
vsize: 119892
[startup+1020.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 28665 0 0 0 101943 85 0 0 25 0 1 0 540608959 123187200 27939 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30075 27939 603 41 0 30034 0
vsize: 120300
[startup+1030.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 28740 0 0 0 102942 85 0 0 25 0 1 0 540608959 123461632 28014 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30142 28014 603 41 0 30101 0
vsize: 120568
[startup+1040.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 28824 0 0 0 103942 85 0 0 25 0 1 0 540608959 123883520 28098 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30245 28098 603 41 0 30204 0
vsize: 120980
[startup+1050.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 28828 0 0 0 104943 85 0 0 25 0 1 0 540608959 123883520 28102 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30245 28102 603 41 0 30204 0
vsize: 120980
[startup+1060.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 28891 0 0 0 105943 85 0 0 25 0 1 0 540608959 124153856 28165 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30311 28165 603 41 0 30270 0
vsize: 121244
[startup+1070.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 29035 0 0 0 106943 86 0 0 25 0 1 0 540608959 124694528 28309 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30443 28309 603 41 0 30402 0
vsize: 121772
[startup+1080.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 29106 0 0 0 107942 86 0 0 25 0 1 0 540608959 124964864 28380 4294967295 134512640 134672761 3221224544 3221223708 134565030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30509 28380 603 41 0 30468 0
vsize: 122036
[startup+1090.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 29178 0 0 0 108942 86 0 0 25 0 1 0 540608959 125251584 28452 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30579 28452 603 41 0 30538 0
vsize: 122316
[startup+1100.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 29275 0 0 0 109942 87 0 0 25 0 1 0 540608959 125677568 28549 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30683 28549 603 41 0 30642 0
vsize: 122732
[startup+1110.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 29355 0 0 0 110942 87 0 0 25 0 1 0 540608959 125947904 28629 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30749 28629 603 41 0 30708 0
vsize: 122996
[startup+1120.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 29490 0 0 0 111942 87 0 0 25 0 1 0 540608959 126488576 28764 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30881 28764 603 41 0 30840 0
vsize: 123524
[startup+1130.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 30015 0 0 0 112940 89 0 0 25 0 1 0 540608959 128626688 29289 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31403 29289 603 41 0 31362 0
vsize: 125612
[startup+1140.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 30094 0 0 0 113940 89 0 0 25 0 1 0 540608959 129028096 29368 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31501 29368 603 41 0 31460 0
vsize: 126004
[startup+1150.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 30213 0 0 0 114940 90 0 0 25 0 1 0 540608959 129425408 29487 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31598 29487 603 41 0 31557 0
vsize: 126392
[startup+1160.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 30386 0 0 0 115939 91 0 0 25 0 1 0 540608959 130101248 29660 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31763 29660 603 41 0 31722 0
vsize: 127052
[startup+1170.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 30463 0 0 0 116939 91 0 0 25 0 1 0 540608959 130506752 29737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31862 29737 603 41 0 31821 0
vsize: 127448
[startup+1180.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 30560 0 0 0 117939 91 0 0 25 0 1 0 540608959 130777088 29834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31928 29834 603 41 0 31887 0
vsize: 127712
[startup+1190.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 30638 0 0 0 118939 91 0 0 25 0 1 0 540608959 131219456 29912 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32036 29912 603 41 0 31995 0
vsize: 128144
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 18971
Raw data (stat): 18969 (minisat+) R 18968 27222 27221 0 -1 0 30726 0 0 0 119938 92 0 0 25 0 1 0 540608959 131489792 30000 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32102 30000 603 41 0 32061 0
vsize: 128408
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 18971
Raw data (stat): 18969 (minisat+) Z 18968 27222 27221 0 -1 12 30728 0 0 0 119939 98 0 0 25 0 1 0 540608959 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.23
CPU time (s): 1200.37
CPU user time (s): 1199.39
CPU system time (s): 0.98285
CPU usage (%): 100.012
Max. virtual memory (Kb): 128408
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####