PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-seba.opb
MD5SUM	41b5898e0f1b65f739b9a89af7596ef6
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	7565
Biggest coefficient in the objective function	258342282854400
Number of bits for the biggest coefficient in the objective function	48
Sum of the numbers in the objective function	4664562894591719
Number of bits of the sum of numbers in the objective function	53
Biggest number in a constraint	258342282854400
Number of bits of the biggest number in a constraint	48
Biggest sum of numbers in a constraint	4664562894591719
Number of bits of the biggest sum of numbers	53
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1259.63
Number of variables	23376
Total number of constraints	1029
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1029
Minimum length of a constraint	10
Maximum length of a constraint	496
Trace number 30670

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        449736 kB
Buffers:         35008 kB
Cached:         524332 kB
SwapCached:        572 kB
Active:          68176 kB
Inactive:       496664 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        449484 kB
SwapTotal:     2097892 kB
SwapFree:      2096728 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5612 kB
Slab:            14576 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 18:44:45 (client local time) WITH STATUS 152 IN 1229.92 SECONDS
stats: 22058 7 1229.92 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c PARSE ERROR! [line 1032] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1421 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1491]---> BDD-cost:   11
c ---[1490]---> BDD-cost:   11
c ---[1489]---> BDD-cost:   12
c ---[1488]---> BDD-cost:   15
c ---[1486]---> BDD-cost:   14
c ---[1485]---> BDD-cost:   11
c ---[1483]---> BDD-cost:   17
c ---[1482]---> BDD-cost:   18
c ---[1481]---> BDD-cost:   18
c ---[1480]---> BDD-cost:   17
c ---[1479]---> BDD-cost:   14
c ---[1478]---> BDD-cost:   16
c ---[1477]---> BDD-cost:   17
c ---[1476]---> BDD-cost:   18
c ---[1475]---> BDD-cost:   16
c ---[1474]---> BDD-cost:   17
c ---[1473]---> BDD-cost:   19
c ---[1472]---> BDD-cost:   13
c ---[1471]---> BDD-cost:   13
c ---[1470]---> BDD-cost:   13
c ---[1469]---> BDD-cost:   14
c ---[1467]---> BDD-cost:   16
c ---[1466]---> BDD-cost:   19
c ---[1465]---> BDD-cost:   19
c ---[1464]---> BDD-cost:   17
c ---[1463]---> BDD-cost:   18
c ---[1462]---> BDD-cost:   17
c ---[1461]---> BDD-cost:   14
c ---[1459]---> BDD-cost:   19
c ---[1458]---> BDD-cost:   13
c ---[1457]---> BDD-cost:   15
c ---[1456]---> BDD-cost:   14
c ---[1455]---> BDD-cost:   19
c ---[1454]---> BDD-cost:   18
c ---[1453]---> BDD-cost:   14
c ---[1451]---> BDD-cost:   17
c ---[1450]---> BDD-cost:   13
c ---[1449]---> BDD-cost:   14
c ---[1448]---> BDD-cost:   15
c ---[1447]---> BDD-cost:   12
c ---[1445]---> BDD-cost:   14
c ---[1443]---> BDD-cost:   15
c ---[1442]---> BDD-cost:   13
c ---[1441]---> BDD-cost:   16
c ---[1440]---> BDD-cost:   14
c ---[1439]---> BDD-cost:   14
c ---[1438]---> BDD-cost:   14
c ---[1437]---> BDD-cost:   15
c ---[1432]---> BDD-cost:   14
c ---[1431]---> BDD-cost:   15
c ---[1429]---> BDD-cost:   19
c ---[1428]---> BDD-cost:   19
c ---[1427]---> BDD-cost:   19
c ---[1425]---> BDD-cost:   11
c ---[1424]---> BDD-cost:   17
c ---[1423]---> BDD-cost:   16
c ---[1422]---> BDD-cost:   13
c ---[1421]---> BDD-cost:   17
c ---[1420]---> BDD-cost:   18
c ---[1419]---> BDD-cost:   18
c ---[1418]---> BDD-cost:   12
c ---[1417]---> BDD-cost:   17
c ---[1416]---> BDD-cost:   17
c ---[1415]---> BDD-cost:   14
c ---[1414]---> BDD-cost:   16
c ---[1413]---> BDD-cost:   13
c ---[1412]---> BDD-cost:   13
c ---[1411]---> BDD-cost:   16
c ---[1410]---> BDD-cost:   14
c ---[1406]---> BDD-cost:   19
c ---[1405]---> BDD-cost:   16
c ---[1404]---> BDD-cost:   11
c ---[1403]---> BDD-cost:   17
c ---[1401]---> BDD-cost:   14
c ---[1400]---> BDD-cost:   14
c ---[1399]---> BDD-cost:   13
c ---[1397]---> BDD-cost:   16
c ---[1396]---> BDD-cost:   11
c ---[1395]---> BDD-cost:   13
c ---[1394]---> BDD-cost:   18
c ---[1393]---> BDD-cost:   17
c ---[1392]---> BDD-cost:   16
c ---[1391]---> BDD-cost:   13
c ---[1390]---> BDD-cost:   13
c ---[1389]---> BDD-cost:   15
c ---[1388]---> BDD-cost:   14
c ---[1387]---> BDD-cost:   11
c ---[1386]---> BDD-cost:   16
c ---[1385]---> BDD-cost:   17
c ---[1384]---> BDD-cost:   15
c ---[1383]---> BDD-cost:   15
c ---[1382]---> BDD-cost:   15
c ---[1381]---> BDD-cost:   16
c ---[1380]---> BDD-cost:    8
c ---[1378]---> BDD-cost:   10
c ---[1377]---> BDD-cost:   15
c ---[1376]---> BDD-cost:   15
c ---[1375]---> BDD-cost:   14
c ---[1374]---> BDD-cost:   18
c ---[1373]---> BDD-cost:   11
c ---[1372]---> BDD-cost:   17
c ---[1371]---> BDD-cost:   18
c ---[1370]---> BDD-cost:   14
c ---[1369]---> BDD-cost:   15
c ---[1365]---> BDD-cost:   18
c ---[1364]---> BDD-cost:   19
c ---[1363]---> BDD-cost:   16
c ---[1362]---> BDD-cost:   14
c ---[1361]---> BDD-cost:   17
c ---[1359]---> BDD-cost:   15
c ---[1358]---> BDD-cost:   14
c ---[1357]---> BDD-cost:   15
c ---[1354]---> BDD-cost:   16
c ---[1352]---> BDD-cost:   13
c ---[1350]---> BDD-cost:   17
c ---[1349]---> BDD-cost:   15
c ---[1348]---> BDD-cost:   15
c ---[1347]---> BDD-cost:   15
c ---[1346]---> BDD-cost:   16
c ---[1343]---> BDD-cost:   14
c ---[1342]---> BDD-cost:    9
c ---[1341]---> BDD-cost:   14
c ---[1340]---> BDD-cost:   15
c ---[1339]---> BDD-cost:   14
c ---[1338]---> BDD-cost:   14
c ---[1337]---> BDD-cost:   14
c ---[1336]---> BDD-cost:   13
c ---[1335]---> BDD-cost:   15
c ---[1334]---> BDD-cost:   14
c ---[1333]---> BDD-cost:   14
c ---[1332]---> BDD-cost:   15
c ---[1331]---> BDD-cost:   15
c ---[1329]---> BDD-cost:   15
c ---[1328]---> BDD-cost:   12
c ---[1327]---> BDD-cost:   10
c ---[1326]---> BDD-cost:   14
c ---[1325]---> BDD-cost:   11
c ---[1324]---> BDD-cost:   15
c ---[1323]---> BDD-cost:   14
c ---[1322]---> BDD-cost:   11
c ---[1321]---> BDD-cost:   15
c ---[1320]---> BDD-cost:   18
c ---[1319]---> BDD-cost:   15
c ---[1317]---> BDD-cost:   12
c ---[1316]---> BDD-cost:   13
c ---[1315]---> BDD-cost:   11
c ---[1314]---> BDD-cost:   13
c ---[1313]---> BDD-cost:   13
c ---[1312]---> BDD-cost:   11
c ---[1311]---> BDD-cost:   18
c ---[1310]---> BDD-cost:   17
c ---[1308]---> BDD-cost:   13
c ---[1306]---> BDD-cost:   13
c ---[1305]---> BDD-cost:   17
c ---[1304]---> BDD-cost:   14
c ---[1303]---> BDD-cost:   15
c ---[1300]---> BDD-cost:   14
c ---[1297]---> BDD-cost:   16
c ---[1296]---> BDD-cost:   16
c ---[1295]---> BDD-cost:   13
c ---[1293]---> BDD-cost:   15
c ---[1290]---> BDD-cost:   10
c ---[1289]---> BDD-cost:   16
c ---[1288]---> BDD-cost:   18
c ---[1287]---> BDD-cost:   10
c ---[1286]---> BDD-cost:   17
c ---[1285]---> BDD-cost:   14
c ---[1284]---> BDD-cost:   14
c ---[1283]---> BDD-cost:   11
c ---[1281]---> BDD-cost:   11
c ---[1280]---> BDD-cost:   14
c ---[1278]---> BDD-cost:   16
c ---[1277]---> BDD-cost:   13
c ---[1276]---> BDD-cost:   16
c ---[1274]---> BDD-cost:   15
c ---[1271]---> BDD-cost:   15
c ---[1270]---> BDD-cost:   14
c ---[1268]---> BDD-cost:   11
c ---[1267]---> BDD-cost:   14
c ---[1266]---> BDD-cost:   15
c ---[1265]---> BDD-cost:   14
c ---[1264]---> BDD-cost:   12
c ---[1262]---> BDD-cost:   12
c ---[1261]---> BDD-cost:   13
c ---[1260]---> BDD-cost:   14
c ---[1259]---> BDD-cost:   16
c ---[1257]---> BDD-cost:   15
c ---[1256]---> BDD-cost:   17
c ---[1255]---> BDD-cost:   18
c ---[1253]---> BDD-cost:   17
c ---[1251]---> BDD-cost:   15
c ---[1249]---> BDD-cost:    9
c ---[1248]---> BDD-cost:    5
c ---[1247]---> BDD-cost:    9
c ---[1246]---> BDD-cost:   14
c ---[1245]---> BDD-cost:   15
c ---[1244]---> BDD-cost:   13
c ---[1243]---> BDD-cost:   15
c ---[1242]---> BDD-cost:   13
c ---[1241]---> BDD-cost:   12
c ---[1240]---> BDD-cost:   15
c ---[1239]---> BDD-cost:   13
c ---[1237]---> BDD-cost:   18
c ---[1236]---> BDD-cost:   17
c ---[1235]---> BDD-cost:   11
c ---[1234]---> BDD-cost:   15
c ---[1233]---> BDD-cost:   12
c ---[1232]---> BDD-cost:   14
c ---[1230]---> BDD-cost:   10
c ---[1229]---> BDD-cost:   10
c ---[1228]---> BDD-cost:   12
c ---[1227]---> BDD-cost:   15
c ---[1226]---> BDD-cost:   14
c ---[1224]---> BDD-cost:   14
c ---[1218]---> BDD-cost:   15
c ---[1216]---> BDD-cost:   17
c ---[1215]---> BDD-cost:   18
c ---[1214]---> BDD-cost:   16
c ---[1213]---> BDD-cost:   15
c ---[1212]---> BDD-cost:   17
c ---[1211]---> BDD-cost:   16
c ---[1210]---> BDD-cost:   14
c ---[1209]---> BDD-cost:   15
c ---[1207]---> BDD-cost:   15
c ---[1206]---> BDD-cost:   18
c ---[1205]---> BDD-cost:    9
c ---[1204]---> BDD-cost:   12
c ---[1203]---> BDD-cost:   13
c ---[1202]---> BDD-cost:   11
c ---[1201]---> BDD-cost:   15
c ---[1200]---> BDD-cost:   12
c ---[1199]---> BDD-cost:   11
c ---[1198]---> BDD-cost:   13
c ---[1197]---> BDD-cost:   13
c ---[1196]---> BDD-cost:   12
c ---[1195]---> BDD-cost:   13
c ---[1194]---> BDD-cost:   15
c ---[1191]---> BDD-cost:   13
c ---[1190]---> BDD-cost:   14
c ---[1189]---> BDD-cost:   12
c ---[1188]---> BDD-cost:   13
c ---[1187]---> BDD-cost:   13
c ---[1185]---> BDD-cost:   10
c ---[1184]---> BDD-cost:   13
c ---[1182]---> BDD-cost:   14
c ---[1181]---> BDD-cost:   14
c ---[1180]---> BDD-cost:   12
c ---[1178]---> BDD-cost:    6
c ---[1177]---> BDD-cost:    7
c ---[1175]---> BDD-cost:   12
c ---[1173]---> BDD-cost:   12
c ---[1172]---> BDD-cost:   19
c ---[1171]---> BDD-cost:   18
c ---[1170]---> BDD-cost:   18
c ---[1169]---> BDD-cost:   12
c ---[1168]---> BDD-cost:   10
c ---[1165]---> BDD-cost:    9
c ---[1161]---> BDD-cost:   16
c ---[1160]---> BDD-cost:   11
c ---[1157]---> BDD-cost:   10
c ---[1156]---> BDD-cost:    9
c ---[1155]---> BDD-cost:   10
c ---[1154]---> BDD-cost:   12
c ---[1149]---> BDD-cost:   11
c ---[1148]---> BDD-cost:   14
c ---[1147]---> BDD-cost:   18
c ---[1145]---> BDD-cost:   12
c ---[1144]---> BDD-cost:   15
c ---[1143]---> BDD-cost:   11
c ---[1142]---> BDD-cost:   17
c ---[1141]---> BDD-cost:   12
c ---[1140]---> BDD-cost:   10
c ---[1139]---> BDD-cost:   11
c ---[1138]---> BDD-cost:   12
c ---[1137]---> BDD-cost:   13
c ---[1135]---> BDD-cost:   15
c ---[1134]---> BDD-cost:   14
c ---[1133]---> BDD-cost:   19
c ---[1132]---> BDD-cost:   13
c ---[1131]---> BDD-cost:   14
c ---[1130]---> BDD-cost:   13
c ---[1128]---> BDD-cost:   13
c ---[1127]---> BDD-cost:   10
c ---[1125]---> BDD-cost:   17
c ---[1124]---> BDD-cost:   15
c ---[1123]---> BDD-cost:   13
c ---[1122]---> BDD-cost:   12
c ---[1121]---> BDD-cost:   10
c ---[1120]---> BDD-cost:   13
c ---[1117]---> BDD-cost:   12
c ---[1116]---> BDD-cost:   12
c ---[1115]---> BDD-cost:   14
c ---[1114]---> BDD-cost:   13
c ---[1112]---> BDD-cost:   12
c ---[1111]---> BDD-cost:   13
c ---[1110]---> BDD-cost:   13
c ---[1109]---> BDD-cost:   11
c ---[1108]---> BDD-cost:   15
c ---[1107]---> BDD-cost:   13
c ---[1106]---> BDD-cost:   15
c ---[1105]---> BDD-cost:   12
c ---[1104]---> BDD-cost:   11
c ---[1103]---> BDD-cost:    9
c ---[1102]---> BDD-cost:   12
c ---[1101]---> BDD-cost:   14
c ---[1100]---> BDD-cost:   13
c ---[1099]---> BDD-cost:   15
c ---[1098]---> BDD-cost:   14
c ---[1096]---> BDD-cost:   13
c ---[1094]---> BDD-cost:   11
c ---[1092]---> BDD-cost:   14
c ---[1090]---> BDD-cost:   14
c ---[1088]---> BDD-cost:    9
c ---[1086]---> BDD-cost:   13
c ---[1085]---> BDD-cost:    7
c ---[1084]---> BDD-cost:   11
c ---[1083]---> BDD-cost:   12
c ---[1081]---> BDD-cost:   12
c ---[1080]---> BDD-cost:    6
c ---[1079]---> BDD-cost:   10
c ---[1077]---> BDD-cost:   11
c ---[1076]---> BDD-cost:   15
c ---[1075]---> BDD-cost:   13
c ---[1073]---> BDD-cost:   13
c ---[1071]---> BDD-cost:   10
c ---[1070]---> BDD-cost:    7
c ---[1069]---> BDD-cost:   17
c ---[1068]---> BDD-cost:   18
c ---[1067]---> BDD-cost:   16
c ---[1066]---> BDD-cost:   12
c ---[1065]---> BDD-cost:   18
c ---[1064]---> BDD-cost:   14
c ---[1063]---> BDD-cost:   14
c ---[1062]---> BDD-cost:   17
c ---[1048]---> BDD-cost:   17
c ---[1047]---> BDD-cost:   15
c ---[1046]---> BDD-cost:   15
c ---[1045]---> BDD-cost:   16
c ---[1042]---> BDD-cost:   11
c ---[1041]---> BDD-cost:   16
c ---[1039]---> BDD-cost:   15
c ---[1038]---> BDD-cost:   17
c ---[1037]---> BDD-cost:   15
c ---[1036]---> BDD-cost:   13
c ---[1035]---> BDD-cost:   12
c ---[1034]---> BDD-cost:   12
c ---[1028]---> BDD-cost:    8
c ---[1027]---> BDD-cost:   15
c ---[1026]---> BDD-cost:   12
c ---[1025]---> BDD-cost:   13
c ---[1024]---> BDD-cost:   16
c ---[1023]---> BDD-cost:   16
c ---[1022]---> BDD-cost:   14
c ---[1021]---> BDD-cost:   14
c ---[1016]---> BDD-cost:   13
c ---[1015]---> BDD-cost:   13
c ---[1014]---> BDD-cost:   14
c ---[1013]---> BDD-cost:   11
c ---[1012]---> BDD-cost:    8
c ---[1008]---> BDD-cost:   13
c ---[1007]---> BDD-cost:   11
c ---[1006]---> BDD-cost:   11
c ---[1005]---> BDD-cost:   13
c ---[ 999]---> BDD-cost:   13
c ---[ 998]---> BDD-cost:   12
c ---[ 997]---> BDD-cost:   14
c ---[ 996]---> BDD-cost:   14
c ---[ 995]---> BDD-cost:   14
c ---[ 994]---> BDD-cost:   18
c ---[ 993]---> BDD-cost:   19
c ---[ 992]---> BDD-cost:   11
c ---[ 991]---> BDD-cost:   16
c ---[ 985]---> Sorter-cost:  295     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 984]---> BDD-cost:   63
c ---[ 983]---> BDD-cost:   58
c ---[ 982]---> BDD-cost:   68
c ---[ 981]---> BDD-cost:   58
c ---[ 980]---> BDD-cost:   73
c ---[ 979]---> BDD-cost:   63
c ---[ 977]---> BDD-cost:  112
c ---[ 975]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 973]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 971]---> Sorter-cost: 1039     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 969]---> Sorter-cost:  485     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 967]---> Adder-cost: 438   maxlim: 630756   bits: 21/20
c ---[ 965]---> Sorter-cost:  771     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 963]---> BDD-cost:  180
c ---[ 961]---> Sorter-cost:  836     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 959]---> Adder-cost: 394   maxlim: 13189095   bits: 25/24
c ---[ 957]---> Sorter-cost: 1499     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 955]---> Sorter-cost: 2907     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 953]---> Sorter-cost: 1456     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 951]---> BDD-cost:  180
c ---[ 949]---> BDD-cost:  176
c ---[ 947]---> Sorter-cost: 2763     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 945]---> BDD-cost:  194
c ---[ 943]---> Adder-cost: 290   maxlim: 221175   bits: 19/18
c ---[ 941]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 939]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 937]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 935]---> Adder-cost: 308   maxlim: 212978   bits: 19/18
c ---[ 933]---> Adder-cost: 690   maxlim: 11435964   bits: 25/24
c ---[ 931]---> Adder-cost: 574   maxlim: 11042750   bits: 25/24
c ---[ 929]---> Adder-cost: 428   maxlim: 11042750   bits: 25/24
c ---[ 927]---> Adder-cost: 1000   maxlim: 75267630   bits: 28/27
c ---[ 925]---> Adder-cost: 622   maxlim: 75267630   bits: 28/27
c ---[ 923]---> Adder-cost: 379   maxlim: 1867758   bits: 22/21
c ---[ 921]---> Adder-cost: 576   maxlim: 10944429   bits: 25/24
c ---[ 919]---> Adder-cost: 488   maxlim: 10944429   bits: 25/24
c ---[ 917]---> Adder-cost: 372   maxlim: 9502666   bits: 25/24
c ---[ 915]---> Adder-cost: 666   maxlim: 1277895   bits: 22/21
c ---[ 913]---> Adder-cost: 672   maxlim: 1298372   bits: 22/21
c ---[ 911]---> Adder-cost: 289   maxlim: 229360   bits: 19/18
c ---[ 909]---> Adder-cost: 357   maxlim: 3243968   bits: 23/22
c ---[ 907]---> BDD-cost:  184
c ---[ 905]---> Adder-cost: 248   maxlim: 1621984   bits: 22/21
c ---[ 903]---> Sorter-cost: 3144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 901]---> Adder-cost: 248   maxlim: 1621984   bits: 22/21
c ---[ 899]---> Sorter-cost:  892     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 897]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 895]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 893]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 891]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 889]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 887]---> Adder-cost: 571   maxlim: 937938   bits: 21/20
c ---[ 885]---> Adder-cost: 312   maxlim: 630756   bits: 21/20
c ---[ 883]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 881]---> BDD-cost:  157
c ---[ 879]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 877]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 875]---> Sorter-cost: 1796     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 873]---> Adder-cost: 297   maxlim: 483299   bits: 20/19
c ---[ 871]---> Adder-cost: 1024   maxlim: 3616609   bits: 23/22
c ---[ 869]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 867]---> BDD-cost:  178
c ---[ 865]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 863]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 861]---> Sorter-cost: 2894     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 859]---> BDD-cost:  191
c ---[ 857]---> BDD-cost:  185
c ---[ 855]---> Sorter-cost: 1076     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 853]---> Adder-cost: 323   maxlim: 491490   bits: 20/19
c ---[ 851]---> Adder-cost: 763   maxlim: 946134   bits: 21/20
c ---[ 849]---> Adder-cost: 589   maxlim: 937947   bits: 21/20
c ---[ 847]---> Adder-cost: 463   maxlim: 946134   bits: 21/20
c ---[ 845]---> Adder-cost: 896   maxlim: 2404242   bits: 23/22
c ---[ 843]---> Adder-cost: 564   maxlim: 2404242   bits: 23/22
c ---[ 841]---> Adder-cost: 747   maxlim: 2002861   bits: 22/21
c ---[ 839]---> BDD-cost:  171
c ---[ 837]---> Adder-cost: 799   maxlim: 3952477   bits: 23/22
c ---[ 835]---> BDD-cost:  180
c ---[ 833]---> Adder-cost: 319   maxlim: 315378   bits: 20/19
c ---[ 831]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 829]---> Sorter-cost: 1639     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 827]---> Sorter-cost: 2256     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 825]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 823]---> Adder-cost: 574   maxlim: 5406679   bits: 24/23
c ---[ 821]---> Adder-cost: 336   maxlim: 4358094   bits: 24/23
c ---[ 819]---> Adder-cost: 417   maxlim: 3932115   bits: 23/22
c ---[ 817]---> Adder-cost: 366   maxlim: 5210052   bits: 24/23
c ---[ 815]---> Adder-cost: 300   maxlim: 3932115   bits: 23/22
c ---[ 813]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 811]---> Adder-cost: 316   maxlim: 2523024   bits: 23/22
c ---[ 809]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 807]---> Sorter-cost: 2419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 805]---> BDD-cost:  144
c ---[ 803]---> Sorter-cost: 2290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 801]---> Sorter-cost: 2382     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 799]---> Adder-cost: 428   maxlim: 589803   bits: 21/20
c ---[ 797]---> Sorter-cost: 2382     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 795]---> Sorter-cost: 2303     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 793]---> BDD-cost:  170
c ---[ 791]---> Adder-cost: 284   maxlim: 589803   bits: 21/20
c ---[ 789]---> BDD-cost:  162
c ---[ 787]---> Sorter-cost: 1911     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 785]---> Sorter-cost: 2309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 783]---> Sorter-cost: 2309     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 781]---> Sorter-cost: 2303     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 779]---> Sorter-cost: 2378     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 777]---> Sorter-cost: 2391     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 775]---> Adder-cost: 474   maxlim: 1376207   bits: 22/21
c ---[ 773]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 771]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 769]---> Adder-cost: 348   maxlim: 348145   bits: 20/19
c ---[ 767]---> Sorter-cost: 1522     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 765]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 763]---> Adder-cost: 264   maxlim: 294901   bits: 20/19
c ---[ 761]---> Adder-cost: 440   maxlim: 860142   bits: 21/20
c ---[ 759]---> Adder-cost: 312   maxlim: 630756   bits: 21/20
c ---[ 757]---> Adder-cost: 936   maxlim: 3665754   bits: 23/22
c ---[ 755]---> Adder-cost: 558   maxlim: 3350376   bits: 23/22
c ---[ 753]---> Adder-cost: 1460   maxlim: 22264803   bits: 26/25
c ---[ 751]---> Adder-cost: 1416   maxlim: 32160271   bits: 26/25
c ---[ 749]---> Adder-cost: 508   maxlim: 2408335   bits: 23/22
c ---[ 747]---> Adder-cost: 870   maxlim: 2297747   bits: 23/22
c ---[ 745]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 743]---> BDD-cost:  136
c ---[ 741]---> Adder-cost: 988   maxlim: 6663881   bits: 24/23
c ---[ 739]---> Adder-cost: 1102   maxlim: 4853526   bits: 24/23
c ---[ 737]---> Adder-cost: 624   maxlim: 4853526   bits: 24/23
c ---[ 735]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 733]---> Adder-cost: 588   maxlim: 2219934   bits: 23/22
c ---[ 731]---> Adder-cost: 269   maxlim: 241654   bits: 19/18
c ---[ 729]---> Adder-cost: 453   maxlim: 954326   bits: 21/20
c ---[ 727]---> Adder-cost: 540   maxlim: 622557   bits: 21/20
c ---[ 725]---> Adder-cost: 322   maxlim: 298995   bits: 20/19
c ---[ 723]---> Adder-cost: 376   maxlim: 1269690   bits: 22/21
c ---[ 721]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 719]---> Adder-cost: 550   maxlim: 851920   bits: 21/20
c ---[ 717]---> Adder-cost: 1144   maxlim: 9559638   bits: 25/24
c ---[ 715]---> Adder-cost: 264   maxlim: 294901   bits: 20/19
c ---[ 713]---> Adder-cost: 492   maxlim: 565220   bits: 21/20
c ---[ 711]---> Adder-cost: 643   maxlim: 1900460   bits: 22/21
c ---[ 709]---> Adder-cost: 522   maxlim: 827354   bits: 21/20
c ---[ 707]---> Adder-cost: 350   maxlim: 401390   bits: 20/19
c ---[ 705]---> Adder-cost: 311   maxlim: 229364   bits: 19/18
c ---[ 703]---> Adder-cost: 650   maxlim: 1617842   bits: 22/21
c ---[ 701]---> Adder-cost: 306   maxlim: 458729   bits: 20/19
c ---[ 699]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 697]---> Adder-cost: 211   maxlim: 241654   bits: 19/18
c ---[ 695]---> Sorter-cost: 1639     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 693]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 691]---> BDD-cost:  153
c ---[ 689]---> Sorter-cost:  669     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 687]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 685]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 683]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 681]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 679]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 677]---> Adder-cost: 264   maxlim: 294901   bits: 20/19
c ---[ 675]---> Adder-cost: 268   maxlim: 303092   bits: 20/19
c ---[ 673]---> Adder-cost: 264   maxlim: 294901   bits: 20/19
c ---[ 671]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 669]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 667]---> Adder-cost: 202   maxlim: 151542   bits: 19/18
c ---[ 665]---> Sorter-cost:  451     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 663]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 661]---> Sorter-cost:  523     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 659]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 657]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 655]---> Sorter-cost:  805     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Adder-cost: 312   maxlim: 630756   bits: 21/20
c ---[ 651]---> Sorter-cost: 2035     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> BDD-cost:  166
c ---[ 647]---> Adder-cost: 314   maxlim: 630756   bits: 21/20
c ---[ 645]---> Sorter-cost: 1649     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 643]---> Sorter-cost: 1649     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 639]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 637]---> Sorter-cost: 1639     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost: 1465     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 631]---> Sorter-cost: 1456     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 629]---> Sorter-cost: 1481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 627]---> Sorter-cost: 1332     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 625]---> Sorter-cost: 1805     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> BDD-cost:  139
c ---[ 621]---> Adder-cost: 773   maxlim: 1978278   bits: 22/21
c ---[ 619]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 617]---> BDD-cost:  153
c ---[ 615]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 613]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 611]---> Sorter-cost: 1626     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Adder-cost: 432   maxlim: 679905   bits: 21/20
c ---[ 607]---> Adder-cost: 464   maxlim: 1617842   bits: 22/21
c ---[ 605]---> Adder-cost: 228   maxlim: 176120   bits: 19/18
c ---[ 603]---> Adder-cost: 230   maxlim: 135159   bits: 19/18
c ---[ 601]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 599]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 597]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 595]---> Sorter-cost: 1626     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 593]---> Adder-cost: 564   maxlim: 2404242   bits: 23/22
c ---[ 591]---> BDD-cost:  184
c ---[ 589]---> Adder-cost: 208   maxlim: 217080   bits: 19/18
c ---[ 587]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 585]---> BDD-cost:  144
c ---[ 583]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 581]---> BDD-cost:  137
c ---[ 577]---> Sorter-cost: 1517     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 573]---> Adder-cost: 282   maxlim: 204787   bits: 19/18
c ---[ 571]---> BDD-cost:  154
c ---[ 569]---> Adder-cost: 208   maxlim: 217080   bits: 19/18
c ---[ 567]---> Adder-cost: 342   maxlim: 651240   bits: 21/20
c ---[ 565]---> Adder-cost: 398   maxlim: 1085400   bits: 22/21
c ---[ 563]---> Sorter-cost: 2902     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 561]---> BDD-cost:  148
c ---[ 559]---> Sorter-cost: 2580     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 557]---> Sorter-cost: 2595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 555]---> Sorter-cost: 2466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 553]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Sorter-cost: 2466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost: 2399     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 543]---> Sorter-cost: 2466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 541]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 539]---> Sorter-cost: 1853     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 537]---> BDD-cost:  140
c ---[ 535]---> BDD-cost:  144
c ---[ 533]---> Sorter-cost: 2604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 531]---> Sorter-cost: 2597     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 529]---> BDD-cost:  162
c ---[ 527]---> Sorter-cost: 1837     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 525]---> Sorter-cost: 3432     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 523]---> Adder-cost: 278   maxlim: 397296   bits: 20/19
c ---[ 521]---> Adder-cost: 357   maxlim: 815073   bits: 21/20
c ---[ 519]---> Sorter-cost: 1776     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Adder-cost: 268   maxlim: 434160   bits: 20/19
c ---[ 515]---> Sorter-cost: 1626     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 513]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 511]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 509]---> Sorter-cost:  481     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 505]---> Adder-cost: 312   maxlim: 651240   bits: 21/20
c ---[ 503]---> Sorter-cost: 1818     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 501]---> Sorter-cost: 2466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 499]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost: 1399     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost: 2347     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Adder-cost: 533   maxlim: 1855383   bits: 22/21
c ---[ 489]---> Adder-cost: 343   maxlim: 1765273   bits: 22/21
c ---[ 487]---> Adder-cost: 424   maxlim: 675801   bits: 21/20
c ---[ 485]---> Sorter-cost: 1388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Adder-cost: 637   maxlim: 1978257   bits: 22/21
c ---[ 481]---> Sorter-cost: 2160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> BDD-cost:  139
c ---[ 477]---> Sorter-cost:  556     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost:  605     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost: 1132     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> BDD-cost:  135
c ---[ 469]---> Sorter-cost: 2466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> BDD-cost:  134
c ---[ 465]---> Sorter-cost: 1742     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 463]---> Sorter-cost: 1772     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Sorter-cost: 1439     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost: 2466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Adder-cost: 392   maxlim: 1490858   bits: 22/21
c ---[ 451]---> Adder-cost: 406   maxlim: 1216443   bits: 22/21
c ---[ 449]---> Adder-cost: 375   maxlim: 634841   bits: 21/20
c ---[ 447]---> Adder-cost: 325   maxlim: 622558   bits: 21/20
c ---[ 445]---> Adder-cost: 313   maxlim: 421865   bits: 20/19
c ---[ 443]---> Adder-cost: 330   maxlim: 1187770   bits: 22/21
c ---[ 441]---> Adder-cost: 486   maxlim: 1470379   bits: 22/21
c ---[ 439]---> Adder-cost: 508   maxlim: 1503149   bits: 22/21
c ---[ 437]---> Adder-cost: 326   maxlim: 1839001   bits: 22/21
c ---[ 435]---> Adder-cost: 688   maxlim: 2338712   bits: 23/22
c ---[ 433]---> Adder-cost: 775   maxlim: 2064295   bits: 22/21
c ---[ 431]---> Sorter-cost: 1193     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost:  527     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost:  903     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost:  941     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 423]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> Sorter-cost: 2179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 419]---> Sorter-cost: 2138     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 417]---> Sorter-cost:  542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> Sorter-cost: 1103     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 413]---> Sorter-cost: 1103     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 411]---> Sorter-cost: 1150     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> Sorter-cost: 2475     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> Sorter-cost:  532     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> Sorter-cost: 2597     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 399]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 397]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 395]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 393]---> Sorter-cost: 1439     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 389]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 387]---> BDD-cost:  153
c ---[ 385]---> Sorter-cost: 1467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 383]---> BDD-cost:  109
c ---[ 381]---> BDD-cost:  112
c ---[ 379]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> BDD-cost:  125
c ---[ 375]---> Sorter-cost:  825     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> BDD-cost:  126
c ---[ 371]---> Sorter-cost: 1918     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 369]---> Adder-cost: 631   maxlim: 1662901   bits: 22/21
c ---[ 367]---> Adder-cost: 685   maxlim: 1654711   bits: 22/21
c ---[ 365]---> Sorter-cost: 2303     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 363]---> BDD-cost:  110
c ---[ 361]---> BDD-cost:  104
c ---[ 359]---> BDD-cost:  112
c ---[ 357]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 355]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 353]---> BDD-cost:  114
c ---[ 351]---> Sorter-cost:  565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> BDD-cost:  126
c ---[ 345]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> Sorter-cost: 2303     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 339]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 337]---> Sorter-cost:12307     Base: 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 335]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 333]---> Adder-cost: 270   maxlim: 278517   bits: 20/19
c ---[ 331]---> Adder-cost: 488   maxlim: 868314   bits: 21/20
c ---[ 329]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 327]---> Adder-cost: 319   maxlim: 315378   bits: 20/19
c ---[ 325]---> Sorter-cost: 3287     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 323]---> Sorter-cost:  565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 321]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 317]---> Adder-cost: 532   maxlim: 15809908   bits: 25/24
c ---[ 315]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 313]---> Sorter-cost: 1621     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost: 1615     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> Adder-cost: 523   maxlim: 3952477   bits: 23/22
c ---[ 307]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> Sorter-cost: 2466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Adder-cost: 217   maxlim: 249847   bits: 19/18
c ---[ 299]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Sorter-cost:  654     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 295]---> Adder-cost: 820   maxlim: 2379666   bits: 23/22
c ---[ 293]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 291]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 289]---> Sorter-cost: 1610     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 287]---> Sorter-cost: 1350     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 285]---> Sorter-cost: 1103     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 281]---> Sorter-cost: 1103     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 279]---> Sorter-cost: 1103     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 277]---> Sorter-cost: 2217     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 275]---> Sorter-cost: 2179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 273]---> Adder-cost: 226   maxlim: 159735   bits: 19/18
c ---[ 271]---> BDD-cost:  148
c ---[ 269]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 267]---> Sorter-cost: 1639     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 265]---> Sorter-cost:  540     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 263]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 261]---> Sorter-cost: 1639     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 259]---> Sorter-cost: 2466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 257]---> Sorter-cost: 2179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> Sorter-cost: 1350     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost:  508     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost: 1626     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost: 2574     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost: 1639     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost: 2466     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 241]---> Sorter-cost:  638     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 239]---> Sorter-cost:  627     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> Sorter-cost: 1673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost: 2376     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 233]---> BDD-cost:  139
c ---[ 231]---> BDD-cost:  114
c ---[ 229]---> BDD-cost:  110
c ---[ 227]---> Sorter-cost: 2303     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 225]---> Sorter-cost: 1151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost:  589     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> BDD-cost:  131
c ---[ 219]---> Sorter-cost: 1060     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost: 1350     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> BDD-cost:  112
c ---[ 211]---> Sorter-cost: 2179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 205]---> BDD-cost:  149
c ---[ 203]---> BDD-cost:  153
c ---[ 201]---> Sorter-cost:  499     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> BDD-cost:  100
c ---[ 197]---> Adder-cost: 564   maxlim: 2404242   bits: 23/22
c ---[ 195]---> BDD-cost:  180
c ---[ 193]---> BDD-cost:  180
c ---[ 191]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Adder-cost: 476   maxlim: 3350376   bits: 23/22
c ---[ 187]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 185]---> Adder-cost: 319   maxlim: 315378   bits: 20/19
c ---[ 183]---> Adder-cost: 319   maxlim: 315378   bits: 20/19
c ---[ 181]---> Sorter-cost:  754     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost: 2179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1077     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Adder-cost: 812   maxlim: 19782745   bits: 26/25
c ---[ 171]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 167]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 165]---> Adder-cost: 314   maxlim: 315378   bits: 20/19
c ---[ 163]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 161]---> BDD-cost:  152
c ---[ 157]---> BDD-cost:  157
c ---[ 155]---> BDD-cost:  161
c ---[ 153]---> BDD-cost:  157
c ---[ 151]---> Sorter-cost: 2239     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost:  884     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 145]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Adder-cost: 314   maxlim: 630756   bits: 21/20
c ---[ 139]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> BDD-cost:  153
c ---[ 135]---> Adder-cost: 259   maxlim: 253936   bits: 19/18
c ---[ 133]---> Adder-cost: 269   maxlim: 233462   bits: 19/18
c ---[ 131]---> Adder-cost: 523   maxlim: 3952477   bits: 23/22
c ---[ 129]---> Adder-cost: 606   maxlim: 2441111   bits: 23/22
c ---[ 127]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 125]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[ 123]---> Sorter-cost: 1639     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 121]---> Sorter-cost: 1639     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost: 1060     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost:  518     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  489     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost:  893     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost: 1138     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost: 3209     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[  99]---> Adder-cost: 312   maxlim: 315378   bits: 20/19
c ---[  97]---> Sorter-cost: 2578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> BDD-cost:  148
c ---[  93]---> Sorter-cost:  771     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Adder-cost: 529   maxlim: 15809908   bits: 25/24
c ---[  89]---> Sorter-cost: 2160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Adder-cost: 312   maxlim: 1425399   bits: 22/21
c ---[  79]---> Adder-cost: 342   maxlim: 255984   bits: 19/18
c ---[  76]---> BDD-cost:   38
c ---[  75]---> BDD-cost:   44
c ---[  73]---> BDD-cost:   47
c ---[  72]---> BDD-cost:   43
c ---[  71]---> Sorter-cost: 1367     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    9
c ---[  68]---> BDD-cost:   14
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   12
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   13
c ---[  63]---> BDD-cost:   16
c ---[  62]---> BDD-cost:   14
c ---[  61]---> BDD-cost:   16
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   11
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   10
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   12
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:   10
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:    9
c ---[  40]---> BDD-cost:    5
c ---[  39]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   12
c ---[  33]---> BDD-cost:   12
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:    6
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:    6
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:   12
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   17
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:    6
c ---[  11]---> BDD-cost:    7
c ---[  10]---> BDD-cost:   11
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:    8
c ---[   7]---> BDD-cost:    8
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:    8
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:  104
c ---[   1]---> BDD-cost:   35
c ---[   0]---> BDD-cost:   32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1380421  3915776 |  460140       0        0     nan |  0.000 % |
c |       100 | 1379860  3914524 |  506154      98      520     5.3 |  6.468 % |
c |       250 | 1379860  3914524 |  556769     248     1235     5.0 |  6.468 % |
c |       475 | 1379858  3914520 |  612446     472     2616     5.5 |  6.468 % |
c |       812 | 1379802  3914396 |  673690     797     4172     5.2 |  6.472 % |
c |      1318 | 1374309  3901930 |  741060    1269     7253     5.7 |  6.835 % |
c |      2077 | 1372944  3898833 |  815166    1984    12268     6.2 |  6.926 % |
c |      3216 | 1372699  3898273 |  896682    3118    23460     7.5 |  6.943 % |
c |      4924 | 1372683  3898237 |  986350    4824    49805    10.3 |  6.944 % |
c |      7488 | 1372563  3897968 | 1084986    7384    86865    11.8 |  6.952 % |
c |     11333 | 1372549  3897937 | 1193484   11227   188541    16.8 |  6.953 % |
c |     17102 | 1372549  3897937 | 1312833   16996   382799    22.5 |  6.953 % |
c |     25751 | 1372539  3897915 | 1444116   25640   700797    27.3 |  6.954 % |
c |     38725 | 1372539  3897915 | 1588528   38614  1550487    40.2 |  6.954 % |
c |     58186 | 1371650  3895931 | 1747380   58058  2822182    48.6 |  7.008 % |
/oldhome/oroussel/solvers/minisat+_script: line 16:  3634 CPU time limit exceeded $XDIR/minisat+_bignum_static* "$@"
#### 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.91 0.98 0.97 2/54 3629
Raw data (stat): 3629 (runsolver) R 3628 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841011127 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0006 s]
Raw data (loadavg): 0.93 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+40.0018 s]
Raw data (loadavg): 0.95 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+90.003 s]
Raw data (loadavg): 0.98 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+140.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+150.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+160.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+170.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+180.014 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+190.014 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+200.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+210.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+220.014 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+230.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+240.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+250.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+260.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+270.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+280.016 s]
Raw data (loadavg): 1.07 1.00 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+290.016 s]
Raw data (loadavg): 1.06 1.00 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+300.017 s]
Raw data (loadavg): 1.05 1.00 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+310.018 s]
Raw data (loadavg): 1.04 1.00 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+320.019 s]
Raw data (loadavg): 1.03 1.00 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+330.02 s]
Raw data (loadavg): 1.03 1.00 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+340.02 s]
Raw data (loadavg): 1.02 1.00 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+350.02 s]
Raw data (loadavg): 1.02 1.00 0.97 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+360.021 s]
Raw data (loadavg): 1.10 1.01 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+370.021 s]
Raw data (loadavg): 1.08 1.01 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+380.022 s]
Raw data (loadavg): 1.07 1.01 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+390.025 s]
Raw data (loadavg): 1.06 1.01 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+400.025 s]
Raw data (loadavg): 1.05 1.01 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+410.025 s]
Raw data (loadavg): 1.04 1.01 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+420.03 s]
Raw data (loadavg): 1.03 1.01 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+430.133 s]
Raw data (loadavg): 1.09 1.02 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+440.133 s]
Raw data (loadavg): 1.08 1.02 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+450.133 s]
Raw data (loadavg): 1.07 1.02 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+460.134 s]
Raw data (loadavg): 1.06 1.02 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+470.134 s]
Raw data (loadavg): 1.05 1.02 0.98 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+480.135 s]
Raw data (loadavg): 1.11 1.03 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+490.135 s]
Raw data (loadavg): 1.09 1.03 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+500.136 s]
Raw data (loadavg): 1.08 1.03 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+510.136 s]
Raw data (loadavg): 1.07 1.03 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+520.135 s]
Raw data (loadavg): 1.06 1.03 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+530.135 s]
Raw data (loadavg): 1.05 1.03 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+540.135 s]
Raw data (loadavg): 1.04 1.03 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+550.135 s]
Raw data (loadavg): 1.03 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+560.136 s]
Raw data (loadavg): 1.03 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+570.136 s]
Raw data (loadavg): 1.02 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+580.135 s]
Raw data (loadavg): 1.02 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+590.135 s]
Raw data (loadavg): 1.02 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+600.135 s]
Raw data (loadavg): 1.01 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+610.136 s]
Raw data (loadavg): 1.01 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+620.135 s]
Raw data (loadavg): 1.01 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+630.135 s]
Raw data (loadavg): 1.01 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+640.136 s]
Raw data (loadavg): 1.00 1.02 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+650.136 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+660.136 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+670.137 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+680.136 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+690.136 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+700.136 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+710.136 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+720.136 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+730.136 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+740.137 s]
Raw data (loadavg): 1.00 1.01 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+750.137 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+760.137 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+770.137 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+780.137 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+790.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+800.137 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+810.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+820.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+830.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+840.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+850.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+860.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+870.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+880.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+890.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+900.138 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+910.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+920.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+930.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+940.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+950.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+960.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+970.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+980.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+990.139 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1000.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1010.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1020.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1030.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1040.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1050.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1060.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1070.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1080.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1090.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1100.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1110.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1120.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1130.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1140.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1150.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1160.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1170.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1180.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1190.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1210.15 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1220.15 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1230.15 s]
Raw data (loadavg): 1.00 1.00 0.99 2/55 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1230.36 s]
Raw data (loadavg): 1.00 1.00 0.99 1/53 3634
Raw data (stat): 3629 (minisat+_script) S 3628 20001 20000 0 -1 0 300 333 0 0 0 0 0 1 20 0 1 0 841011127 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 0

Child status: 152
Real time (s): 1230.36
CPU time (s): 1229.92
CPU user time (s): 1228.78
CPU system time (s): 1.14383
CPU usage (%): 99.964
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####