PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-seba.opb
MD5SUM	4a697c297ecbc7d83b192d907b1ba64c
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	5999
Biggest coefficient in the objective function	252287385600
Number of bits for the biggest coefficient in the objective function	38
Sum of the numbers in the objective function	4556926949351
Number of bits of the sum of numbers in the objective function	43
Biggest number in a constraint	252287385600
Number of bits of the biggest number in a constraint	38
Biggest sum of numbers in a constraint	4556926949351
Number of bits of the biggest sum of numbers	43
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.150976
Number of variables	16645
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	7
Maximum length of a constraint	333
Trace number 31059

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-05-25 21:39:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22442 boxname=wulflinc17 idbench=1258 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  4a697c297ecbc7d83b192d907b1ba64c  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-seba.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-seba.opb
IDLAUNCH: 22442
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        882860 kB
Buffers:         23916 kB
Cached:         105208 kB
SwapCached:        484 kB
Active:          20264 kB
Inactive:       110936 kB
HighTotal:      131008 kB
HighFree:        25088 kB
LowTotal:       903652 kB
LowFree:        857772 kB
SwapTotal:     2097892 kB
SwapFree:      2096560 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            14876 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 22:00:10 (client local time) WITH STATUS 152 IN 1229.9 SECONDS
stats: 22442 7 1229.9 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1420 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1490]---> BDD-cost:    8
c ---[1489]---> BDD-cost:    7
c ---[1488]---> BDD-cost:    9
c ---[1487]---> BDD-cost:   12
c ---[1485]---> BDD-cost:    8
c ---[1484]---> BDD-cost:    6
c ---[1482]---> BDD-cost:   13
c ---[1481]---> BDD-cost:   14
c ---[1480]---> BDD-cost:   15
c ---[1479]---> BDD-cost:   14
c ---[1478]---> BDD-cost:   14
c ---[1477]---> BDD-cost:   14
c ---[1476]---> BDD-cost:   14
c ---[1475]---> BDD-cost:   15
c ---[1474]---> BDD-cost:   14
c ---[1473]---> BDD-cost:   15
c ---[1472]---> BDD-cost:   16
c ---[1471]---> BDD-cost:   10
c ---[1470]---> BDD-cost:   12
c ---[1469]---> BDD-cost:   11
c ---[1468]---> BDD-cost:    9
c ---[1466]---> BDD-cost:   12
c ---[1465]---> BDD-cost:   15
c ---[1464]---> BDD-cost:   14
c ---[1463]---> BDD-cost:   16
c ---[1462]---> BDD-cost:   16
c ---[1461]---> BDD-cost:   14
c ---[1460]---> BDD-cost:   10
c ---[1458]---> BDD-cost:   16
c ---[1457]---> BDD-cost:   13
c ---[1456]---> BDD-cost:   13
c ---[1455]---> BDD-cost:   10
c ---[1454]---> BDD-cost:   14
c ---[1453]---> BDD-cost:   14
c ---[1452]---> BDD-cost:   13
c ---[1450]---> BDD-cost:   14
c ---[1449]---> BDD-cost:   10
c ---[1448]---> BDD-cost:   12
c ---[1447]---> BDD-cost:   12
c ---[1446]---> BDD-cost:   11
c ---[1444]---> BDD-cost:    9
c ---[1442]---> BDD-cost:   13
c ---[1441]---> BDD-cost:    8
c ---[1440]---> BDD-cost:   12
c ---[1439]---> BDD-cost:    9
c ---[1438]---> BDD-cost:    9
c ---[1437]---> BDD-cost:    9
c ---[1436]---> BDD-cost:   12
c ---[1431]---> BDD-cost:   13
c ---[1430]---> BDD-cost:   12
c ---[1428]---> BDD-cost:   15
c ---[1427]---> BDD-cost:   16
c ---[1426]---> BDD-cost:   13
c ---[1424]---> BDD-cost:    4
c ---[1423]---> BDD-cost:   13
c ---[1422]---> BDD-cost:   12
c ---[1421]---> BDD-cost:   13
c ---[1420]---> BDD-cost:   13
c ---[1419]---> BDD-cost:   11
c ---[1418]---> BDD-cost:   15
c ---[1417]---> BDD-cost:   12
c ---[1416]---> BDD-cost:   14
c ---[1415]---> BDD-cost:   15
c ---[1414]---> BDD-cost:   14
c ---[1413]---> BDD-cost:   14
c ---[1412]---> BDD-cost:    9
c ---[1411]---> BDD-cost:    9
c ---[1410]---> BDD-cost:   14
c ---[1409]---> BDD-cost:   10
c ---[1405]---> BDD-cost:   15
c ---[1404]---> BDD-cost:   14
c ---[1403]---> BDD-cost:   10
c ---[1402]---> BDD-cost:   15
c ---[1400]---> BDD-cost:   11
c ---[1399]---> BDD-cost:   10
c ---[1398]---> BDD-cost:   10
c ---[1396]---> BDD-cost:   13
c ---[1395]---> BDD-cost:   11
c ---[1394]---> BDD-cost:   11
c ---[1393]---> BDD-cost:   14
c ---[1392]---> BDD-cost:   14
c ---[1391]---> BDD-cost:   13
c ---[1390]---> BDD-cost:   12
c ---[1389]---> BDD-cost:   11
c ---[1388]---> BDD-cost:   12
c ---[1387]---> BDD-cost:   11
c ---[1386]---> BDD-cost:   11
c ---[1385]---> BDD-cost:    9
c ---[1384]---> BDD-cost:   15
c ---[1383]---> BDD-cost:   11
c ---[1382]---> BDD-cost:   12
c ---[1381]---> BDD-cost:   11
c ---[1380]---> BDD-cost:   14
c ---[1379]---> BDD-cost:    7
c ---[1377]---> BDD-cost:   10
c ---[1376]---> BDD-cost:   13
c ---[1375]---> BDD-cost:   11
c ---[1374]---> BDD-cost:   14
c ---[1373]---> BDD-cost:   11
c ---[1372]---> BDD-cost:   10
c ---[1371]---> BDD-cost:   16
c ---[1370]---> BDD-cost:   15
c ---[1369]---> BDD-cost:   14
c ---[1368]---> BDD-cost:    9
c ---[1364]---> BDD-cost:   13
c ---[1363]---> BDD-cost:   15
c ---[1362]---> BDD-cost:   16
c ---[1361]---> BDD-cost:    9
c ---[1360]---> BDD-cost:   14
c ---[1358]---> BDD-cost:   13
c ---[1357]---> BDD-cost:   13
c ---[1356]---> BDD-cost:   11
c ---[1353]---> BDD-cost:   12
c ---[1351]---> BDD-cost:   11
c ---[1349]---> BDD-cost:   13
c ---[1348]---> BDD-cost:   12
c ---[1347]---> BDD-cost:   10
c ---[1346]---> BDD-cost:   12
c ---[1345]---> BDD-cost:   12
c ---[1342]---> BDD-cost:   11
c ---[1341]---> BDD-cost:    9
c ---[1340]---> BDD-cost:   10
c ---[1339]---> BDD-cost:   12
c ---[1338]---> BDD-cost:   10
c ---[1337]---> BDD-cost:    7
c ---[1336]---> BDD-cost:   10
c ---[1335]---> BDD-cost:   10
c ---[1334]---> BDD-cost:   12
c ---[1333]---> BDD-cost:   13
c ---[1332]---> BDD-cost:   10
c ---[1331]---> BDD-cost:   12
c ---[1330]---> BDD-cost:   11
c ---[1328]---> BDD-cost:   12
c ---[1327]---> BDD-cost:    8
c ---[1326]---> BDD-cost:    7
c ---[1325]---> BDD-cost:   11
c ---[1324]---> BDD-cost:    8
c ---[1323]---> BDD-cost:   10
c ---[1322]---> BDD-cost:   11
c ---[1321]---> BDD-cost:    8
c ---[1320]---> BDD-cost:   12
c ---[1319]---> BDD-cost:   15
c ---[1318]---> BDD-cost:   14
c ---[1316]---> BDD-cost:   10
c ---[1315]---> BDD-cost:    9
c ---[1314]---> BDD-cost:    9
c ---[1313]---> BDD-cost:    7
c ---[1312]---> BDD-cost:   10
c ---[1311]---> BDD-cost:    6
c ---[1310]---> BDD-cost:   14
c ---[1309]---> BDD-cost:   13
c ---[1307]---> BDD-cost:   10
c ---[1305]---> BDD-cost:   11
c ---[1304]---> BDD-cost:   14
c ---[1303]---> BDD-cost:   11
c ---[1302]---> BDD-cost:   11
c ---[1299]---> BDD-cost:   11
c ---[1296]---> BDD-cost:   11
c ---[1295]---> BDD-cost:   12
c ---[1294]---> BDD-cost:   10
c ---[1292]---> BDD-cost:   12
c ---[1289]---> BDD-cost:    9
c ---[1288]---> BDD-cost:   15
c ---[1287]---> BDD-cost:   16
c ---[1286]---> BDD-cost:   10
c ---[1285]---> BDD-cost:   14
c ---[1284]---> BDD-cost:    7
c ---[1283]---> BDD-cost:    8
c ---[1282]---> BDD-cost:    6
c ---[1280]---> BDD-cost:   10
c ---[1279]---> BDD-cost:   11
c ---[1277]---> BDD-cost:   13
c ---[1276]---> BDD-cost:    6
c ---[1275]---> BDD-cost:   12
c ---[1273]---> BDD-cost:   12
c ---[1270]---> BDD-cost:   12
c ---[1269]---> BDD-cost:   12
c ---[1267]---> BDD-cost:   11
c ---[1266]---> BDD-cost:    8
c ---[1265]---> BDD-cost:   12
c ---[1264]---> BDD-cost:    8
c ---[1263]---> BDD-cost:   12
c ---[1261]---> BDD-cost:   11
c ---[1260]---> BDD-cost:   10
c ---[1259]---> BDD-cost:   10
c ---[1258]---> BDD-cost:   13
c ---[1256]---> BDD-cost:   13
c ---[1255]---> BDD-cost:   14
c ---[1254]---> BDD-cost:   15
c ---[1252]---> BDD-cost:   12
c ---[1250]---> BDD-cost:   12
c ---[1248]---> BDD-cost:    6
c ---[1247]---> BDD-cost:    5
c ---[1246]---> BDD-cost:    6
c ---[1245]---> BDD-cost:   10
c ---[1244]---> BDD-cost:   12
c ---[1243]---> BDD-cost:   10
c ---[1242]---> BDD-cost:   10
c ---[1241]---> BDD-cost:   11
c ---[1240]---> BDD-cost:    7
c ---[1239]---> BDD-cost:    9
c ---[1238]---> BDD-cost:    6
c ---[1236]---> BDD-cost:   15
c ---[1235]---> BDD-cost:   12
c ---[1234]---> BDD-cost:    6
c ---[1233]---> BDD-cost:   14
c ---[1232]---> BDD-cost:    9
c ---[1231]---> BDD-cost:   11
c ---[1229]---> BDD-cost:   10
c ---[1228]---> BDD-cost:    9
c ---[1227]---> BDD-cost:   10
c ---[1226]---> BDD-cost:   12
c ---[1225]---> BDD-cost:   10
c ---[1223]---> BDD-cost:   10
c ---[1217]---> BDD-cost:   11
c ---[1215]---> BDD-cost:   14
c ---[1214]---> BDD-cost:   15
c ---[1213]---> BDD-cost:   15
c ---[1212]---> BDD-cost:   15
c ---[1211]---> BDD-cost:   13
c ---[1210]---> BDD-cost:   12
c ---[1209]---> BDD-cost:   14
c ---[1208]---> BDD-cost:   13
c ---[1206]---> BDD-cost:   15
c ---[1205]---> BDD-cost:   14
c ---[1204]---> BDD-cost:    9
c ---[1203]---> BDD-cost:    6
c ---[1202]---> BDD-cost:    6
c ---[1201]---> BDD-cost:   10
c ---[1200]---> BDD-cost:   12
c ---[1199]---> BDD-cost:   10
c ---[1198]---> BDD-cost:    8
c ---[1197]---> BDD-cost:   10
c ---[1196]---> BDD-cost:    9
c ---[1195]---> BDD-cost:   10
c ---[1194]---> BDD-cost:    9
c ---[1193]---> BDD-cost:   12
c ---[1190]---> BDD-cost:   10
c ---[1189]---> BDD-cost:   11
c ---[1188]---> BDD-cost:   10
c ---[1187]---> BDD-cost:   11
c ---[1186]---> BDD-cost:   11
c ---[1184]---> BDD-cost:    8
c ---[1183]---> BDD-cost:    6
c ---[1181]---> BDD-cost:    9
c ---[1180]---> BDD-cost:   11
c ---[1179]---> BDD-cost:   12
c ---[1177]---> BDD-cost:    6
c ---[1176]---> BDD-cost:    7
c ---[1174]---> BDD-cost:   10
c ---[1172]---> BDD-cost:    9
c ---[1171]---> BDD-cost:   15
c ---[1170]---> BDD-cost:   13
c ---[1169]---> BDD-cost:   13
c ---[1168]---> BDD-cost:   11
c ---[1167]---> BDD-cost:    5
c ---[1164]---> BDD-cost:    3
c ---[1160]---> BDD-cost:   12
c ---[1159]---> BDD-cost:    8
c ---[1156]---> BDD-cost:    8
c ---[1155]---> BDD-cost:    9
c ---[1154]---> BDD-cost:    9
c ---[1153]---> BDD-cost:    9
c ---[1148]---> BDD-cost:    8
c ---[1147]---> BDD-cost:   11
c ---[1146]---> BDD-cost:   13
c ---[1144]---> BDD-cost:   10
c ---[1143]---> BDD-cost:   11
c ---[1142]---> BDD-cost:    7
c ---[1141]---> BDD-cost:   12
c ---[1140]---> BDD-cost:   10
c ---[1139]---> BDD-cost:    9
c ---[1138]---> BDD-cost:    6
c ---[1137]---> BDD-cost:    7
c ---[1136]---> BDD-cost:   13
c ---[1134]---> BDD-cost:   11
c ---[1133]---> BDD-cost:    9
c ---[1132]---> BDD-cost:   12
c ---[1131]---> BDD-cost:    9
c ---[1130]---> BDD-cost:   12
c ---[1129]---> BDD-cost:   10
c ---[1127]---> BDD-cost:   10
c ---[1126]---> BDD-cost:    7
c ---[1124]---> BDD-cost:   16
c ---[1123]---> BDD-cost:   12
c ---[1122]---> BDD-cost:   11
c ---[1121]---> BDD-cost:    7
c ---[1120]---> BDD-cost:    8
c ---[1119]---> BDD-cost:   10
c ---[1116]---> BDD-cost:   10
c ---[1115]---> BDD-cost:    8
c ---[1114]---> BDD-cost:   10
c ---[1113]---> BDD-cost:   10
c ---[1111]---> BDD-cost:   12
c ---[1110]---> BDD-cost:    9
c ---[1109]---> BDD-cost:    9
c ---[1108]---> BDD-cost:    6
c ---[1107]---> BDD-cost:   12
c ---[1106]---> BDD-cost:    7
c ---[1105]---> BDD-cost:   12
c ---[1104]---> BDD-cost:   10
c ---[1103]---> BDD-cost:    6
c ---[1102]---> BDD-cost:    7
c ---[1101]---> BDD-cost:    9
c ---[1100]---> BDD-cost:   11
c ---[1099]---> BDD-cost:    8
c ---[1098]---> BDD-cost:   12
c ---[1097]---> BDD-cost:   11
c ---[1095]---> BDD-cost:   11
c ---[1093]---> BDD-cost:   10
c ---[1091]---> BDD-cost:   11
c ---[1089]---> BDD-cost:   11
c ---[1087]---> BDD-cost:    4
c ---[1085]---> BDD-cost:    8
c ---[1084]---> BDD-cost:    7
c ---[1083]---> BDD-cost:    9
c ---[1082]---> BDD-cost:    8
c ---[1080]---> BDD-cost:    7
c ---[1079]---> BDD-cost:    6
c ---[1078]---> BDD-cost:    6
c ---[1076]---> BDD-cost:    9
c ---[1075]---> BDD-cost:   12
c ---[1074]---> BDD-cost:   11
c ---[1072]---> BDD-cost:   12
c ---[1070]---> BDD-cost:    8
c ---[1069]---> BDD-cost:    5
c ---[1068]---> BDD-cost:   12
c ---[1067]---> BDD-cost:   14
c ---[1066]---> BDD-cost:   14
c ---[1065]---> BDD-cost:   11
c ---[1064]---> BDD-cost:   13
c ---[1063]---> BDD-cost:   10
c ---[1062]---> BDD-cost:   14
c ---[1061]---> BDD-cost:   14
c ---[1047]---> BDD-cost:   16
c ---[1046]---> BDD-cost:   12
c ---[1045]---> BDD-cost:   12
c ---[1044]---> BDD-cost:   12
c ---[1041]---> BDD-cost:   11
c ---[1040]---> BDD-cost:   13
c ---[1038]---> BDD-cost:   11
c ---[1037]---> BDD-cost:   14
c ---[1036]---> BDD-cost:   11
c ---[1035]---> BDD-cost:   10
c ---[1034]---> BDD-cost:    6
c ---[1033]---> BDD-cost:   10
c ---[1027]---> BDD-cost:    6
c ---[1026]---> BDD-cost:    8
c ---[1025]---> BDD-cost:   11
c ---[1024]---> BDD-cost:   12
c ---[1023]---> BDD-cost:   15
c ---[1022]---> BDD-cost:   14
c ---[1021]---> BDD-cost:    7
c ---[1020]---> BDD-cost:    8
c ---[1015]---> BDD-cost:    8
c ---[1014]---> BDD-cost:    8
c ---[1013]---> BDD-cost:    9
c ---[1012]---> BDD-cost:    6
c ---[1011]---> BDD-cost:    8
c ---[1007]---> BDD-cost:    9
c ---[1006]---> BDD-cost:    4
c ---[1005]---> BDD-cost:    8
c ---[1004]---> BDD-cost:    9
c ---[ 999]---> BDD-cost:    9
c ---[ 998]---> BDD-cost:    7
c ---[ 997]---> BDD-cost:   12
c ---[ 996]---> BDD-cost:    9
c ---[ 995]---> BDD-cost:   10
c ---[ 994]---> BDD-cost:   15
c ---[ 993]---> BDD-cost:   14
c ---[ 992]---> BDD-cost:    9
c ---[ 991]---> BDD-cost:   12
c ---[ 985]---> Sorter-cost:  226     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 984]---> BDD-cost:   48
c ---[ 983]---> BDD-cost:   43
c ---[ 982]---> BDD-cost:   53
c ---[ 981]---> BDD-cost:   43
c ---[ 980]---> BDD-cost:   58
c ---[ 979]---> BDD-cost:   48
c ---[ 977]---> BDD-cost:   85
c ---[ 975]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 973]---> Sorter-cost: 1134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 971]---> Sorter-cost:  841     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 969]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2
c ---[ 967]---> Adder-cost: 348   maxlim: 78820   bits: 18/17
c ---[ 965]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 963]---> BDD-cost:  148
c ---[ 961]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 959]---> Adder-cost: 328   maxlim: 1648615   bits: 22/21
c ---[ 957]---> Sorter-cost: 1235     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 955]---> Sorter-cost: 2349     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 953]---> Sorter-cost: 1198     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 951]---> BDD-cost:  153
c ---[ 949]---> BDD-cost:  149
c ---[ 947]---> Sorter-cost: 2235     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 945]---> BDD-cost:  162
c ---[ 943]---> Adder-cost: 230   maxlim: 27639   bits: 16/15
c ---[ 941]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 939]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 937]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 935]---> Adder-cost: 242   maxlim: 26610   bits: 16/15
c ---[ 933]---> Adder-cost: 563   maxlim: 1036220   bits: 21/20
c ---[ 931]---> Adder-cost: 471   maxlim: 1003454   bits: 21/20
c ---[ 929]---> Adder-cost: 355   maxlim: 1003454   bits: 21/20
c ---[ 927]---> Adder-cost: 800   maxlim: 6016558   bits: 23/23
c ---[ 925]---> Adder-cost: 504   maxlim: 6016558   bits: 23/23
c ---[ 923]---> Adder-cost: 304   maxlim: 184302   bits: 19/18
c ---[ 921]---> Adder-cost: 464   maxlim: 1040301   bits: 21/20
c ---[ 919]---> Adder-cost: 399   maxlim: 1040301   bits: 21/20
c ---[ 917]---> Adder-cost: 300   maxlim: 860106   bits: 21/20
c ---[ 915]---> Adder-cost: 528   maxlim: 159687   bits: 19/18
c ---[ 913]---> Adder-cost: 528   maxlim: 162244   bits: 19/18
c ---[ 911]---> Adder-cost: 229   maxlim: 28656   bits: 16/15
c ---[ 909]---> Sorter-cost: 3168     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 907]---> BDD-cost:  157
c ---[ 905]---> Sorter-cost: 3037     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 903]---> Sorter-cost: 2476     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 901]---> Sorter-cost: 3059     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 899]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 897]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 895]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 893]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 891]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 889]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 887]---> Adder-cost: 457   maxlim: 117202   bits: 18/17
c ---[ 885]---> Adder-cost: 246   maxlim: 78820   bits: 18/17
c ---[ 883]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 881]---> BDD-cost:  130
c ---[ 879]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 877]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 875]---> Sorter-cost: 1400     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 873]---> Adder-cost: 237   maxlim: 60387   bits: 17/16
c ---[ 871]---> Adder-cost: 808   maxlim: 451937   bits: 20/19
c ---[ 869]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 867]---> BDD-cost:  146
c ---[ 865]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 863]---> Sorter-cost:  649     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 861]---> Sorter-cost: 2282     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 859]---> BDD-cost:  162
c ---[ 857]---> BDD-cost:  158
c ---[ 855]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 853]---> Adder-cost: 257   maxlim: 61410   bits: 17/16
c ---[ 851]---> Adder-cost: 601   maxlim: 118230   bits: 18/17
c ---[ 849]---> Adder-cost: 469   maxlim: 117211   bits: 18/17
c ---[ 847]---> Adder-cost: 373   maxlim: 118230   bits: 18/17
c ---[ 845]---> Adder-cost: 710   maxlim: 300434   bits: 20/19
c ---[ 843]---> Adder-cost: 450   maxlim: 300434   bits: 20/19
c ---[ 841]---> Adder-cost: 591   maxlim: 250285   bits: 19/18
c ---[ 839]---> BDD-cost:  144
c ---[ 837]---> Adder-cost: 637   maxlim: 493917   bits: 20/19
c ---[ 835]---> BDD-cost:  153
c ---[ 833]---> Adder-cost: 253   maxlim: 39410   bits: 17/16
c ---[ 831]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 829]---> Sorter-cost: 1273     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 827]---> Sorter-cost: 1854     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 825]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 823]---> Adder-cost: 472   maxlim: 675799   bits: 21/20
c ---[ 821]---> Adder-cost: 276   maxlim: 544718   bits: 21/20
c ---[ 819]---> Adder-cost: 339   maxlim: 491475   bits: 20/19
c ---[ 817]---> Adder-cost: 300   maxlim: 651204   bits: 21/20
c ---[ 815]---> Adder-cost: 246   maxlim: 491475   bits: 20/19
c ---[ 813]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 811]---> Adder-cost: 250   maxlim: 315280   bits: 20/19
c ---[ 809]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 807]---> Sorter-cost: 1867     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 805]---> BDD-cost:  117
c ---[ 803]---> Sorter-cost: 1762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 801]---> Sorter-cost: 1854     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 799]---> Adder-cost: 338   maxlim: 73707   bits: 18/17
c ---[ 797]---> Sorter-cost: 1854     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 795]---> Sorter-cost: 1775     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 793]---> BDD-cost:  143
c ---[ 791]---> Adder-cost: 230   maxlim: 73707   bits: 18/17
c ---[ 789]---> BDD-cost:  135
c ---[ 787]---> Sorter-cost: 1509     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 785]---> Sorter-cost: 1781     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 783]---> Sorter-cost: 1781     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 781]---> Sorter-cost: 1775     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 779]---> Sorter-cost: 1850     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 777]---> Sorter-cost: 1863     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 775]---> Adder-cost: 378   maxlim: 171983   bits: 19/18
c ---[ 773]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 771]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 769]---> Adder-cost: 276   maxlim: 43505   bits: 17/16
c ---[ 767]---> Sorter-cost: 1258     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 765]---> Sorter-cost:  356     Base: 2 2 2 2 2 2 2 2 2
c ---[ 763]---> Adder-cost: 210   maxlim: 36853   bits: 17/16
c ---[ 761]---> Adder-cost: 350   maxlim: 107502   bits: 18/17
c ---[ 759]---> Adder-cost: 246   maxlim: 78820   bits: 18/17
c ---[ 757]---> Adder-cost: 732   maxlim: 458074   bits: 20/19
c ---[ 755]---> Adder-cost: 438   maxlim: 418664   bits: 20/19
c ---[ 753]---> Adder-cost: 1156   maxlim: 2782179   bits: 22/22
c ---[ 751]---> Adder-cost: 1116   maxlim: 4018703   bits: 23/22
c ---[ 749]---> Adder-cost: 406   maxlim: 300943   bits: 20/19
c ---[ 747]---> Adder-cost: 690   maxlim: 287123   bits: 20/19
c ---[ 745]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 743]---> BDD-cost:  109
c ---[ 741]---> Adder-cost: 778   maxlim: 832713   bits: 21/20
c ---[ 739]---> Adder-cost: 874   maxlim: 606486   bits: 21/20
c ---[ 737]---> Adder-cost: 510   maxlim: 606486   bits: 21/20
c ---[ 735]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 733]---> Adder-cost: 468   maxlim: 277406   bits: 20/19
c ---[ 731]---> Adder-cost: 215   maxlim: 30198   bits: 16/15
c ---[ 729]---> Adder-cost: 363   maxlim: 119254   bits: 18/17
c ---[ 727]---> Adder-cost: 426   maxlim: 77789   bits: 18/17
c ---[ 725]---> Adder-cost: 256   maxlim: 37363   bits: 17/16
c ---[ 723]---> Adder-cost: 298   maxlim: 158650   bits: 19/18
c ---[ 721]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 719]---> Adder-cost: 436   maxlim: 106448   bits: 18/17
c ---[ 717]---> Adder-cost: 914   maxlim: 1194582   bits: 22/21
c ---[ 715]---> Adder-cost: 210   maxlim: 36853   bits: 17/16
c ---[ 713]---> Adder-cost: 390   maxlim: 70628   bits: 18/17
c ---[ 711]---> Adder-cost: 511   maxlim: 237484   bits: 19/18
c ---[ 709]---> Adder-cost: 414   maxlim: 103386   bits: 18/17
c ---[ 707]---> Adder-cost: 278   maxlim: 50158   bits: 17/16
c ---[ 705]---> Adder-cost: 245   maxlim: 28660   bits: 16/15
c ---[ 703]---> Adder-cost: 518   maxlim: 202162   bits: 19/18
c ---[ 701]---> Adder-cost: 240   maxlim: 57321   bits: 17/16
c ---[ 699]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 697]---> Adder-cost: 169   maxlim: 30198   bits: 16/15
c ---[ 695]---> Sorter-cost: 1273     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 693]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 691]---> BDD-cost:  126
c ---[ 689]---> Sorter-cost:  549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 687]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 685]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 683]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 681]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 679]---> Sorter-cost:  566     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 677]---> Adder-cost: 210   maxlim: 36853   bits: 17/16
c ---[ 675]---> Adder-cost: 214   maxlim: 37876   bits: 17/16
c ---[ 673]---> Adder-cost: 210   maxlim: 36853   bits: 17/16
c ---[ 671]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 669]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 667]---> Adder-cost: 160   maxlim: 18934   bits: 16/15
c ---[ 665]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2
c ---[ 663]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 661]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 659]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 657]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 655]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Adder-cost: 246   maxlim: 78820   bits: 18/17
c ---[ 651]---> Sorter-cost: 1705     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> BDD-cost:  139
c ---[ 647]---> Adder-cost: 248   maxlim: 78820   bits: 18/17
c ---[ 645]---> Sorter-cost: 1283     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 643]---> Sorter-cost: 1283     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 639]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 637]---> Sorter-cost: 1273     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> Sorter-cost: 1093     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost: 1207     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 631]---> Sorter-cost: 1198     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 629]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 627]---> Sorter-cost: 1032     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 625]---> Sorter-cost: 1493     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> BDD-cost:  112
c ---[ 621]---> Adder-cost: 611   maxlim: 247206   bits: 19/18
c ---[ 619]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 617]---> BDD-cost:  126
c ---[ 615]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 613]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 611]---> Sorter-cost: 1260     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Adder-cost: 342   maxlim: 84961   bits: 18/17
c ---[ 607]---> Adder-cost: 374   maxlim: 202162   bits: 19/18
c ---[ 605]---> Adder-cost: 180   maxlim: 22008   bits: 16/15
c ---[ 603]---> Adder-cost: 182   maxlim: 16887   bits: 16/15
c ---[ 601]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 599]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 597]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 595]---> Sorter-cost: 1260     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 593]---> Adder-cost: 450   maxlim: 300434   bits: 20/19
c ---[ 591]---> BDD-cost:  157
c ---[ 589]---> Adder-cost: 166   maxlim: 27128   bits: 16/15
c ---[ 587]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 585]---> BDD-cost:  117
c ---[ 583]---> Sorter-cost:  509     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 581]---> BDD-cost:  110
c ---[ 577]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 573]---> Adder-cost: 222   maxlim: 25587   bits: 16/15
c ---[ 571]---> BDD-cost:  127
c ---[ 569]---> Adder-cost: 166   maxlim: 27128   bits: 16/15
c ---[ 567]---> Adder-cost: 276   maxlim: 81384   bits: 18/17
c ---[ 565]---> Adder-cost: 320   maxlim: 135640   bits: 19/18
c ---[ 563]---> Sorter-cost: 2260     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 561]---> BDD-cost:  121
c ---[ 559]---> Sorter-cost: 2046     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 557]---> Sorter-cost: 2061     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 555]---> Sorter-cost: 1932     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 553]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Sorter-cost: 1932     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost: 1865     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 543]---> Sorter-cost: 1932     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 541]---> Sorter-cost:  757     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 539]---> Sorter-cost: 1469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 537]---> BDD-cost:  113
c ---[ 535]---> BDD-cost:  117
c ---[ 533]---> Sorter-cost: 2070     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 531]---> Sorter-cost: 2063     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 529]---> BDD-cost:  135
c ---[ 527]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 525]---> Sorter-cost: 2758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 523]---> Adder-cost: 224   maxlim: 49648   bits: 17/16
c ---[ 521]---> Adder-cost: 285   maxlim: 101857   bits: 18/17
c ---[ 519]---> Sorter-cost: 1404     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 517]---> Adder-cost: 214   maxlim: 54256   bits: 17/16
c ---[ 515]---> Sorter-cost: 1260     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 513]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 511]---> Sorter-cost:  367     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 509]---> Sorter-cost:  367     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 505]---> Adder-cost: 252   maxlim: 81384   bits: 18/17
c ---[ 503]---> Sorter-cost: 1428     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 501]---> Sorter-cost: 1932     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 499]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost: 1099     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost:  798     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost: 1795     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Adder-cost: 425   maxlim: 231831   bits: 19/18
c ---[ 489]---> Adder-cost: 271   maxlim: 220569   bits: 19/18
c ---[ 487]---> Adder-cost: 334   maxlim: 84441   bits: 18/17
c ---[ 485]---> Sorter-cost: 1070     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Adder-cost: 499   maxlim: 247185   bits: 19/18
c ---[ 481]---> Sorter-cost: 1632     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> BDD-cost:  112
c ---[ 477]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost:  485     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:  880     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> BDD-cost:  108
c ---[ 469]---> Sorter-cost: 1932     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> BDD-cost:  107
c ---[ 465]---> Sorter-cost: 1370     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 463]---> Sorter-cost: 1376     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Sorter-cost: 1139     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost:  583     Base: 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost: 1932     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Adder-cost: 308   maxlim: 186282   bits: 19/18
c ---[ 451]---> Adder-cost: 322   maxlim: 151995   bits: 19/18
c ---[ 449]---> Adder-cost: 297   maxlim: 79321   bits: 18/17
c ---[ 447]---> Adder-cost: 259   maxlim: 77790   bits: 18/17
c ---[ 445]---> Adder-cost: 247   maxlim: 52713   bits: 17/16
c ---[ 443]---> Adder-cost: 264   maxlim: 148410   bits: 19/18
c ---[ 441]---> Adder-cost: 384   maxlim: 183723   bits: 19/18
c ---[ 439]---> Adder-cost: 406   maxlim: 187821   bits: 19/18
c ---[ 437]---> Adder-cost: 260   maxlim: 229785   bits: 19/18
c ---[ 435]---> Adder-cost: 544   maxlim: 292248   bits: 20/19
c ---[ 433]---> Adder-cost: 613   maxlim: 257959   bits: 19/18
c ---[ 431]---> Sorter-cost:  935     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost:  711     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost:  743     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 423]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> Sorter-cost: 1651     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 419]---> Sorter-cost: 1610     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 417]---> Sorter-cost:  422     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 413]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 411]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> Sorter-cost: 1911     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> Sorter-cost: 2063     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 399]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 397]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 395]---> Sorter-cost:  346     Base: 2 2 2 2 2 2 2 2 2
c ---[ 393]---> Sorter-cost: 1139     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 389]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 387]---> BDD-cost:  126
c ---[ 385]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 383]---> BDD-cost:   82
c ---[ 381]---> BDD-cost:   85
c ---[ 379]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> BDD-cost:   98
c ---[ 375]---> Sorter-cost:  627     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> BDD-cost:   99
c ---[ 371]---> Sorter-cost: 1588     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 369]---> Adder-cost: 499   maxlim: 207797   bits: 19/18
c ---[ 367]---> Adder-cost: 541   maxlim: 206775   bits: 19/18
c ---[ 365]---> Sorter-cost: 1775     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 363]---> BDD-cost:   83
c ---[ 361]---> BDD-cost:   77
c ---[ 359]---> BDD-cost:   85
c ---[ 357]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 355]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 353]---> BDD-cost:   87
c ---[ 351]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> Sorter-cost:  718     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> BDD-cost:   99
c ---[ 345]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> Sorter-cost: 1775     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> Sorter-cost:  609     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 339]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 337]---> Sorter-cost: 9265     Base: 7 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 335]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 333]---> Sorter-cost: 2390     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 331]---> Adder-cost: 386   maxlim: 108506   bits: 18/17
c ---[ 329]---> Sorter-cost:  632     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 327]---> Adder-cost: 253   maxlim: 39410   bits: 17/16
c ---[ 325]---> Sorter-cost: 2573     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 323]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 321]---> Sorter-cost:  856     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> Sorter-cost:  856     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 317]---> Adder-cost: 430   maxlim: 1975668   bits: 22/21
c ---[ 315]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 313]---> Sorter-cost: 1303     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> Sorter-cost: 1297     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 309]---> Adder-cost: 421   maxlim: 493917   bits: 20/19
c ---[ 307]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> Sorter-cost: 1932     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost:  451     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost: 2556     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Sorter-cost:  534     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 295]---> Adder-cost: 652   maxlim: 297362   bits: 20/19
c ---[ 293]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 291]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 289]---> Sorter-cost: 1244     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 287]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 285]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 281]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 279]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 277]---> Sorter-cost: 1689     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 275]---> Sorter-cost: 1651     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 273]---> Adder-cost: 178   maxlim: 19959   bits: 16/15
c ---[ 271]---> BDD-cost:  121
c ---[ 269]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 267]---> Sorter-cost: 1273     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 265]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 263]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 261]---> Sorter-cost: 1273     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 259]---> Sorter-cost: 1932     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 257]---> Sorter-cost: 1651     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost:  368     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost: 1260     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost: 2040     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost: 1273     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost: 1932     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 241]---> Sorter-cost:  518     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 239]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> Sorter-cost: 1307     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost: 1848     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 233]---> BDD-cost:  112
c ---[ 231]---> BDD-cost:   87
c ---[ 229]---> BDD-cost:   83
c ---[ 227]---> Sorter-cost: 1775     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 225]---> Sorter-cost:  893     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> BDD-cost:  104
c ---[ 219]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  328     Base: 2 2 2 2 2 2 2 2 2
c ---[ 213]---> BDD-cost:   85
c ---[ 211]---> Sorter-cost: 1651     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost:  782     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 205]---> BDD-cost:  122
c ---[ 203]---> BDD-cost:  126
c ---[ 201]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> BDD-cost:   73
c ---[ 197]---> Adder-cost: 450   maxlim: 300434   bits: 20/19
c ---[ 195]---> BDD-cost:  153
c ---[ 193]---> BDD-cost:  153
c ---[ 191]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Adder-cost: 386   maxlim: 418664   bits: 20/19
c ---[ 187]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 185]---> Adder-cost: 253   maxlim: 39410   bits: 17/16
c ---[ 183]---> Adder-cost: 253   maxlim: 39410   bits: 17/16
c ---[ 181]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost: 1651     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost:  843     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Adder-cost: 632   maxlim: 2472025   bits: 22/22
c ---[ 171]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 167]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 165]---> Adder-cost: 248   maxlim: 39410   bits: 17/16
c ---[ 163]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 161]---> BDD-cost:  125
c ---[ 157]---> BDD-cost:  130
c ---[ 155]---> BDD-cost:  134
c ---[ 153]---> BDD-cost:  130
c ---[ 151]---> Sorter-cost: 1711     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 145]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Adder-cost: 248   maxlim: 78820   bits: 18/17
c ---[ 139]---> Sorter-cost:  328     Base: 2 2 2 2 2 2 2 2 2
c ---[ 137]---> BDD-cost:  126
c ---[ 135]---> Adder-cost: 205   maxlim: 31728   bits: 16/15
c ---[ 133]---> Adder-cost: 215   maxlim: 29174   bits: 16/15
c ---[ 131]---> Adder-cost: 421   maxlim: 493917   bits: 20/19
c ---[ 129]---> Adder-cost: 480   maxlim: 305047   bits: 20/19
c ---[ 127]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 125]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[ 123]---> Sorter-cost: 1273     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 121]---> Sorter-cost: 1273     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 117]---> Sorter-cost:  362     Base: 2 2 2 2 2 2 2 2 2
c ---[ 115]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 111]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost:  701     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost:  856     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> Sorter-cost:  904     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost: 2495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  99]---> Adder-cost: 246   maxlim: 39410   bits: 17/16
c ---[  97]---> Sorter-cost: 2044     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  95]---> BDD-cost:  121
c ---[  93]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Adder-cost: 424   maxlim: 1975668   bits: 22/21
c ---[  89]---> Sorter-cost: 1632     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Adder-cost: 253   maxlim: 129015   bits: 18/17
c ---[  79]---> Adder-cost: 270   maxlim: 31984   bits: 16/15
c ---[  76]---> BDD-cost:   29
c ---[  75]---> BDD-cost:   35
c ---[  73]---> BDD-cost:   38
c ---[  72]---> BDD-cost:   34
c ---[  71]---> Sorter-cost: 1079     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    5
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:    8
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   11
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   11
c ---[  59]---> BDD-cost:   13
c ---[  58]---> BDD-cost:    6
c ---[  57]---> BDD-cost:   10
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:    9
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   10
c ---[  51]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:   10
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:    7
c ---[  44]---> BDD-cost:    5
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:   13
c ---[  41]---> BDD-cost:    8
c ---[  40]---> BDD-cost:    5
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    7
c ---[  36]---> BDD-cost:    7
c ---[  35]---> BDD-cost:    8
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:    9
c ---[  32]---> BDD-cost:    7
c ---[  31]---> BDD-cost:    4
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:    2
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    6
c ---[  24]---> BDD-cost:   10
c ---[  23]---> BDD-cost:    6
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    2
c ---[  18]---> BDD-cost:    8
c ---[  17]---> BDD-cost:    8
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    2
c ---[  11]---> BDD-cost:    7
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:   12
c ---[   8]---> BDD-cost:    7
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    7
c ---[   5]---> BDD-cost:    7
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   26
c ---[   0]---> BDD-cost:   23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1109627  3129556 |  369875       0        0     nan |  0.000 % |
c |       101 | 1107482  3124735 |  406862      98      579     5.9 |  6.356 % |
c |       251 | 1107482  3124735 |  447548     248     1814     7.3 |  6.356 % |
c |       476 | 1107480  3124731 |  492303     471     3013     6.4 |  6.356 % |
c |       814 | 1107179  3124052 |  541533     775     4648     6.0 |  6.382 % |
c |      1323 | 1107156  3124001 |  595687    1282    14996    11.7 |  6.384 % |
c |      2082 | 1106230  3121929 |  655256    2032    20153     9.9 |  6.451 % |
c |      3221 | 1106137  3121721 |  720781    3147    30743     9.8 |  6.459 % |
c |      4929 | 1106133  3121713 |  792859    4854    54130    11.2 |  6.460 % |
c |      7492 | 1106004  3121427 |  872145    7403    82062    11.1 |  6.471 % |
c |     11336 | 1105691  3120718 |  959360   11202   147210    13.1 |  6.498 % |
c |     17103 | 1103836  3116528 | 1055296   16899   293531    17.4 |  6.648 % |
c |     25754 | 1103836  3116528 | 1160826   25550   692449    27.1 |  6.648 % |
c |     38728 | 1100641  3109222 | 1276908   38513  1236115    32.1 |  6.920 % |
c |     58189 | 1100626  3109188 | 1404599   57969  2375412    41.0 |  6.921 % |
c |     87382 | 1100532  3108969 | 1545059   87136  4318036    49.6 |  6.931 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 27329 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 27325
Raw data (stat): 27325 (runsolver) R 27324 7475 7474 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842200529 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+9.99937 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+19.9999 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+29.9996 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+39.9992 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+49.9997 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+59.9993 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0002 s]
Raw data (loadavg): 1.06 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+99.9997 s]
Raw data (loadavg): 1.05 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+109.999 s]
Raw data (loadavg): 1.04 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120 s]
Raw data (loadavg): 1.04 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.001 s]
Raw data (loadavg): 1.03 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.001 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.001 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.002 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.002 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.002 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.003 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.002 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.002 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.003 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.003 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.003 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.002 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.003 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.003 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.003 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.004 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.004 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.004 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.005 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27329
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.75 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 27382
Raw data (stat): 27325 (minisat+_script) S 27324 7475 7474 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842200529 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.75
CPU time (s): 1229.9
CPU user time (s): 1228.58
CPU system time (s): 1.3188
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####