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/milp/normalized-mps-v2-13-7-neos6.opb
MD5SUM	0633214154e8bab02f648560b9bfa54f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	4460
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	233832225
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	233832225
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.18697
Number of variables	17260
Total number of constraints	9376
Number of constraints which are clauses	48
Number of constraints which are cardinality constraints (but not clauses)	9095
Number of constraints which are nor clauses,nor cardinality constraints	233
Minimum length of a constraint	1
Maximum length of a constraint	834
Trace number 14059

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        437400 kB
Buffers:         35728 kB
Cached:         538256 kB
SwapCached:          4 kB
Active:         237180 kB
Inactive:       339632 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        437148 kB
SwapTotal:     2097136 kB
SwapFree:      2097044 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14780 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:09:27 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 19731 7 1200.4 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1259 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................
c ---[1258]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1257]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1256]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1255]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1254]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1253]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1252]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1251]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1250]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1249]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1248]---> Adder-cost: 104   maxlim: 2   bits: 3/2
c ---[1247]---> Adder-cost: 209   maxlim: 2   bits: 3/2
c ---[1246]---> Adder-cost: 254   maxlim: 2   bits: 3/2
c ---[1245]---> Adder-cost: 291   maxlim: 2   bits: 3/2
c ---[1244]---> Adder-cost: 360   maxlim: 2   bits: 3/2
c ---[1243]---> Adder-cost: 401   maxlim: 2   bits: 3/2
c ---[1242]---> Adder-cost: 453   maxlim: 2   bits: 3/2
c ---[1241]---> Adder-cost: 545   maxlim: 5   bits: 4/3
c ---[1240]---> Adder-cost: 859   maxlim: 5   bits: 4/3
c ---[1239]---> Adder-cost: 927   maxlim: 5   bits: 4/3
c ---[1238]---> Adder-cost: 798   maxlim: 3   bits: 3/2
c ---[1237]---> Adder-cost: 858   maxlim: 3   bits: 3/2
c ---[1236]---> Adder-cost: 859   maxlim: 3   bits: 3/2
c ---[1235]---> Adder-cost: 942   maxlim: 3   bits: 3/2
c ---[1234]---> Adder-cost: 974   maxlim: 3   bits: 3/2
c ---[1233]---> Adder-cost: 1092   maxlim: 5   bits: 4/3
c ---[1232]---> Adder-cost: 1139   maxlim: 5   bits: 4/3
c ---[1231]---> Adder-cost: 1134   maxlim: 5   bits: 4/3
c ---[1230]---> Adder-cost: 1183   maxlim: 5   bits: 4/3
c ---[1229]---> Adder-cost: 1007   maxlim: 2   bits: 3/2
c ---[1228]---> Adder-cost: 996   maxlim: 2   bits: 3/2
c ---[1227]---> Adder-cost: 1007   maxlim: 2   bits: 3/2
c ---[1226]---> Adder-cost: 935   maxlim: 2   bits: 3/2
c ---[1225]---> Adder-cost: 867   maxlim: 2   bits: 3/2
c ---[1224]---> Adder-cost: 836   maxlim: 2   bits: 3/2
c ---[1223]---> Adder-cost: 777   maxlim: 2   bits: 3/2
c ---[1222]---> Adder-cost: 749   maxlim: 2   bits: 3/2
c ---[1221]---> Adder-cost: 693   maxlim: 2   bits: 3/2
c ---[1220]---> Adder-cost: 580   maxlim: 2   bits: 3/2
c ---[1219]---> Adder-cost: 501   maxlim: 2   bits: 3/2
c ---[1218]---> Adder-cost: 426   maxlim: 2   bits: 3/2
c ---[1217]---> Adder-cost: 375   maxlim: 2   bits: 3/2
c ---[1216]---> Adder-cost: 276   maxlim: 2   bits: 3/2
c ---[1215]---> Adder-cost: 169   maxlim: 1   bits: 2/1
c ---[1214]---> Adder-cost: 81   maxlim: 1   bits: 2/1
c ---[1213]---> Adder-cost: 104   maxlim: 2   bits: 3/2
c ---[1212]---> Adder-cost: 169   maxlim: 2   bits: 3/2
c ---[1211]---> Adder-cost: 222   maxlim: 2   bits: 3/2
c ---[1210]---> Adder-cost: 266   maxlim: 2   bits: 3/2
c ---[1209]---> Adder-cost: 352   maxlim: 2   bits: 3/2
c ---[1208]---> Adder-cost: 386   maxlim: 2   bits: 3/2
c ---[1207]---> Adder-cost: 420   maxlim: 2   bits: 3/2
c ---[1206]---> Adder-cost: 462   maxlim: 3   bits: 3/2
c ---[1205]---> Adder-cost: 789   maxlim: 3   bits: 3/2
c ---[1204]---> Adder-cost: 869   maxlim: 3   bits: 3/2
c ---[1203]---> Adder-cost: 792   maxlim: 3   bits: 3/2
c ---[1202]---> Adder-cost: 852   maxlim: 3   bits: 3/2
c ---[1201]---> Adder-cost: 889   maxlim: 3   bits: 3/2
c ---[1200]---> Adder-cost: 925   maxlim: 2   bits: 3/2
c ---[1199]---> Adder-cost: 988   maxlim: 2   bits: 3/2
c ---[1198]---> Adder-cost: 1106   maxlim: 5   bits: 4/3
c ---[1197]---> Adder-cost: 1115   maxlim: 5   bits: 4/3
c ---[1196]---> Adder-cost: 1154   maxlim: 5   bits: 4/3
c ---[1195]---> Adder-cost: 1123   maxlim: 5   bits: 4/3
c ---[1194]---> Adder-cost: 1011   maxlim: 2   bits: 3/2
c ---[1193]---> Adder-cost: 988   maxlim: 2   bits: 3/2
c ---[1192]---> Adder-cost: 962   maxlim: 2   bits: 3/2
c ---[1191]---> Adder-cost: 915   maxlim: 2   bits: 3/2
c ---[1190]---> Adder-cost: 881   maxlim: 2   bits: 3/2
c ---[1189]---> Adder-cost: 866   maxlim: 2   bits: 3/2
c ---[1188]---> Adder-cost: 788   maxlim: 2   bits: 3/2
c ---[1187]---> Adder-cost: 729   maxlim: 2   bits: 3/2
c ---[1186]---> Adder-cost: 665   maxlim: 2   bits: 3/2
c ---[1185]---> Adder-cost: 610   maxlim: 2   bits: 3/2
c ---[1184]---> Adder-cost: 497   maxlim: 2   bits: 3/2
c ---[1183]---> Adder-cost: 434   maxlim: 2   bits: 3/2
c ---[1182]---> Adder-cost: 385   maxlim: 2   bits: 3/2
c ---[1181]---> Adder-cost: 288   maxlim: 2   bits: 3/2
c ---[1180]---> Adder-cost: 173   maxlim: 1   bits: 2/1
c ---[1179]---> Adder-cost: 87   maxlim: 1   bits: 2/1
c ---[1178]---> Adder-cost: 104   maxlim: 2   bits: 3/2
c ---[1177]---> Adder-cost: 169   maxlim: 2   bits: 3/2
c ---[1176]---> Adder-cost: 222   maxlim: 2   bits: 3/2
c ---[1175]---> Adder-cost: 275   maxlim: 2   bits: 3/2
c ---[1174]---> Adder-cost: 326   maxlim: 2   bits: 3/2
c ---[1173]---> Adder-cost: 399   maxlim: 2   bits: 3/2
c ---[1172]---> Adder-cost: 401   maxlim: 2   bits: 3/2
c ---[1171]---> Adder-cost: 481   maxlim: 3   bits: 3/2
c ---[1170]---> Adder-cost: 776   maxlim: 2   bits: 3/2
c ---[1169]---> Adder-cost: 834   maxlim: 2   bits: 3/2
c ---[1168]---> Adder-cost: 774   maxlim: 2   bits: 3/2
c ---[1167]---> Adder-cost: 880   maxlim: 2   bits: 3/2
c ---[1166]---> Adder-cost: 997   maxlim: 5   bits: 4/3
c ---[1165]---> Adder-cost: 1059   maxlim: 5   bits: 4/3
c ---[1164]---> Adder-cost: 1073   maxlim: 5   bits: 4/3
c ---[1163]---> Adder-cost: 1144   maxlim: 5   bits: 4/3
c ---[1162]---> Adder-cost: 1129   maxlim: 5   bits: 4/3
c ---[1161]---> Adder-cost: 1142   maxlim: 5   bits: 4/3
c ---[1160]---> Adder-cost: 1151   maxlim: 5   bits: 4/3
c ---[1159]---> Adder-cost: 1134   maxlim: 5   bits: 4/3
c ---[1158]---> Adder-cost: 1091   maxlim: 4   bits: 4/3
c ---[1157]---> Adder-cost: 1003   maxlim: 2   bits: 3/2
c ---[1156]---> Adder-cost: 883   maxlim: 2   bits: 3/2
c ---[1155]---> Adder-cost: 914   maxlim: 2   bits: 3/2
c ---[1154]---> Adder-cost: 831   maxlim: 2   bits: 3/2
c ---[1153]---> Adder-cost: 808   maxlim: 2   bits: 3/2
c ---[1152]---> Adder-cost: 727   maxlim: 2   bits: 3/2
c ---[1151]---> Adder-cost: 701   maxlim: 2   bits: 3/2
c ---[1150]---> Adder-cost: 596   maxlim: 2   bits: 3/2
c ---[1149]---> Adder-cost: 519   maxlim: 2   bits: 3/2
c ---[1148]---> Adder-cost: 430   maxlim: 2   bits: 3/2
c ---[1147]---> Adder-cost: 379   maxlim: 2   bits: 3/2
c ---[1146]---> Adder-cost: 282   maxlim: 2   bits: 3/2
c ---[1145]---> Adder-cost: 173   maxlim: 1   bits: 2/1
c ---[1144]---> Adder-cost: 83   maxlim: 1   bits: 2/1
c ---[1143]---> Adder-cost: 104   maxlim: 2   bits: 3/2
c ---[1142]---> Adder-cost: 169   maxlim: 2   bits: 3/2
c ---[1141]---> Adder-cost: 218   maxlim: 2   bits: 3/2
c ---[1140]---> Adder-cost: 271   maxlim: 2   bits: 3/2
c ---[1139]---> Adder-cost: 339   maxlim: 2   bits: 3/2
c ---[1138]---> Adder-cost: 401   maxlim: 2   bits: 3/2
c ---[1137]---> Adder-cost: 430   maxlim: 2   bits: 3/2
c ---[1136]---> Adder-cost: 467   maxlim: 3   bits: 3/2
c ---[1135]---> Adder-cost: 795   maxlim: 3   bits: 3/2
c ---[1134]---> Adder-cost: 759   maxlim: 3   bits: 3/2
c ---[1133]---> Adder-cost: 854   maxlim: 3   bits: 3/2
c ---[1132]---> Adder-cost: 861   maxlim: 3   bits: 3/2
c ---[1131]---> Adder-cost: 885   maxlim: 3   bits: 3/2
c ---[1130]---> Adder-cost: 925   maxlim: 2   bits: 3/2
c ---[1129]---> Adder-cost: 972   maxlim: 2   bits: 3/2
c ---[1128]---> Adder-cost: 1103   maxlim: 2   bits: 3/2
c ---[1127]---> Adder-cost: 970   maxlim: 2   bits: 3/2
c ---[1126]---> Adder-cost: 1084   maxlim: 2   bits: 3/2
c ---[1125]---> Adder-cost: 1045   maxlim: 2   bits: 3/2
c ---[1124]---> Adder-cost: 1007   maxlim: 2   bits: 3/2
c ---[1123]---> Adder-cost: 1010   maxlim: 2   bits: 3/2
c ---[1122]---> Adder-cost: 1015   maxlim: 2   bits: 3/2
c ---[1121]---> Adder-cost: 921   maxlim: 2   bits: 3/2
c ---[1120]---> Adder-cost: 900   maxlim: 2   bits: 3/2
c ---[1119]---> Adder-cost: 852   maxlim: 2   bits: 3/2
c ---[1118]---> Adder-cost: 824   maxlim: 2   bits: 3/2
c ---[1117]---> Adder-cost: 747   maxlim: 2   bits: 3/2
c ---[1116]---> Adder-cost: 655   maxlim: 2   bits: 3/2
c ---[1115]---> Adder-cost: 610   maxlim: 2   bits: 3/2
c ---[1114]---> Adder-cost: 507   maxlim: 2   bits: 3/2
c ---[1113]---> Adder-cost: 434   maxlim: 2   bits: 3/2
c ---[1112]---> Adder-cost: 371   maxlim: 2   bits: 3/2
c ---[1111]---> Adder-cost: 284   maxlim: 2   bits: 3/2
c ---[1110]---> Adder-cost: 165   maxlim: 1   bits: 2/1
c ---[1109]---> Adder-cost: 81   maxlim: 1   bits: 2/1
c ---[1108]---> Adder-cost: 104   maxlim: 2   bits: 3/2
c ---[1107]---> Adder-cost: 169   maxlim: 2   bits: 3/2
c ---[1106]---> Adder-cost: 226   maxlim: 2   bits: 3/2
c ---[1105]---> Adder-cost: 266   maxlim: 2   bits: 3/2
c ---[1104]---> Adder-cost: 356   maxlim: 2   bits: 3/2
c ---[1103]---> Adder-cost: 392   maxlim: 2   bits: 3/2
c ---[1102]---> Adder-cost: 439   maxlim: 2   bits: 3/2
c ---[1101]---> Adder-cost: 452   maxlim: 3   bits: 3/2
c ---[1100]---> Adder-cost: 791   maxlim: 3   bits: 3/2
c ---[1099]---> Adder-cost: 833   maxlim: 3   bits: 3/2
c ---[1098]---> Adder-cost: 786   maxlim: 3   bits: 3/2
c ---[1097]---> Adder-cost: 854   maxlim: 3   bits: 3/2
c ---[1096]---> Adder-cost: 915   maxlim: 3   bits: 3/2
c ---[1095]---> Adder-cost: 925   maxlim: 2   bits: 3/2
c ---[1094]---> Adder-cost: 1022   maxlim: 2   bits: 3/2
c ---[1093]---> Adder-cost: 1070   maxlim: 5   bits: 4/3
c ---[1092]---> Adder-cost: 1121   maxlim: 5   bits: 4/3
c ---[1091]---> Adder-cost: 1140   maxlim: 5   bits: 4/3
c ---[1090]---> Adder-cost: 1109   maxlim: 5   bits: 4/3
c ---[1089]---> Adder-cost: 999   maxlim: 2   bits: 3/2
c ---[1088]---> Adder-cost: 1014   maxlim: 2   bits: 3/2
c ---[1087]---> Adder-cost: 1027   maxlim: 2   bits: 3/2
c ---[1086]---> Adder-cost: 911   maxlim: 2   bits: 3/2
c ---[1085]---> Adder-cost: 906   maxlim: 2   bits: 3/2
c ---[1084]---> Adder-cost: 854   maxlim: 2   bits: 3/2
c ---[1083]---> Adder-cost: 766   maxlim: 2   bits: 3/2
c ---[1082]---> Adder-cost: 763   maxlim: 2   bits: 3/2
c ---[1081]---> Adder-cost: 681   maxlim: 2   bits: 3/2
c ---[1080]---> Adder-cost: 588   maxlim: 2   bits: 3/2
c ---[1079]---> Adder-cost: 499   maxlim: 2   bits: 3/2
c ---[1078]---> Adder-cost: 442   maxlim: 2   bits: 3/2
c ---[1077]---> Adder-cost: 377   maxlim: 2   bits: 3/2
c ---[1076]---> Adder-cost: 290   maxlim: 2   bits: 3/2
c ---[1075]---> Adder-cost: 169   maxlim: 1   bits: 2/1
c ---[1074]---> Adder-cost: 87   maxlim: 1   bits: 2/1
c ---[1024]---> Adder-cost: 156   maxlim: 1055615   bits: 22/21
c ---[1022]---> Adder-cost: 268   maxlim: 1063295   bits: 22/21
c ---[1020]---> Adder-cost: 334   maxlim: 1070975   bits: 22/21
c ---[1018]---> Adder-cost: 398   maxlim: 1078655   bits: 22/21
c ---[1016]---> Adder-cost: 448   maxlim: 1086335   bits: 22/21
c ---[1014]---> Adder-cost: 506   maxlim: 1093887   bits: 22/21
c ---[1012]---> Adder-cost: 544   maxlim: 1101567   bits: 22/21
c ---[1010]---> Adder-cost: 594   maxlim: 1109247   bits: 22/21
c ---[1008]---> Adder-cost: 702   maxlim: 1115647   bits: 22/21
c ---[1006]---> Adder-cost: 764   maxlim: 1122047   bits: 22/21
c ---[1004]---> Adder-cost: 804   maxlim: 1127423   bits: 22/21
c ---[1002]---> Adder-cost: 890   maxlim: 1132543   bits: 22/21
c ---[1000]---> Adder-cost: 936   maxlim: 1136383   bits: 22/21
c ---[ 998]---> Adder-cost: 994   maxlim: 1140223   bits: 22/21
c ---[ 996]---> Adder-cost: 1028   maxlim: 1142783   bits: 22/21
c ---[ 994]---> Adder-cost: 1066   maxlim: 1145087   bits: 22/21
c ---[ 992]---> Adder-cost: 1086   maxlim: 1146367   bits: 22/21
c ---[ 990]---> Adder-cost: 1102   maxlim: 1147647   bits: 22/21
c ---[ 988]---> Adder-cost: 1120   maxlim: 1146367   bits: 22/21
c ---[ 986]---> Adder-cost: 1014   maxlim: 1145471   bits: 22/21
c ---[ 984]---> Adder-cost: 1050   maxlim: 1142911   bits: 22/21
c ---[ 982]---> Adder-cost: 1042   maxlim: 1140351   bits: 22/21
c ---[ 980]---> Adder-cost: 988   maxlim: 1136511   bits: 22/21
c ---[ 978]---> Adder-cost: 998   maxlim: 1132415   bits: 22/21
c ---[ 976]---> Adder-cost: 946   maxlim: 1127295   bits: 22/21
c ---[ 974]---> Adder-cost: 874   maxlim: 1122175   bits: 22/21
c ---[ 972]---> Adder-cost: 836   maxlim: 1116031   bits: 22/21
c ---[ 970]---> Adder-cost: 754   maxlim: 1109631   bits: 22/21
c ---[ 968]---> Adder-cost: 674   maxlim: 1101951   bits: 22/21
c ---[ 966]---> Adder-cost: 568   maxlim: 1094271   bits: 22/21
c ---[ 964]---> Adder-cost: 516   maxlim: 1086591   bits: 22/21
c ---[ 962]---> Adder-cost: 450   maxlim: 1078527   bits: 22/21
c ---[ 960]---> Adder-cost: 358   maxlim: 1070847   bits: 22/21
c ---[ 958]---> Adder-cost: 276   maxlim: 1063679   bits: 22/21
c ---[ 956]---> Adder-cost: 166   maxlim: 1055999   bits: 22/21
c ---[ 954]---> Adder-cost: 156   maxlim: 1055615   bits: 22/21
c ---[ 952]---> Adder-cost: 258   maxlim: 1063295   bits: 22/21
c ---[ 950]---> Adder-cost: 330   maxlim: 1070975   bits: 22/21
c ---[ 948]---> Adder-cost: 400   maxlim: 1078655   bits: 22/21
c ---[ 946]---> Adder-cost: 452   maxlim: 1086335   bits: 22/21
c ---[ 944]---> Adder-cost: 498   maxlim: 1094143   bits: 22/21
c ---[ 942]---> Adder-cost: 542   maxlim: 1101823   bits: 22/21
c ---[ 940]---> Adder-cost: 590   maxlim: 1109503   bits: 22/21
c ---[ 938]---> Adder-cost: 694   maxlim: 1115903   bits: 22/21
c ---[ 936]---> Adder-cost: 758   maxlim: 1122303   bits: 22/21
c ---[ 934]---> Adder-cost: 826   maxlim: 1127423   bits: 22/21
c ---[ 932]---> Adder-cost: 892   maxlim: 1132543   bits: 22/21
c ---[ 930]---> Adder-cost: 960   maxlim: 1136383   bits: 22/21
c ---[ 928]---> Adder-cost: 990   maxlim: 1140351   bits: 22/21
c ---[ 926]---> Adder-cost: 1044   maxlim: 1142911   bits: 22/21
c ---[ 924]---> Adder-cost: 1018   maxlim: 1145087   bits: 22/21
c ---[ 922]---> Adder-cost: 1106   maxlim: 1146367   bits: 22/21
c ---[ 920]---> Adder-cost: 1122   maxlim: 1147647   bits: 22/21
c ---[ 918]---> Adder-cost: 1074   maxlim: 1146367   bits: 22/21
c ---[ 916]---> Adder-cost: 1064   maxlim: 1145471   bits: 22/21
c ---[ 914]---> Adder-cost: 1062   maxlim: 1142911   bits: 22/21
c ---[ 912]---> Adder-cost: 1064   maxlim: 1140351   bits: 22/21
c ---[ 910]---> Adder-cost: 1006   maxlim: 1136511   bits: 22/21
c ---[ 908]---> Adder-cost: 990   maxlim: 1132415   bits: 22/21
c ---[ 906]---> Adder-cost: 950   maxlim: 1127295   bits: 22/21
c ---[ 904]---> Adder-cost: 880   maxlim: 1122175   bits: 22/21
c ---[ 902]---> Adder-cost: 846   maxlim: 1116031   bits: 22/21
c ---[ 900]---> Adder-cost: 746   maxlim: 1109631   bits: 22/21
c ---[ 898]---> Adder-cost: 658   maxlim: 1101951   bits: 22/21
c ---[ 896]---> Adder-cost: 570   maxlim: 1094271   bits: 22/21
c ---[ 894]---> Adder-cost: 528   maxlim: 1086591   bits: 22/21
c ---[ 892]---> Adder-cost: 460   maxlim: 1078527   bits: 22/21
c ---[ 890]---> Adder-cost: 352   maxlim: 1070847   bits: 22/21
c ---[ 888]---> Adder-cost: 276   maxlim: 1063679   bits: 22/21
c ---[ 886]---> Adder-cost: 172   maxlim: 1055999   bits: 22/21
c ---[ 884]---> Adder-cost: 162   maxlim: 1055615   bits: 22/21
c ---[ 882]---> Adder-cost: 258   maxlim: 1063295   bits: 22/21
c ---[ 880]---> Adder-cost: 326   maxlim: 1070975   bits: 22/21
c ---[ 878]---> Adder-cost: 404   maxlim: 1078655   bits: 22/21
c ---[ 876]---> Adder-cost: 452   maxlim: 1086335   bits: 22/21
c ---[ 874]---> Adder-cost: 516   maxlim: 1094015   bits: 22/21
c ---[ 872]---> Adder-cost: 518   maxlim: 1101823   bits: 22/21
c ---[ 870]---> Adder-cost: 622   maxlim: 1109503   bits: 22/21
c ---[ 868]---> Adder-cost: 682   maxlim: 1116031   bits: 22/21
c ---[ 866]---> Adder-cost: 768   maxlim: 1122431   bits: 22/21
c ---[ 864]---> Adder-cost: 808   maxlim: 1127551   bits: 22/21
c ---[ 862]---> Adder-cost: 878   maxlim: 1132671   bits: 22/21
c ---[ 860]---> Adder-cost: 934   maxlim: 1136127   bits: 22/21
c ---[ 858]---> Adder-cost: 988   maxlim: 1139967   bits: 22/21
c ---[ 856]---> Adder-cost: 1026   maxlim: 1142527   bits: 22/21
c ---[ 854]---> Adder-cost: 1040   maxlim: 1145087   bits: 22/21
c ---[ 852]---> Adder-cost: 1086   maxlim: 1146367   bits: 22/21
c ---[ 850]---> Adder-cost: 1094   maxlim: 1147647   bits: 22/21
c ---[ 848]---> Adder-cost: 1102   maxlim: 1146367   bits: 22/21
c ---[ 846]---> Adder-cost: 1068   maxlim: 1145087   bits: 22/21
c ---[ 844]---> Adder-cost: 1042   maxlim: 1142655   bits: 22/21
c ---[ 842]---> Adder-cost: 1038   maxlim: 1140095   bits: 22/21
c ---[ 840]---> Adder-cost: 1008   maxlim: 1136255   bits: 22/21
c ---[ 838]---> Adder-cost: 1004   maxlim: 1132415   bits: 22/21
c ---[ 836]---> Adder-cost: 958   maxlim: 1127295   bits: 22/21
c ---[ 834]---> Adder-cost: 860   maxlim: 1122175   bits: 22/21
c ---[ 832]---> Adder-cost: 834   maxlim: 1116031   bits: 22/21
c ---[ 830]---> Adder-cost: 774   maxlim: 1109631   bits: 22/21
c ---[ 828]---> Adder-cost: 652   maxlim: 1101951   bits: 22/21
c ---[ 826]---> Adder-cost: 598   maxlim: 1094271   bits: 22/21
c ---[ 824]---> Adder-cost: 524   maxlim: 1086591   bits: 22/21
c ---[ 822]---> Adder-cost: 454   maxlim: 1078527   bits: 22/21
c ---[ 820]---> Adder-cost: 350   maxlim: 1070847   bits: 22/21
c ---[ 818]---> Adder-cost: 270   maxlim: 1063679   bits: 22/21
c ---[ 816]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 814]---> Adder-cost: 156   maxlim: 1055615   bits: 22/21
c ---[ 812]---> Adder-cost: 260   maxlim: 1063295   bits: 22/21
c ---[ 810]---> Adder-cost: 334   maxlim: 1070975   bits: 22/21
c ---[ 808]---> Adder-cost: 398   maxlim: 1078655   bits: 22/21
c ---[ 806]---> Adder-cost: 444   maxlim: 1086335   bits: 22/21
c ---[ 804]---> Adder-cost: 508   maxlim: 1094143   bits: 22/21
c ---[ 802]---> Adder-cost: 550   maxlim: 1101823   bits: 22/21
c ---[ 800]---> Adder-cost: 584   maxlim: 1109503   bits: 22/21
c ---[ 798]---> Adder-cost: 736   maxlim: 1115903   bits: 22/21
c ---[ 796]---> Adder-cost: 768   maxlim: 1122303   bits: 22/21
c ---[ 794]---> Adder-cost: 812   maxlim: 1127423   bits: 22/21
c ---[ 792]---> Adder-cost: 870   maxlim: 1132543   bits: 22/21
c ---[ 790]---> Adder-cost: 954   maxlim: 1136383   bits: 22/21
c ---[ 788]---> Adder-cost: 960   maxlim: 1140351   bits: 22/21
c ---[ 786]---> Adder-cost: 1014   maxlim: 1142911   bits: 22/21
c ---[ 784]---> Adder-cost: 1084   maxlim: 1145471   bits: 22/21
c ---[ 782]---> Adder-cost: 1086   maxlim: 1146751   bits: 22/21
c ---[ 780]---> Adder-cost: 1108   maxlim: 1148031   bits: 22/21
c ---[ 778]---> Adder-cost: 1082   maxlim: 1146751   bits: 22/21
c ---[ 776]---> Adder-cost: 1070   maxlim: 1145471   bits: 22/21
c ---[ 774]---> Adder-cost: 1044   maxlim: 1142911   bits: 22/21
c ---[ 772]---> Adder-cost: 1064   maxlim: 1140351   bits: 22/21
c ---[ 770]---> Adder-cost: 988   maxlim: 1136511   bits: 22/21
c ---[ 768]---> Adder-cost: 982   maxlim: 1132415   bits: 22/21
c ---[ 766]---> Adder-cost: 924   maxlim: 1127295   bits: 22/21
c ---[ 764]---> Adder-cost: 886   maxlim: 1122175   bits: 22/21
c ---[ 762]---> Adder-cost: 826   maxlim: 1116031   bits: 22/21
c ---[ 760]---> Adder-cost: 758   maxlim: 1109631   bits: 22/21
c ---[ 758]---> Adder-cost: 692   maxlim: 1101951   bits: 22/21
c ---[ 756]---> Adder-cost: 562   maxlim: 1094271   bits: 22/21
c ---[ 754]---> Adder-cost: 496   maxlim: 1086591   bits: 22/21
c ---[ 752]---> Adder-cost: 456   maxlim: 1078527   bits: 22/21
c ---[ 750]---> Adder-cost: 360   maxlim: 1070847   bits: 22/21
c ---[ 748]---> Adder-cost: 276   maxlim: 1063679   bits: 22/21
c ---[ 746]---> Adder-cost: 164   maxlim: 1055999   bits: 22/21
c ---[ 744]---> Adder-cost: 156   maxlim: 1055615   bits: 22/21
c ---[ 742]---> Adder-cost: 256   maxlim: 1063295   bits: 22/21
c ---[ 740]---> Adder-cost: 336   maxlim: 1070975   bits: 22/21
c ---[ 738]---> Adder-cost: 394   maxlim: 1078655   bits: 22/21
c ---[ 736]---> Adder-cost: 456   maxlim: 1086335   bits: 22/21
c ---[ 734]---> Adder-cost: 504   maxlim: 1094015   bits: 22/21
c ---[ 732]---> Adder-cost: 550   maxlim: 1101695   bits: 22/21
c ---[ 730]---> Adder-cost: 592   maxlim: 1109503   bits: 22/21
c ---[ 728]---> Adder-cost: 686   maxlim: 1115903   bits: 22/21
c ---[ 726]---> Adder-cost: 756   maxlim: 1122303   bits: 22/21
c ---[ 724]---> Adder-cost: 796   maxlim: 1127423   bits: 22/21
c ---[ 722]---> Adder-cost: 906   maxlim: 1132543   bits: 22/21
c ---[ 720]---> Adder-cost: 978   maxlim: 1136383   bits: 22/21
c ---[ 718]---> Adder-cost: 966   maxlim: 1140351   bits: 22/21
c ---[ 716]---> Adder-cost: 1046   maxlim: 1142911   bits: 22/21
c ---[ 714]---> Adder-cost: 1022   maxlim: 1145087   bits: 22/21
c ---[ 712]---> Adder-cost: 1136   maxlim: 1146367   bits: 22/21
c ---[ 710]---> Adder-cost: 1144   maxlim: 1147647   bits: 22/21
c ---[ 708]---> Adder-cost: 1132   maxlim: 1146367   bits: 22/21
c ---[ 706]---> Adder-cost: 1056   maxlim: 1145471   bits: 22/21
c ---[ 704]---> Adder-cost: 1026   maxlim: 1142911   bits: 22/21
c ---[ 702]---> Adder-cost: 1070   maxlim: 1140351   bits: 22/21
c ---[ 700]---> Adder-cost: 980   maxlim: 1136511   bits: 22/21
c ---[ 698]---> Adder-cost: 988   maxlim: 1132415   bits: 22/21
c ---[ 696]---> Adder-cost: 968   maxlim: 1127295   bits: 22/21
c ---[ 694]---> Adder-cost: 872   maxlim: 1122175   bits: 22/21
c ---[ 692]---> Adder-cost: 826   maxlim: 1116031   bits: 22/21
c ---[ 690]---> Adder-cost: 752   maxlim: 1109631   bits: 22/21
c ---[ 688]---> Adder-cost: 696   maxlim: 1101951   bits: 22/21
c ---[ 686]---> Adder-cost: 582   maxlim: 1094271   bits: 22/21
c ---[ 684]---> Adder-cost: 512   maxlim: 1086591   bits: 22/21
c ---[ 682]---> Adder-cost: 456   maxlim: 1078527   bits: 22/21
c ---[ 680]---> Adder-cost: 346   maxlim: 1070847   bits: 22/21
c ---[ 678]---> Adder-cost: 278   maxlim: 1063679   bits: 22/21
c ---[ 676]---> Adder-cost: 172   maxlim: 1055999   bits: 22/21
c ---[ 674]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 672]---> Adder-cost: 272   maxlim: 1063679   bits: 22/21
c ---[ 670]---> Adder-cost: 416   maxlim: 1071359   bits: 22/21
c ---[ 668]---> Adder-cost: 404   maxlim: 1079039   bits: 22/21
c ---[ 666]---> Adder-cost: 456   maxlim: 1086719   bits: 22/21
c ---[ 664]---> Adder-cost: 542   maxlim: 1094399   bits: 22/21
c ---[ 662]---> Adder-cost: 598   maxlim: 1102079   bits: 22/21
c ---[ 660]---> Adder-cost: 826   maxlim: 1108479   bits: 22/21
c ---[ 658]---> Adder-cost: 794   maxlim: 1113599   bits: 22/21
c ---[ 656]---> Adder-cost: 916   maxlim: 1117439   bits: 22/21
c ---[ 654]---> Adder-cost: 914   maxlim: 1119999   bits: 22/21
c ---[ 652]---> Adder-cost: 968   maxlim: 1121279   bits: 22/21
c ---[ 650]---> Adder-cost: 944   maxlim: 1121279   bits: 22/21
c ---[ 648]---> Adder-cost: 884   maxlim: 1119999   bits: 22/21
c ---[ 646]---> Adder-cost: 878   maxlim: 1117439   bits: 22/21
c ---[ 644]---> Adder-cost: 876   maxlim: 1113599   bits: 22/21
c ---[ 642]---> Adder-cost: 834   maxlim: 1108479   bits: 22/21
c ---[ 640]---> Adder-cost: 752   maxlim: 1102079   bits: 22/21
c ---[ 638]---> Adder-cost: 656   maxlim: 1094399   bits: 22/21
c ---[ 636]---> Adder-cost: 574   maxlim: 1086719   bits: 22/21
c ---[ 634]---> Adder-cost: 496   maxlim: 1079039   bits: 22/21
c ---[ 632]---> Adder-cost: 394   maxlim: 1071359   bits: 22/21
c ---[ 630]---> Adder-cost: 286   maxlim: 1063679   bits: 22/21
c ---[ 628]---> Adder-cost: 168   maxlim: 1055999   bits: 22/21
c ---[ 626]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 624]---> Adder-cost: 272   maxlim: 1063679   bits: 22/21
c ---[ 622]---> Adder-cost: 348   maxlim: 1071359   bits: 22/21
c ---[ 620]---> Adder-cost: 424   maxlim: 1079039   bits: 22/21
c ---[ 618]---> Adder-cost: 490   maxlim: 1086719   bits: 22/21
c ---[ 616]---> Adder-cost: 544   maxlim: 1094399   bits: 22/21
c ---[ 614]---> Adder-cost: 620   maxlim: 1102079   bits: 22/21
c ---[ 612]---> Adder-cost: 930   maxlim: 1108479   bits: 22/21
c ---[ 610]---> Adder-cost: 908   maxlim: 1113599   bits: 22/21
c ---[ 608]---> Adder-cost: 924   maxlim: 1117439   bits: 22/21
c ---[ 606]---> Adder-cost: 894   maxlim: 1119999   bits: 22/21
c ---[ 604]---> Adder-cost: 944   maxlim: 1121279   bits: 22/21
c ---[ 602]---> Adder-cost: 952   maxlim: 1121151   bits: 22/21
c ---[ 600]---> Adder-cost: 886   maxlim: 1119871   bits: 22/21
c ---[ 598]---> Adder-cost: 894   maxlim: 1117311   bits: 22/21
c ---[ 596]---> Adder-cost: 860   maxlim: 1113471   bits: 22/21
c ---[ 594]---> Adder-cost: 812   maxlim: 1108351   bits: 22/21
c ---[ 592]---> Adder-cost: 766   maxlim: 1101951   bits: 22/21
c ---[ 590]---> Adder-cost: 658   maxlim: 1094271   bits: 22/21
c ---[ 588]---> Adder-cost: 580   maxlim: 1086591   bits: 22/21
c ---[ 586]---> Adder-cost: 488   maxlim: 1078911   bits: 22/21
c ---[ 584]---> Adder-cost: 368   maxlim: 1071231   bits: 22/21
c ---[ 582]---> Adder-cost: 282   maxlim: 1063551   bits: 22/21
c ---[ 580]---> Adder-cost: 170   maxlim: 1055871   bits: 22/21
c ---[ 579]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 578]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 577]---> Adder-cost: 32   maxlim: 22   bits: 5/5
c ---[ 576]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 575]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 574]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[ 573]---> Adder-cost: 68   maxlim: 46   bits: 6/6
c ---[ 572]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 571]---> Adder-cost: 88   maxlim: 58   bits: 6/6
c ---[ 570]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 569]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 568]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 567]---> Adder-cost: 28   maxlim: 28   bits: 5/5
c ---[ 566]---> Adder-cost: 56   maxlim: 34   bits: 6/6
c ---[ 565]---> Adder-cost: 60   maxlim: 40   bits: 6/6
c ---[ 564]---> Adder-cost: 68   maxlim: 46   bits: 6/6
c ---[ 563]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 562]---> Adder-cost: 72   maxlim: 58   bits: 6/6
c ---[ 561]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 560]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 559]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 558]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[ 557]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 556]---> Adder-cost: 66   maxlim: 40   bits: 6/6
c ---[ 555]---> Adder-cost: 72   maxlim: 46   bits: 6/6
c ---[ 554]---> Adder-cost: 76   maxlim: 52   bits: 6/6
c ---[ 553]---> Adder-cost: 76   maxlim: 58   bits: 6/6
c ---[ 552]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 551]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 550]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 549]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 548]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 547]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 546]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 545]---> Adder-cost: 40   maxlim: 22   bits: 5/5
c ---[ 544]---> Adder-cost: 30   maxlim: 28   bits: 5/5
c ---[ 543]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 542]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 541]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 540]---> Adder-cost: 44   maxlim: 28   bits: 5/5
c ---[ 539]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 538]---> Adder-cost: 60   maxlim: 40   bits: 6/6
c ---[ 537]---> Adder-cost: 74   maxlim: 46   bits: 6/6
c ---[ 536]---> Adder-cost: 72   maxlim: 52   bits: 6/6
c ---[ 535]---> Adder-cost: 82   maxlim: 58   bits: 6/6
c ---[ 534]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 533]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 532]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 531]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 530]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 529]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 528]---> Adder-cost: 38   maxlim: 28   bits: 5/5
c ---[ 527]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 526]---> Adder-cost: 64   maxlim: 40   bits: 6/6
c ---[ 525]---> Adder-cost: 62   maxlim: 46   bits: 6/6
c ---[ 524]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 523]---> Adder-cost: 80   maxlim: 58   bits: 6/6
c ---[ 522]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 521]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 520]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 519]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[ 518]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 517]---> Adder-cost: 48   maxlim: 40   bits: 6/6
c ---[ 516]---> Adder-cost: 56   maxlim: 46   bits: 6/6
c ---[ 515]---> Adder-cost: 60   maxlim: 52   bits: 6/6
c ---[ 514]---> Adder-cost: 60   maxlim: 58   bits: 6/6
c ---[ 513]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 512]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 511]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 510]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[ 509]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 508]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[ 507]---> Adder-cost: 64   maxlim: 46   bits: 6/6
c ---[ 506]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 505]---> Adder-cost: 82   maxlim: 58   bits: 6/6
c ---[ 504]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 503]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 502]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 501]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 500]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 499]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 498]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 497]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 496]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 495]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 494]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 493]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 492]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 491]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 490]---> Adder-cost: 52   maxlim: 40   bits: 6/6
c ---[ 489]---> Adder-cost: 66   maxlim: 46   bits: 6/6
c ---[ 488]---> Adder-cost: 70   maxlim: 52   bits: 6/6
c ---[ 487]---> Adder-cost: 68   maxlim: 58   bits: 6/6
c ---[ 486]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 485]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 484]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 483]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 482]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 481]---> Adder-cost: 32   maxlim: 22   bits: 5/5
c ---[ 480]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 479]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 478]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[ 477]---> Adder-cost: 72   maxlim: 46   bits: 6/6
c ---[ 476]---> Adder-cost: 80   maxlim: 52   bits: 6/6
c ---[ 475]---> Adder-cost: 86   maxlim: 58   bits: 6/6
c ---[ 474]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 473]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 472]---> Adder-cost: 28   maxlim: 22   bits: 5/5
c ---[ 471]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 470]---> Adder-cost: 42   maxlim: 34   bits: 6/6
c ---[ 469]---> Adder-cost: 66   maxlim: 40   bits: 6/6
c ---[ 468]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[ 467]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 466]---> Adder-cost: 70   maxlim: 58   bits: 6/6
c ---[ 465]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 464]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 463]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 462]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 461]---> Adder-cost: 50   maxlim: 34   bits: 6/6
c ---[ 460]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[ 459]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[ 458]---> Adder-cost: 76   maxlim: 52   bits: 6/6
c ---[ 457]---> Adder-cost: 76   maxlim: 58   bits: 6/6
c ---[ 456]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 455]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 454]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 453]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 452]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 451]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 450]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 449]---> Adder-cost: 42   maxlim: 22   bits: 5/5
c ---[ 448]---> Adder-cost: 44   maxlim: 28   bits: 5/5
c ---[ 447]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 446]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 445]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 444]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 443]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 442]---> Adder-cost: 54   maxlim: 40   bits: 6/6
c ---[ 441]---> Adder-cost: 72   maxlim: 46   bits: 6/6
c ---[ 440]---> Adder-cost: 70   maxlim: 52   bits: 6/6
c ---[ 439]---> Adder-cost: 84   maxlim: 58   bits: 6/6
c ---[ 438]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 437]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 436]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 435]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 434]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 433]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 432]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 431]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 430]---> Adder-cost: 64   maxlim: 40   bits: 6/6
c ---[ 429]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[ 428]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 427]---> Adder-cost: 86   maxlim: 58   bits: 6/6
c ---[ 426]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 425]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 424]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 423]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 422]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 421]---> Adder-cost: 48   maxlim: 40   bits: 6/6
c ---[ 420]---> Adder-cost: 56   maxlim: 46   bits: 6/6
c ---[ 419]---> Adder-cost: 68   maxlim: 52   bits: 6/6
c ---[ 418]---> Adder-cost: 64   maxlim: 58   bits: 6/6
c ---[ 417]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 416]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 415]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 414]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[ 413]---> Adder-cost: 44   maxlim: 34   bits: 6/6
c ---[ 412]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[ 411]---> Adder-cost: 64   maxlim: 46   bits: 6/6
c ---[ 410]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 409]---> Adder-cost: 84   maxlim: 58   bits: 6/6
c ---[ 408]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 407]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 406]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 405]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 404]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 403]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 402]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 401]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 400]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 399]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 398]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 397]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 396]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[ 395]---> Adder-cost: 54   maxlim: 34   bits: 6/6
c ---[ 394]---> Adder-cost: 58   maxlim: 40   bits: 6/6
c ---[ 393]---> Adder-cost: 64   maxlim: 46   bits: 6/6
c ---[ 392]---> Adder-cost: 68   maxlim: 52   bits: 6/6
c ---[ 391]---> Adder-cost: 72   maxlim: 58   bits: 6/6
c ---[ 390]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 389]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 388]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 387]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 386]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 385]---> Adder-cost: 32   maxlim: 22   bits: 5/5
c ---[ 384]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 383]---> Adder-cost: 54   maxlim: 34   bits: 6/6
c ---[ 382]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[ 381]---> Adder-cost: 68   maxlim: 46   bits: 6/6
c ---[ 380]---> Adder-cost: 78   maxlim: 52   bits: 6/6
c ---[ 379]---> Adder-cost: 82   maxlim: 58   bits: 6/6
c ---[ 378]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 377]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 376]---> Adder-cost: 28   maxlim: 22   bits: 5/5
c ---[ 375]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 374]---> Adder-cost: 46   maxlim: 34   bits: 6/6
c ---[ 373]---> Adder-cost: 66   maxlim: 40   bits: 6/6
c ---[ 372]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[ 371]---> Adder-cost: 68   maxlim: 52   bits: 6/6
c ---[ 370]---> Adder-cost: 68   maxlim: 58   bits: 6/6
c ---[ 369]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 368]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 367]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 366]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[ 365]---> Adder-cost: 54   maxlim: 34   bits: 6/6
c ---[ 364]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[ 363]---> Adder-cost: 66   maxlim: 46   bits: 6/6
c ---[ 362]---> Adder-cost: 76   maxlim: 52   bits: 6/6
c ---[ 361]---> Adder-cost: 76   maxlim: 58   bits: 6/6
c ---[ 360]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 359]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 358]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 357]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 356]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 355]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 354]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 353]---> Adder-cost: 40   maxlim: 22   bits: 5/5
c ---[ 352]---> Adder-cost: 44   maxlim: 28   bits: 5/5
c ---[ 351]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 350]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 349]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 348]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 347]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 346]---> Adder-cost: 50   maxlim: 40   bits: 6/6
c ---[ 345]---> Adder-cost: 66   maxlim: 46   bits: 6/6
c ---[ 344]---> Adder-cost: 66   maxlim: 52   bits: 6/6
c ---[ 343]---> Adder-cost: 74   maxlim: 58   bits: 6/6
c ---[ 342]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 341]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 340]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 339]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 338]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 337]---> Adder-cost: 42   maxlim: 22   bits: 5/5
c ---[ 336]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 335]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 334]---> Adder-cost: 66   maxlim: 40   bits: 6/6
c ---[ 333]---> Adder-cost: 72   maxlim: 46   bits: 6/6
c ---[ 332]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 331]---> Adder-cost: 86   maxlim: 58   bits: 6/6
c ---[ 330]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 329]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 328]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 327]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 326]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 325]---> Adder-cost: 56   maxlim: 40   bits: 6/6
c ---[ 324]---> Adder-cost: 62   maxlim: 46   bits: 6/6
c ---[ 323]---> Adder-cost: 68   maxlim: 52   bits: 6/6
c ---[ 322]---> Adder-cost: 64   maxlim: 58   bits: 6/6
c ---[ 321]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 320]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 319]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 318]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 317]---> Adder-cost: 50   maxlim: 34   bits: 6/6
c ---[ 316]---> Adder-cost: 56   maxlim: 40   bits: 6/6
c ---[ 315]---> Adder-cost: 60   maxlim: 46   bits: 6/6
c ---[ 314]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 313]---> Adder-cost: 68   maxlim: 58   bits: 6/6
c ---[ 312]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 311]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 310]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 309]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 308]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 307]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 306]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 305]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 304]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 303]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 302]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 301]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 300]---> Adder-cost: 38   maxlim: 28   bits: 5/5
c ---[ 299]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 298]---> Adder-cost: 56   maxlim: 40   bits: 6/6
c ---[ 297]---> Adder-cost: 64   maxlim: 46   bits: 6/6
c ---[ 296]---> Adder-cost: 68   maxlim: 52   bits: 6/6
c ---[ 295]---> Adder-cost: 68   maxlim: 58   bits: 6/6
c ---[ 294]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 293]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 292]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 291]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 290]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 289]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 288]---> Adder-cost: 38   maxlim: 28   bits: 5/5
c ---[ 287]---> Adder-cost: 56   maxlim: 34   bits: 6/6
c ---[ 286]---> Adder-cost: 56   maxlim: 40   bits: 6/6
c ---[ 285]---> Adder-cost: 74   maxlim: 46   bits: 6/6
c ---[ 284]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 283]---> Adder-cost: 90   maxlim: 58   bits: 6/6
c ---[ 282]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 281]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 280]---> Adder-cost: 28   maxlim: 22   bits: 5/5
c ---[ 279]---> Adder-cost: 28   maxlim: 28   bits: 5/5
c ---[ 278]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 277]---> Adder-cost: 54   maxlim: 40   bits: 6/6
c ---[ 276]---> Adder-cost: 52   maxlim: 46   bits: 6/6
c ---[ 275]---> Adder-cost: 56   maxlim: 52   bits: 6/6
c ---[ 274]---> Adder-cost: 60   maxlim: 58   bits: 6/6
c ---[ 273]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 272]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 271]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 270]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[ 269]---> Adder-cost: 54   maxlim: 34   bits: 6/6
c ---[ 268]---> Adder-cost: 62   maxlim: 40   bits: 6/6
c ---[ 267]---> Adder-cost: 66   maxlim: 46   bits: 6/6
c ---[ 266]---> Adder-cost: 78   maxlim: 52   bits: 6/6
c ---[ 265]---> Adder-cost: 76   maxlim: 58   bits: 6/6
c ---[ 264]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 263]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 262]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 261]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 260]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 259]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 258]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 257]---> Adder-cost: 40   maxlim: 22   bits: 5/5
c ---[ 256]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 255]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 254]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 253]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 252]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 251]---> Adder-cost: 46   maxlim: 34   bits: 6/6
c ---[ 250]---> Adder-cost: 50   maxlim: 40   bits: 6/6
c ---[ 249]---> Adder-cost: 68   maxlim: 46   bits: 6/6
c ---[ 248]---> Adder-cost: 68   maxlim: 52   bits: 6/6
c ---[ 247]---> Adder-cost: 74   maxlim: 58   bits: 6/6
c ---[ 246]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 245]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 244]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 243]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 242]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 241]---> Adder-cost: 32   maxlim: 22   bits: 5/5
c ---[ 240]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 239]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 238]---> Adder-cost: 60   maxlim: 40   bits: 6/6
c ---[ 237]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[ 236]---> Adder-cost: 78   maxlim: 52   bits: 6/6
c ---[ 235]---> Adder-cost: 86   maxlim: 58   bits: 6/6
c ---[ 234]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 233]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 232]---> Adder-cost: 32   maxlim: 22   bits: 5/5
c ---[ 231]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 230]---> Adder-cost: 58   maxlim: 34   bits: 6/6
c ---[ 229]---> Adder-cost: 60   maxlim: 40   bits: 6/6
c ---[ 228]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[ 227]---> Adder-cost: 68   maxlim: 52   bits: 6/6
c ---[ 226]---> Adder-cost: 84   maxlim: 58   bits: 6/6
c ---[ 225]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 224]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 223]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 222]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[ 221]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 220]---> Adder-cost: 58   maxlim: 40   bits: 6/6
c ---[ 219]---> Adder-cost: 56   maxlim: 46   bits: 6/6
c ---[ 218]---> Adder-cost: 80   maxlim: 52   bits: 6/6
c ---[ 217]---> Adder-cost: 68   maxlim: 58   bits: 6/6
c ---[ 216]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 215]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 214]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 213]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 212]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 211]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 210]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 209]---> Adder-cost: 40   maxlim: 22   bits: 5/5
c ---[ 208]---> Adder-cost: 40   maxlim: 28   bits: 5/5
c ---[ 207]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 206]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 205]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 204]---> Adder-cost: 34   maxlim: 28   bits: 5/5
c ---[ 203]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 202]---> Adder-cost: 52   maxlim: 40   bits: 6/6
c ---[ 201]---> Adder-cost: 64   maxlim: 46   bits: 6/6
c ---[ 200]---> Adder-cost: 68   maxlim: 52   bits: 6/6
c ---[ 199]---> Adder-cost: 72   maxlim: 58   bits: 6/6
c ---[ 198]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 197]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 196]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 195]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 194]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 193]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 192]---> Adder-cost: 38   maxlim: 28   bits: 5/5
c ---[ 191]---> Adder-cost: 50   maxlim: 34   bits: 6/6
c ---[ 190]---> Adder-cost: 58   maxlim: 40   bits: 6/6
c ---[ 189]---> Adder-cost: 64   maxlim: 46   bits: 6/6
c ---[ 188]---> Adder-cost: 76   maxlim: 52   bits: 6/6
c ---[ 187]---> Adder-cost: 78   maxlim: 58   bits: 6/6
c ---[ 186]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 185]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 184]---> Adder-cost: 28   maxlim: 22   bits: 5/5
c ---[ 183]---> Adder-cost: 32   maxlim: 28   bits: 5/5
c ---[ 182]---> Adder-cost: 42   maxlim: 34   bits: 6/6
c ---[ 181]---> Adder-cost: 48   maxlim: 40   bits: 6/6
c ---[ 180]---> Adder-cost: 48   maxlim: 46   bits: 6/6
c ---[ 179]---> Adder-cost: 56   maxlim: 52   bits: 6/6
c ---[ 178]---> Adder-cost: 60   maxlim: 58   bits: 6/6
c ---[ 177]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 176]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 175]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 174]---> Adder-cost: 42   maxlim: 28   bits: 5/5
c ---[ 173]---> Adder-cost: 52   maxlim: 34   bits: 6/6
c ---[ 172]---> Adder-cost: 64   maxlim: 40   bits: 6/6
c ---[ 171]---> Adder-cost: 74   maxlim: 46   bits: 6/6
c ---[ 170]---> Adder-cost: 70   maxlim: 52   bits: 6/6
c ---[ 169]---> Adder-cost: 80   maxlim: 58   bits: 6/6
c ---[ 168]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 167]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 166]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 165]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 164]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 163]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 162]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 161]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 160]---> Adder-cost: 38   maxlim: 28   bits: 5/5
c ---[ 159]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 158]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 157]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 156]---> Adder-cost: 28   maxlim: 28   bits: 5/5
c ---[ 155]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 154]---> Adder-cost: 56   maxlim: 40   bits: 6/6
c ---[ 153]---> Adder-cost: 68   maxlim: 46   bits: 6/6
c ---[ 152]---> Adder-cost: 72   maxlim: 52   bits: 6/6
c ---[ 151]---> Adder-cost: 80   maxlim: 58   bits: 6/6
c ---[ 150]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 149]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 148]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 147]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 146]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 145]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 144]---> Adder-cost: 36   maxlim: 28   bits: 5/5
c ---[ 143]---> Adder-cost: 46   maxlim: 34   bits: 6/6
c ---[ 142]---> Adder-cost: 56   maxlim: 40   bits: 6/6
c ---[ 141]---> Adder-cost: 62   maxlim: 46   bits: 6/6
c ---[ 140]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 139]---> Adder-cost: 82   maxlim: 58   bits: 6/6
c ---[ 138]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 137]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 136]---> Adder-cost: 28   maxlim: 22   bits: 5/5
c ---[ 135]---> Adder-cost: 28   maxlim: 28   bits: 5/5
c ---[ 134]---> Adder-cost: 42   maxlim: 34   bits: 6/6
c ---[ 133]---> Adder-cost: 46   maxlim: 40   bits: 6/6
c ---[ 132]---> Adder-cost: 56   maxlim: 46   bits: 6/6
c ---[ 131]---> Adder-cost: 60   maxlim: 52   bits: 6/6
c ---[ 130]---> Adder-cost: 60   maxlim: 58   bits: 6/6
c ---[ 129]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 128]---> Adder-cost: 26   maxlim: 16   bits: 5/5
c ---[ 127]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 126]---> Adder-cost: 38   maxlim: 28   bits: 5/5
c ---[ 125]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 124]---> Adder-cost: 58   maxlim: 40   bits: 6/6
c ---[ 123]---> Adder-cost: 64   maxlim: 46   bits: 6/6
c ---[ 122]---> Adder-cost: 76   maxlim: 52   bits: 6/6
c ---[ 121]---> Adder-cost: 84   maxlim: 58   bits: 6/6
c ---[ 120]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 119]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 118]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 117]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 116]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 115]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 114]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 113]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 112]---> Adder-cost: 44   maxlim: 28   bits: 5/5
c ---[ 111]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 110]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 109]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 108]---> Adder-cost: 28   maxlim: 28   bits: 5/5
c ---[ 107]---> Adder-cost: 48   maxlim: 34   bits: 6/6
c ---[ 106]---> Adder-cost: 50   maxlim: 40   bits: 6/6
c ---[ 105]---> Adder-cost: 70   maxlim: 46   bits: 6/6
c ---[ 104]---> Adder-cost: 74   maxlim: 52   bits: 6/6
c ---[ 103]---> Adder-cost: 72   maxlim: 58   bits: 6/6
c ---[ 102]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 101]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 100]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[  99]---> Adder-cost: 200   maxlim: 136   bits: 8/8
c ---[  98]---> Adder-cost: 208   maxlim: 136   bits: 8/8
c ---[  97]---> Adder-cost: 198   maxlim: 136   bits: 8/8
c ---[  96]---> Adder-cost: 204   maxlim: 136   bits: 8/8
c ---[  95]---> Adder-cost: 212   maxlim: 136   bits: 8/8
c ---[  94]---> Adder-cost: 108   maxlim: 70   bits: 7/7
c ---[  93]---> Adder-cost: 124   maxlim: 70   bits: 7/7
c ---[  92]---> Adder-cost: 216   maxlim: 136   bits: 8/8
c ---[  91]---> Adder-cost: 188   maxlim: 136   bits: 8/8
c ---[  90]---> Adder-cost: 222   maxlim: 136   bits: 8/8
c ---[  89]---> Adder-cost: 196   maxlim: 136   bits: 8/8
c ---[  88]---> Adder-cost: 198   maxlim: 136   bits: 8/8
c ---[  87]---> Adder-cost: 104   maxlim: 70   bits: 7/7
c ---[  86]---> Adder-cost: 118   maxlim: 70   bits: 7/7
c ---[  85]---> Adder-cost: 208   maxlim: 136   bits: 8/8
c ---[  84]---> Adder-cost: 194   maxlim: 136   bits: 8/8
c ---[  83]---> Adder-cost: 202   maxlim: 136   bits: 8/8
c ---[  82]---> Adder-cost: 204   maxlim: 136   bits: 8/8
c ---[  81]---> Adder-cost: 218   maxlim: 136   bits: 8/8
c ---[  80]---> Adder-cost: 102   maxlim: 70   bits: 7/7
c ---[  79]---> Adder-cost: 112   maxlim: 70   bits: 7/7
c ---[  78]---> Adder-cost: 198   maxlim: 136   bits: 8/8
c ---[  77]---> Adder-cost: 194   maxlim: 136   bits: 8/8
c ---[  76]---> Adder-cost: 222   maxlim: 136   bits: 8/8
c ---[  75]---> Adder-cost: 178   maxlim: 136   bits: 8/8
c ---[  74]---> Adder-cost: 190   maxlim: 136   bits: 8/8
c ---[  73]---> Adder-cost: 106   maxlim: 70   bits: 7/7
c ---[  72]---> Adder-cost: 112   maxlim: 70   bits: 7/7
c ---[  71]---> Adder-cost: 202   maxlim: 136   bits: 8/8
c ---[  70]---> Adder-cost: 190   maxlim: 136   bits: 8/8
c ---[  69]---> Adder-cost: 194   maxlim: 136   bits: 8/8
c ---[  68]---> Adder-cost: 190   maxlim: 136   bits: 8/8
c ---[  67]---> Adder-cost: 190   maxlim: 136   bits: 8/8
c ---[  66]---> Adder-cost: 104   maxlim: 70   bits: 7/7
c ---[  65]---> Adder-cost: 110   maxlim: 70   bits: 7/7
c ---[  64]---> Adder-cost: 192   maxlim: 136   bits: 8/8
c ---[  63]---> Adder-cost: 206   maxlim: 136   bits: 8/8
c ---[  62]---> Adder-cost: 196   maxlim: 136   bits: 8/8
c ---[  61]---> Adder-cost: 194   maxlim: 136   bits: 8/8
c ---[  60]---> Adder-cost: 194   maxlim: 136   bits: 8/8
c ---[  59]---> Adder-cost: 104   maxlim: 70   bits: 7/7
c ---[  58]---> Adder-cost: 112   maxlim: 70   bits: 7/7
c ---[  57]---> Adder-cost: 220   maxlim: 136   bits: 8/8
c ---[  56]---> Adder-cost: 194   maxlim: 136   bits: 8/8
c ---[  55]---> Adder-cost: 198   maxlim: 136   bits: 8/8
c ---[  54]---> Adder-cost: 178   maxlim: 136   bits: 8/8
c ---[  53]---> Adder-cost: 194   maxlim: 136   bits: 8/8
c ---[  52]---> Adder-cost: 98   maxlim: 70   bits: 7/7
c ---[  51]---> Adder-cost: 112   maxlim: 70   bits: 7/7
c ---[  50]---> Adder-cost: 194   maxlim: 136   bits: 8/8
c ---[  49]---> Adder-cost: 210   maxlim: 136   bits: 8/8
c ---[  48]---> Adder-cost: 218   maxlim: 136   bits: 8/8
c ---[  47]---> Adder-cost: 194   maxlim: 136   bits: 8/8
c ---[  46]---> Adder-cost: 198   maxlim: 136   bits: 8/8
c ---[  45]---> Adder-cost: 110   maxlim: 70   bits: 7/7
c ---[  44]---> Adder-cost: 106   maxlim: 70   bits: 7/7
c ---[  43]---> Adder-cost: 204   maxlim: 136   bits: 8/8
c ---[  42]---> Adder-cost: 198   maxlim: 136   bits: 8/8
c ---[  41]---> Adder-cost: 228   maxlim: 136   bits: 8/8
c ---[  40]---> Adder-cost: 182   maxlim: 136   bits: 8/8
c ---[  39]---> Adder-cost: 202   maxlim: 136   bits: 8/8
c ---[  38]---> Adder-cost: 106   maxlim: 70   bits: 7/7
c ---[  37]---> Adder-cost: 116   maxlim: 70   bits: 7/7
c ---[  36]---> Adder-cost: 216   maxlim: 136   bits: 8/8
c ---[  35]---> Adder-cost: 188   maxlim: 136   bits: 8/8
c ---[  34]---> Adder-cost: 218   maxlim: 136   bits: 8/8
c ---[  33]---> Adder-cost: 218   maxlim: 136   bits: 8/8
c ---[  32]---> Adder-cost: 196   maxlim: 136   bits: 8/8
c ---[  31]---> Adder-cost: 112   maxlim: 70   bits: 7/7
c ---[  30]---> Adder-cost: 110   maxlim: 70   bits: 7/7
c ---[  29]---> Adder-cost: 1424   maxlim: 828   bits: 10/10
c ---[  28]---> Adder-cost: 1394   maxlim: 828   bits: 10/10
c ---[  27]---> Adder-cost: 1388   maxlim: 828   bits: 10/10
c ---[  26]---> Adder-cost: 1422   maxlim: 828   bits: 10/10
c ---[  25]---> Adder-cost: 1416   maxlim: 828   bits: 10/10
c ---[  24]---> Adder-cost: 1418   maxlim: 828   bits: 10/10
c ---[  23]---> Adder-cost: 1414   maxlim: 828   bits: 10/10
c ---[  22]---> Adder-cost: 1380   maxlim: 828   bits: 10/10
c ---[  21]---> Adder-cost: 1434   maxlim: 828   bits: 10/10
c ---[  20]---> Adder-cost: 1364   maxlim: 828   bits: 10/10
c ---[  19]---> Adder-cost: 570   maxlim: 326   bits: 9/9
c ---[  18]---> Adder-cost: 574   maxlim: 326   bits: 9/9
c ---[  17]---> Adder-cost: 586   maxlim: 326   bits: 9/9
c ---[  16]---> Adder-cost: 578   maxlim: 326   bits: 9/9
c ---[  15]---> Adder-cost: 570   maxlim: 326   bits: 9/9
c ---[  14]---> Adder-cost: 568   maxlim: 326   bits: 9/9
c ---[  13]---> Adder-cost: 602   maxlim: 326   bits: 9/9
c ---[  12]---> Adder-cost: 588   maxlim: 326   bits: 9/9
c ---[  11]---> Adder-cost: 606   maxlim: 326   bits: 9/9
c ---[  10]---> Adder-cost: 550   maxlim: 326   bits: 9/9
c ---[   9]---> Adder-cost: 236   maxlim: 182   bits: 8/8
c ---[   8]---> Adder-cost: 228   maxlim: 182   bits: 8/8
c ---[   7]---> Adder-cost: 238   maxlim: 182   bits: 8/8
c ---[   6]---> Adder-cost: 232   maxlim: 182   bits: 8/8
c ---[   5]---> Adder-cost: 240   maxlim: 182   bits: 8/8
c ---[   4]---> Adder-cost: 230   maxlim: 182   bits: 8/8
c ---[   3]---> Adder-cost: 228   maxlim: 182   bits: 8/8
c ---[   2]---> Adder-cost: 222   maxlim: 182   bits: 8/8
c ---[   1]---> Adder-cost: 242   maxlim: 182   bits: 8/8
c ---[   0]---> Adder-cost: 260   maxlim: 182   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2245912  8066751 |  748637       0        0     nan |  0.000 % |
c |       100 | 2245912  8066751 |  823500     100      298     3.0 |  3.788 % |
c |       250 | 2245214  8064341 |  905850     135      414     3.1 |  3.821 % |
c |       475 | 2244120  8060545 |  996435     214      681     3.2 |  3.876 % |
c |       812 | 2243298  8057677 | 1096079     457     1516     3.3 |  3.921 % |
c |      1318 | 2242007  8053207 | 1205687     785     2570     3.3 |  3.985 % |
c |      2077 | 2240431  8047765 | 1326256    1296     4205     3.2 |  4.060 % |
c |      3216 | 2236662  8034692 | 1458881    1925     6171     3.2 |  4.244 % |
c |      4924 | 2232353  8019692 | 1604769    3062    10186     3.3 |  4.458 % |
c |      7486 | 2231275  8015963 | 1765246    5474    22109     4.0 |  4.511 % |
c |     11330 | 2227533  8002808 | 1941771    8850    39332     4.4 |  4.653 % |
c |     17097 | 2219924  7975946 | 2135948   13777    65362     4.7 |  4.917 % |
#### 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.92 0.95 0.90 2/54 14993
Raw data (stat): 14993 (runsolver) R 14992 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481941326 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 34353 0 0 0 911 87 0 0 25 0 1 0 481941326 156172288 33060 4294967295 134512640 134672761 3221224544 3221217352 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38128 33061 603 41 0 38087 0
vsize: 152512
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39980 0 0 0 1896 101 0 0 25 0 1 0 481941326 182267904 38687 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 38687 603 41 0 44458 0
vsize: 177996
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39980 0 0 0 2896 101 0 0 25 0 1 0 481941326 182267904 38687 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 38687 603 41 0 44458 0
vsize: 177996
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39981 0 0 0 3896 102 0 0 25 0 1 0 481941326 182267904 38688 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 38688 603 41 0 44458 0
vsize: 177996
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39981 0 0 0 4896 102 0 0 25 0 1 0 481941326 182267904 38688 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 38688 603 41 0 44458 0
vsize: 177996
[startup+60.0028 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39981 0 0 0 5897 102 0 0 25 0 1 0 481941326 182267904 38688 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 38688 603 41 0 44458 0
vsize: 177996
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39981 0 0 0 6897 102 0 0 25 0 1 0 481941326 182267904 38688 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 38688 603 41 0 44458 0
vsize: 177996
[startup+80.0042 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39981 0 0 0 7897 102 0 0 25 0 1 0 481941326 182267904 38688 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 38688 603 41 0 44458 0
vsize: 177996
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39982 0 0 0 8897 102 0 0 25 0 1 0 481941326 182267904 38689 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44499 38689 603 41 0 44458 0
vsize: 177996
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39982 0 0 0 9896 102 0 0 25 0 1 0 481941326 182267904 38689 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 38689 603 41 0 44458 0
vsize: 177996
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39983 0 0 0 10896 102 0 0 25 0 1 0 481941326 182267904 38690 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44499 38690 603 41 0 44458 0
vsize: 177996
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 39988 0 0 0 11896 102 0 0 25 0 1 0 481941326 182403072 38695 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44532 38695 603 41 0 44491 0
vsize: 178128
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40018 0 0 0 12896 102 0 0 25 0 1 0 481941326 182403072 38725 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44532 38725 603 41 0 44491 0
vsize: 178128
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40041 0 0 0 13896 102 0 0 25 0 1 0 481941326 182538240 38748 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44565 38748 603 41 0 44524 0
vsize: 178260
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40071 0 0 0 14896 102 0 0 25 0 1 0 481941326 182673408 38778 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44598 38778 603 41 0 44557 0
vsize: 178392
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40097 0 0 0 15896 102 0 0 25 0 1 0 481941326 182808576 38804 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44631 38804 603 41 0 44590 0
vsize: 178524
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40119 0 0 0 16896 103 0 0 25 0 1 0 481941326 182943744 38826 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44664 38826 603 41 0 44623 0
vsize: 178656
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40147 0 0 0 17896 103 0 0 25 0 1 0 481941326 182943744 38854 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44664 38854 603 41 0 44623 0
vsize: 178656
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40191 0 0 0 18896 103 0 0 25 0 1 0 481941326 183214080 38898 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44730 38898 603 41 0 44689 0
vsize: 178920
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40211 0 0 0 19896 103 0 0 25 0 1 0 481941326 183214080 38918 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44730 38918 603 41 0 44689 0
vsize: 178920
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40267 0 0 0 20896 103 0 0 25 0 1 0 481941326 183484416 38974 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44796 38974 603 41 0 44755 0
vsize: 179184
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40301 0 0 0 21896 103 0 0 25 0 1 0 481941326 183619584 39008 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44829 39008 603 41 0 44788 0
vsize: 179316
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40345 0 0 0 22896 103 0 0 25 0 1 0 481941326 183754752 39052 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44862 39052 603 41 0 44821 0
vsize: 179448
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40382 0 0 0 23896 104 0 0 25 0 1 0 481941326 183889920 39089 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44895 39089 603 41 0 44854 0
vsize: 179580
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40414 0 0 0 24896 104 0 0 25 0 1 0 481941326 184160256 39121 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44961 39121 603 41 0 44920 0
vsize: 179844
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40444 0 0 0 25896 104 0 0 25 0 1 0 481941326 184295424 39151 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44994 39151 603 41 0 44953 0
vsize: 179976
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40498 0 0 0 26896 104 0 0 25 0 1 0 481941326 184430592 39205 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45027 39205 603 41 0 44986 0
vsize: 180108
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40527 0 0 0 27896 104 0 0 25 0 1 0 481941326 184565760 39234 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45060 39234 603 41 0 45019 0
vsize: 180240
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40578 0 0 0 28897 104 0 0 25 0 1 0 481941326 184836096 39285 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45126 39285 603 41 0 45085 0
vsize: 180504
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40635 0 0 0 29897 104 0 0 25 0 1 0 481941326 184971264 39342 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45159 39342 603 41 0 45118 0
vsize: 180636
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40664 0 0 0 30898 104 0 0 25 0 1 0 481941326 185106432 39371 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45192 39371 603 41 0 45151 0
vsize: 180768
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40696 0 0 0 31898 105 0 0 25 0 1 0 481941326 185241600 39403 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45225 39403 603 41 0 45184 0
vsize: 180900
[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40715 0 0 0 32898 105 0 0 25 0 1 0 481941326 185376768 39422 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45258 39422 603 41 0 45217 0
vsize: 181032
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40768 0 0 0 33898 105 0 0 25 0 1 0 481941326 185511936 39475 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45291 39475 603 41 0 45250 0
vsize: 181164
[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40824 0 0 0 34898 105 0 0 25 0 1 0 481941326 185782272 39531 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45357 39531 603 41 0 45316 0
vsize: 181428
[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40856 0 0 0 35898 105 0 0 25 0 1 0 481941326 185917440 39563 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45390 39563 603 41 0 45349 0
vsize: 181560
[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40869 0 0 0 36899 105 0 0 25 0 1 0 481941326 185917440 39576 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45390 39576 603 41 0 45349 0
vsize: 181560
[startup+380.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40897 0 0 0 37899 105 0 0 25 0 1 0 481941326 186052608 39604 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45423 39604 603 41 0 45382 0
vsize: 181692
[startup+390.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40908 0 0 0 38899 105 0 0 25 0 1 0 481941326 186052608 39615 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45423 39615 603 41 0 45382 0
vsize: 181692
[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40925 0 0 0 39899 105 0 0 25 0 1 0 481941326 186187776 39632 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45456 39632 603 41 0 45415 0
vsize: 181824
[startup+410.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40945 0 0 0 40899 105 0 0 25 0 1 0 481941326 186322944 39652 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45489 39652 603 41 0 45448 0
vsize: 181956
[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 40980 0 0 0 41900 105 0 0 25 0 1 0 481941326 186458112 39687 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45522 39687 603 41 0 45481 0
vsize: 182088
[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41001 0 0 0 42900 105 0 0 25 0 1 0 481941326 186458112 39708 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45522 39708 603 41 0 45481 0
vsize: 182088
[startup+440.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41011 0 0 0 43902 105 0 0 25 0 1 0 481941326 186593280 39718 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45555 39718 603 41 0 45514 0
vsize: 182220
[startup+450.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41029 0 0 0 44902 105 0 0 25 0 1 0 481941326 186593280 39736 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45555 39736 603 41 0 45514 0
vsize: 182220
[startup+460.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41063 0 0 0 45902 106 0 0 25 0 1 0 481941326 186728448 39770 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45588 39770 603 41 0 45547 0
vsize: 182352
[startup+470.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41086 0 0 0 46902 106 0 0 25 0 1 0 481941326 186863616 39793 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45621 39793 603 41 0 45580 0
vsize: 182484
[startup+480.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41093 0 0 0 47902 106 0 0 25 0 1 0 481941326 186863616 39800 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45621 39800 603 41 0 45580 0
vsize: 182484
[startup+490.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41128 0 0 0 48902 106 0 0 25 0 1 0 481941326 186998784 39835 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45654 39835 603 41 0 45613 0
vsize: 182616
[startup+500.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41154 0 0 0 49903 106 0 0 25 0 1 0 481941326 187240448 39861 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45713 39861 603 41 0 45672 0
vsize: 182852
[startup+510.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41186 0 0 0 50903 106 0 0 25 0 1 0 481941326 187240448 39893 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45713 39893 603 41 0 45672 0
vsize: 182852
[startup+520.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41237 0 0 0 51903 106 0 0 25 0 1 0 481941326 187510784 39944 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45779 39944 603 41 0 45738 0
vsize: 183116
[startup+530.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41256 0 0 0 52903 106 0 0 25 0 1 0 481941326 187645952 39963 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45812 39963 603 41 0 45771 0
vsize: 183248
[startup+540.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41275 0 0 0 53903 106 0 0 25 0 1 0 481941326 187645952 39982 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45812 39982 603 41 0 45771 0
vsize: 183248
[startup+550.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41296 0 0 0 54903 106 0 0 25 0 1 0 481941326 187781120 40003 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45845 40003 603 41 0 45804 0
vsize: 183380
[startup+560.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41311 0 0 0 55903 106 0 0 25 0 1 0 481941326 187781120 40018 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45845 40018 603 41 0 45804 0
vsize: 183380
[startup+570.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41330 0 0 0 56906 106 0 0 25 0 1 0 481941326 187916288 40037 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45878 40037 603 41 0 45837 0
vsize: 183512
[startup+580.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41336 0 0 0 57906 106 0 0 25 0 1 0 481941326 187916288 40043 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45878 40043 603 41 0 45837 0
vsize: 183512
[startup+590.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41369 0 0 0 58906 106 0 0 25 0 1 0 481941326 188051456 40076 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45911 40076 603 41 0 45870 0
vsize: 183644
[startup+600.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41398 0 0 0 59906 106 0 0 25 0 1 0 481941326 188186624 40105 4294967295 134512640 134672761 3221224544 3221223692 134565968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45944 40105 603 41 0 45903 0
vsize: 183776
[startup+610.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41420 0 0 0 60907 106 0 0 25 0 1 0 481941326 188321792 40127 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45977 40127 603 41 0 45936 0
vsize: 183908
[startup+620.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41448 0 0 0 61907 106 0 0 25 0 1 0 481941326 188321792 40155 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45977 40155 603 41 0 45936 0
vsize: 183908
[startup+630.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14993
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41482 0 0 0 62907 107 0 0 25 0 1 0 481941326 188456960 40189 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46010 40189 603 41 0 45969 0
vsize: 184040
[startup+640.088 s]
Raw data (loadavg): 0.99 0.97 0.91 5/59 15019
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41503 0 0 0 63907 107 0 0 25 0 1 0 481941326 188592128 40210 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46043 40210 603 41 0 46002 0
vsize: 184172
[startup+650.17 s]
Raw data (loadavg): 1.22 1.02 0.93 2/54 15046
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41531 0 0 0 64915 107 0 0 25 0 1 0 481941326 188727296 40238 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46076 40238 603 41 0 46035 0
vsize: 184304
[startup+660.17 s]
Raw data (loadavg): 1.26 1.04 0.93 2/54 15046
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41568 0 0 0 65914 107 0 0 25 0 1 0 481941326 188862464 40275 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46109 40275 603 41 0 46068 0
vsize: 184436
[startup+670.171 s]
Raw data (loadavg): 1.22 1.03 0.93 2/54 15046
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41579 0 0 0 66914 107 0 0 25 0 1 0 481941326 188862464 40286 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46109 40286 603 41 0 46068 0
vsize: 184436
[startup+680.171 s]
Raw data (loadavg): 1.19 1.03 0.93 2/54 15046
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41603 0 0 0 67914 107 0 0 25 0 1 0 481941326 188997632 40310 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46142 40310 603 41 0 46101 0
vsize: 184568
[startup+690.171 s]
Raw data (loadavg): 1.16 1.03 0.93 2/54 15046
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41625 0 0 0 68915 107 0 0 25 0 1 0 481941326 189132800 40332 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46175 40332 603 41 0 46134 0
vsize: 184700
[startup+700.172 s]
Raw data (loadavg): 1.13 1.03 0.93 2/54 15046
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41646 0 0 0 69915 107 0 0 25 0 1 0 481941326 189132800 40353 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46175 40353 603 41 0 46134 0
vsize: 184700
[startup+710.173 s]
Raw data (loadavg): 1.11 1.03 0.93 2/54 15046
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41659 0 0 0 70915 107 0 0 25 0 1 0 481941326 189267968 40366 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46208 40366 603 41 0 46167 0
vsize: 184832
[startup+720.173 s]
Raw data (loadavg): 1.09 1.03 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41679 0 0 0 71915 107 0 0 25 0 1 0 481941326 189267968 40386 4294967295 134512640 134672761 3221224544 3221223708 134564505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46208 40386 603 41 0 46167 0
vsize: 184832
[startup+730.174 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41694 0 0 0 72915 108 0 0 25 0 1 0 481941326 189403136 40401 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46241 40401 603 41 0 46200 0
vsize: 184964
[startup+740.174 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41723 0 0 0 73915 108 0 0 25 0 1 0 481941326 189538304 40430 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46274 40430 603 41 0 46233 0
vsize: 185096
[startup+750.175 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41736 0 0 0 74915 108 0 0 25 0 1 0 481941326 189538304 40443 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46274 40443 603 41 0 46233 0
vsize: 185096
[startup+760.176 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41743 0 0 0 75916 108 0 0 25 0 1 0 481941326 189538304 40450 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46274 40450 603 41 0 46233 0
vsize: 185096
[startup+770.177 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41754 0 0 0 76916 108 0 0 25 0 1 0 481941326 189673472 40461 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46307 40461 603 41 0 46266 0
vsize: 185228
[startup+780.178 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41770 0 0 0 77916 108 0 0 25 0 1 0 481941326 189673472 40477 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46307 40477 603 41 0 46266 0
vsize: 185228
[startup+790.177 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41791 0 0 0 78916 108 0 0 25 0 1 0 481941326 189808640 40498 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46340 40498 603 41 0 46299 0
vsize: 185360
[startup+800.177 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41806 0 0 0 79916 108 0 0 25 0 1 0 481941326 189808640 40513 4294967295 134512640 134672761 3221224544 3221223800 134562229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46340 40513 603 41 0 46299 0
vsize: 185360
[startup+810.178 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41829 0 0 0 80916 108 0 0 25 0 1 0 481941326 189943808 40536 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46373 40536 603 41 0 46332 0
vsize: 185492
[startup+820.179 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41853 0 0 0 81917 108 0 0 25 0 1 0 481941326 190078976 40560 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46406 40560 603 41 0 46365 0
vsize: 185624
[startup+830.179 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41870 0 0 0 82917 108 0 0 25 0 1 0 481941326 190078976 40577 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46406 40577 603 41 0 46365 0
vsize: 185624
[startup+840.18 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41870 0 0 0 83917 108 0 0 25 0 1 0 481941326 190078976 40577 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46406 40577 603 41 0 46365 0
vsize: 185624
[startup+850.18 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41873 0 0 0 84917 108 0 0 25 0 1 0 481941326 190078976 40580 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46406 40580 603 41 0 46365 0
vsize: 185624
[startup+860.18 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41882 0 0 0 85917 108 0 0 25 0 1 0 481941326 190214144 40589 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46439 40589 603 41 0 46398 0
vsize: 185756
[startup+870.182 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41886 0 0 0 86917 108 0 0 25 0 1 0 481941326 190214144 40593 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46439 40593 603 41 0 46398 0
vsize: 185756
[startup+880.182 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41898 0 0 0 87918 108 0 0 25 0 1 0 481941326 190214144 40605 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46439 40605 603 41 0 46398 0
vsize: 185756
[startup+890.182 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41918 0 0 0 88918 108 0 0 25 0 1 0 481941326 190349312 40625 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46472 40625 603 41 0 46431 0
vsize: 185888
[startup+900.183 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41928 0 0 0 89918 108 0 0 25 0 1 0 481941326 190349312 40635 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46472 40635 603 41 0 46431 0
vsize: 185888
[startup+910.183 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41949 0 0 0 90918 108 0 0 25 0 1 0 481941326 190484480 40656 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46505 40656 603 41 0 46464 0
vsize: 186020
[startup+920.184 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41966 0 0 0 91918 108 0 0 25 0 1 0 481941326 190484480 40673 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46505 40673 603 41 0 46464 0
vsize: 186020
[startup+930.185 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41986 0 0 0 92918 108 0 0 25 0 1 0 481941326 190619648 40693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46538 40693 603 41 0 46497 0
vsize: 186152
[startup+940.184 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 41995 0 0 0 93918 108 0 0 25 0 1 0 481941326 190619648 40702 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46538 40702 603 41 0 46497 0
vsize: 186152
[startup+950.185 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42003 0 0 0 94918 109 0 0 25 0 1 0 481941326 190619648 40710 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46538 40710 603 41 0 46497 0
vsize: 186152
[startup+960.185 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42007 0 0 0 95919 109 0 0 25 0 1 0 481941326 190619648 40714 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46538 40714 603 41 0 46497 0
vsize: 186152
[startup+970.185 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42009 0 0 0 96919 109 0 0 25 0 1 0 481941326 190754816 40716 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46571 40716 603 41 0 46530 0
vsize: 186284
[startup+980.186 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15048
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42012 0 0 0 97919 109 0 0 25 0 1 0 481941326 190754816 40719 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46571 40719 603 41 0 46530 0
vsize: 186284
[startup+990.186 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42021 0 0 0 98919 109 0 0 25 0 1 0 481941326 190754816 40728 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46571 40728 603 41 0 46530 0
vsize: 186284
[startup+1000.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42028 0 0 0 99919 109 0 0 25 0 1 0 481941326 190754816 40735 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46571 40735 603 41 0 46530 0
vsize: 186284
[startup+1010.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42040 0 0 0 100919 109 0 0 25 0 1 0 481941326 190754816 40747 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46571 40747 603 41 0 46530 0
vsize: 186284
[startup+1020.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42044 0 0 0 101920 109 0 0 25 0 1 0 481941326 190889984 40751 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46604 40751 603 41 0 46563 0
vsize: 186416
[startup+1030.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42049 0 0 0 102920 109 0 0 25 0 1 0 481941326 190889984 40756 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46604 40756 603 41 0 46563 0
vsize: 186416
[startup+1040.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42062 0 0 0 103920 109 0 0 25 0 1 0 481941326 190889984 40769 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46604 40769 603 41 0 46563 0
vsize: 186416
[startup+1050.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42068 0 0 0 104920 109 0 0 25 0 1 0 481941326 190889984 40775 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46604 40775 603 41 0 46563 0
vsize: 186416
[startup+1060.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42075 0 0 0 105920 109 0 0 25 0 1 0 481941326 190889984 40782 4294967295 134512640 134672761 3221224544 3221223796 134562288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46604 40782 603 41 0 46563 0
vsize: 186416
[startup+1070.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42078 0 0 0 106921 109 0 0 25 0 1 0 481941326 191021056 40785 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46636 40785 603 41 0 46595 0
vsize: 186544
[startup+1080.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42089 0 0 0 107921 109 0 0 25 0 1 0 481941326 191021056 40796 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46636 40796 603 41 0 46595 0
vsize: 186544
[startup+1090.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42092 0 0 0 108921 109 0 0 25 0 1 0 481941326 191021056 40799 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46636 40799 603 41 0 46595 0
vsize: 186544
[startup+1100.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42095 0 0 0 109921 109 0 0 25 0 1 0 481941326 191021056 40802 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46636 40802 603 41 0 46595 0
vsize: 186544
[startup+1110.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42103 0 0 0 110921 109 0 0 25 0 1 0 481941326 191021056 40810 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46636 40810 603 41 0 46595 0
vsize: 186544
[startup+1120.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42125 0 0 0 111921 109 0 0 25 0 1 0 481941326 191156224 40832 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46669 40832 603 41 0 46628 0
vsize: 186676
[startup+1130.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42136 0 0 0 112921 109 0 0 25 0 1 0 481941326 191156224 40843 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46669 40843 603 41 0 46628 0
vsize: 186676
[startup+1140.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42146 0 0 0 113921 109 0 0 25 0 1 0 481941326 191291392 40853 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46702 40853 603 41 0 46661 0
vsize: 186808
[startup+1150.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42149 0 0 0 114922 109 0 0 25 0 1 0 481941326 191291392 40856 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46702 40856 603 41 0 46661 0
vsize: 186808
[startup+1160.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42157 0 0 0 115922 109 0 0 25 0 1 0 481941326 191291392 40864 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46702 40864 603 41 0 46661 0
vsize: 186808
[startup+1170.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42160 0 0 0 116921 109 0 0 25 0 1 0 481941326 191291392 40867 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46702 40867 603 41 0 46661 0
vsize: 186808
[startup+1180.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42167 0 0 0 117921 109 0 0 25 0 1 0 481941326 191291392 40874 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46702 40874 603 41 0 46661 0
vsize: 186808
[startup+1190.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42182 0 0 0 118921 110 0 0 25 0 1 0 481941326 191426560 40889 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46735 40889 603 41 0 46694 0
vsize: 186940
[startup+1200.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15050
Raw data (stat): 14993 (minisat+) R 14992 25285 25284 0 -1 0 42189 0 0 0 119922 110 0 0 25 0 1 0 481941326 191426560 40896 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46735 40896 603 41 0 46694 0
vsize: 186940
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.28 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 15050
Raw data (stat): 14993 (minisat+) Z 14992 25285 25284 0 -1 12 42191 0 0 0 119922 118 0 0 25 0 1 0 481941326 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.28
CPU time (s): 1200.4
CPU user time (s): 1199.22
CPU system time (s): 1.18182
CPU usage (%): 100.011
Max. virtual memory (Kb): 186940
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####